diff options
Diffstat (limited to 'focaccia.py')
| -rwxr-xr-x | focaccia.py | 222 |
1 files changed, 222 insertions, 0 deletions
diff --git a/focaccia.py b/focaccia.py new file mode 100755 index 0000000..f0c6efe --- /dev/null +++ b/focaccia.py @@ -0,0 +1,222 @@ +#!/usr/bin/env python3 + +import argparse +import platform +from typing import Callable, Iterable + +import focaccia.parser as parser +from focaccia.arch import supported_architectures, Arch +from focaccia.compare import compare_simple, compare_symbolic, ErrorTypes +from focaccia.lldb_target import LLDBConcreteTarget +from focaccia.match import fold_traces, match_traces +from focaccia.snapshot import ProgramState +from focaccia.symbolic import collect_symbolic_trace, SymbolicTransform +from focaccia.utils import print_result, get_envp +from focaccia.reproducer import Reproducer +from focaccia.compare import ErrorSeverity +from focaccia.trace import Trace, TraceEnvironment + +verbosity = { + 'info': ErrorTypes.INFO, + 'warning': ErrorTypes.POSSIBLE, + 'error': ErrorTypes.CONFIRMED, +} + +concrete_trace_parsers = { + 'focaccia': lambda f, _: parser.parse_snapshots(f), + 'qemu': parser.parse_qemu, + 'arancini': parser.parse_arancini, +} + +_MatchingAlgorithm = Callable[ + [list[ProgramState], list[SymbolicTransform]], + tuple[list[ProgramState], list[SymbolicTransform]] +] + +matching_algorithms: dict[str, _MatchingAlgorithm] = { + 'none': lambda c, s: (c, s), + 'simple': match_traces, + 'fold': fold_traces, +} + +def collect_concrete_trace(env: TraceEnvironment, breakpoints: Iterable[int]) \ + -> list[ProgramState]: + """Gather snapshots from a native execution via an external debugger. + + :param env: Program to execute and the environment in which to execute it. + :param breakpoints: List of addresses at which to break and record the + program's state. + + :return: A list of snapshots gathered from the execution. + """ + target = LLDBConcreteTarget(env.binary_name, env.argv, env.envp) + + # Set breakpoints + for address in breakpoints: + target.set_breakpoint(address) + + # Execute the native program + snapshots = [] + while not target.is_exited(): + snapshots.append(target.record_snapshot()) + target.run() + + return snapshots + +def parse_arguments(): + parser = argparse.ArgumentParser() + parser.description = '''An emulator tester and verifier. + +You can pre-record symbolic traces with `tools/capture_transforms.py`, then pass +them to the verifier with the --oracle-trace argument. +''' + + # Specification of the symbolic truth trace + symb_trace = parser.add_mutually_exclusive_group(required=True) + symb_trace.add_argument('-p', '--oracle-program', + help='A program from which a symbolic truth will be' + ' recorded.') + symb_trace.add_argument('-o', '--oracle-trace', '--symb-trace', + help='A symbolic trace that serves as a truth state' + ' for comparison.') + parser.add_argument('-a', '--oracle-args', + nargs='*', + default=[], + help='Arguments to the oracle program.') + parser.add_argument('-e', '--oracle-env', + nargs='*', + help='Override the oracle program\'s environment during' + ' symbolic and concrete execution.') + + # Specification of the concrete test trace + parser.add_argument('-t', '--test-trace', + required=True, + help='The concrete test states to test against the' + ' symbolic truth.') + parser.add_argument('--test-trace-type', + default='focaccia', + choices=list(concrete_trace_parsers.keys()), + help='Log file format of the tested program trace.' + ' [Default: focaccia]') + + # Algorithm and output control + parser.add_argument('--match', + choices=list(matching_algorithms.keys()), + default='simple', + help='Select an algorithm to match the test trace to' + ' the truth trace. Only applicable if --symbolic' + ' is enabled.' + ' [Default: simple]') + parser.add_argument('--symbolic', + action='store_true', + default=False, + help='Use an advanced algorithm that uses symbolic' + ' execution to determine accurate data' + ' transformations. This improves the quality of' + ' generated errors significantly, but will take' + ' more time to complete.') + parser.add_argument('--error-level', + default='warning', + choices=list(verbosity.keys()), + help='Verbosity of reported errors. \'error\' only' + ' reports mismatches that have been detected as' + ' errors in the translation with certainty.' + ' \'warning\' will report possible errors that' + ' may as well stem from incomplete input data.' + ' \'info\' will report absolutely everything.' + ' [Default: warning]') + parser.add_argument('--no-verifier', + action='store_true', + default=False, + help='Don\'t print verifier output.') + + # Reproducer + parser.add_argument('--reproducer', + action='store_true', + default=False, + help='Generate repoducer executables for detected' + ' errors.') + + return parser.parse_args() + +def print_reproducer(result, min_severity: ErrorSeverity, oracle, oracle_args): + for res in result: + errs = [e for e in res['errors'] if e.severity >= min_severity] + #breakpoint() + if errs: + rep = Reproducer(oracle, oracle_args, res['snap'], res['ref']) + print(rep.asm()) + return + +def get_test_trace(args, arch: Arch) -> Trace[ProgramState]: + path = args.test_trace + parser = concrete_trace_parsers[args.test_trace_type] + with open(path, 'r') as txl_file: + return parser(txl_file, arch) + +def get_truth_env(args) -> TraceEnvironment: + oracle = args.oracle_program + oracle_args = args.oracle_args + if args.oracle_env: + oracle_env = args.oracle_env + else: + oracle_env = get_envp() + return TraceEnvironment(oracle, oracle_args, oracle_env) + +def get_symbolic_trace(args): + if args.oracle_program: + env = get_truth_env(args) + print('Tracing', env) + return collect_symbolic_trace(env) + elif args.oracle_trace: + with open(args.oracle_trace, 'r') as file: + return parser.parse_transformations(file) + raise AssertionError() + +def main(): + args = parse_arguments() + + # Determine the current machine's architecture. The log type must match the + # architecture on which focaccia is executed because focaccia wants to + # execute the reference program concretely. + if platform.machine() not in supported_architectures: + print(f'Machine {platform.machine()} is not supported! Exiting.') + exit(1) + arch = supported_architectures[platform.machine()] + + # Parse reference trace + test_trace = get_test_trace(args, arch) + + # Compare reference trace to a truth + if args.symbolic: + symb_trace = get_symbolic_trace(args) + match = matching_algorithms[args.match] + conc, symb = match(test_trace.states, symb_trace.states) + + result = compare_symbolic(conc, symb) + oracle_env = symb_trace.env + else: + if not args.oracle_program: + print('Argument --oracle-program is required for non-symbolic' + ' verification!') + exit(1) + + # Record truth states from a concrete execution of the oracle + breakpoints = [state.read_register('PC') for state in test_trace] + env = get_truth_env(args) + truth_trace = collect_concrete_trace(env, breakpoints) + + result = compare_simple(test_trace.states, truth_trace) + oracle_env = env + + if not args.no_verifier: + print_result(result, verbosity[args.error_level]) + + if args.reproducer: + print_reproducer(result, + verbosity[args.error_level], + oracle_env.binary_name, + oracle_env.argv) + +if __name__ == '__main__': + main() |