diff options
| -rw-r--r-- | src/focaccia/symbolic.py | 43 | ||||
| -rwxr-xr-x | src/focaccia/tools/capture_transforms.py | 5 | ||||
| -rw-r--r-- | src/focaccia/trace.py | 7 |
3 files changed, 34 insertions, 21 deletions
diff --git a/src/focaccia/symbolic.py b/src/focaccia/symbolic.py index 444145f..321b39d 100644 --- a/src/focaccia/symbolic.py +++ b/src/focaccia/symbolic.py @@ -663,8 +663,9 @@ def collect_symbolic_trace(env: TraceEnvironment, # Predict next concrete state. # We verify the symbolic execution backend on the fly for some # additional protection from bugs in the backend. - predicted_regs = transform.eval_register_transforms(lldb_state) - predicted_mems = transform.eval_memory_transforms(lldb_state) + if env.cross_validate: + predicted_regs = transform.eval_register_transforms(lldb_state) + predicted_mems = transform.eval_memory_transforms(lldb_state) # Step forward target.step() @@ -674,23 +675,25 @@ def collect_symbolic_trace(env: TraceEnvironment, # Verify last generated transform by comparing concrete state against # predicted values. assert(len(strace) > 0) - for reg, val in predicted_regs.items(): - conc_val = lldb_state.read_register(reg) - if conc_val != val: - warn(f'Symbolic execution backend generated false equation for' - f' [{hex(instruction.addr)}]: {instruction}:' - f' Predicted {reg} = {hex(val)}, but the' - f' concrete state has value {reg} = {hex(conc_val)}.' - f'\nFaulty transformation: {transform}') - for addr, data in predicted_mems.items(): - conc_data = lldb_state.read_memory(addr, len(data)) - if conc_data != data: - warn(f'Symbolic execution backend generated false equation for' - f' [{hex(instruction.addr)}]: {instruction}: Predicted' - f' mem[{hex(addr)}:{hex(addr+len(data))}] = {data},' - f' but the concrete state has value' - f' mem[{hex(addr)}:{hex(addr+len(data))}] = {conc_data}.' - f'\nFaulty transformation: {transform}') - raise Exception() + if env.cross_validate: + for reg, val in predicted_regs.items(): + conc_val = lldb_state.read_register(reg) + if conc_val != val: + warn(f'Symbolic execution backend generated false equation for' + f' [{hex(instruction.addr)}]: {instruction}:' + f' Predicted {reg} = {hex(val)}, but the' + f' concrete state has value {reg} = {hex(conc_val)}.' + f'\nFaulty transformation: {transform}') + for addr, data in predicted_mems.items(): + conc_data = lldb_state.read_memory(addr, len(data)) + if conc_data != data: + warn(f'Symbolic execution backend generated false equation for' + f' [{hex(instruction.addr)}]: {instruction}: Predicted' + f' mem[{hex(addr)}:{hex(addr+len(data))}] = {data},' + f' but the concrete state has value' + f' mem[{hex(addr)}:{hex(addr+len(data))}] = {conc_data}.' + f'\nFaulty transformation: {transform}') + raise Exception() return Trace(strace, env) + diff --git a/src/focaccia/tools/capture_transforms.py b/src/focaccia/tools/capture_transforms.py index 552b855..0b084da 100755 --- a/src/focaccia/tools/capture_transforms.py +++ b/src/focaccia/tools/capture_transforms.py @@ -16,9 +16,12 @@ def main(): prog.add_argument('-o', '--output', default='trace.out', help='Name of output file. (default: trace.out)') + prog.add_argument('-c', '--cross-validate', + default=False, + help='Cross-validate symbolic equations with concrete values') args = prog.parse_args() - env = TraceEnvironment(args.binary, args.args, utils.get_envp()) + env = TraceEnvironment(args.binary, args.args, args.cross_validate, utils.get_envp()) trace = collect_symbolic_trace(env, None) with open(args.output, 'w') as file: parser.serialize_transformations(trace, file) diff --git a/src/focaccia/trace.py b/src/focaccia/trace.py index 094358f..c72d90f 100644 --- a/src/focaccia/trace.py +++ b/src/focaccia/trace.py @@ -10,11 +10,13 @@ class TraceEnvironment: def __init__(self, binary: str, argv: list[str], + cross_validate: bool, envp: list[str], binary_hash: str | None = None): self.argv = argv self.envp = envp self.binary_name = binary + self.cross_validate = cross_validate if binary_hash is None: self.binary_hash = file_hash(binary) else: @@ -26,6 +28,7 @@ class TraceEnvironment: return cls( json['binary_name'], json['argv'], + json['cross_validate'], json['envp'], json['binary_hash'], ) @@ -36,6 +39,7 @@ class TraceEnvironment: 'binary_name': self.binary_name, 'binary_hash': self.binary_hash, 'argv': self.argv, + 'cross_validate': self.cross_validate, 'envp': self.envp, } @@ -46,11 +50,13 @@ class TraceEnvironment: return self.binary_name == other.binary_name \ and self.binary_hash == other.binary_hash \ and self.argv == other.argv \ + and self.cross_validate == other.cross_validate \ and self.envp == other.envp def __repr__(self) -> str: return f'{self.binary_name} {" ".join(self.argv)}' \ f'\n bin-hash={self.binary_hash}' \ + f'\n options=cross-validate' \ f'\n envp={repr(self.envp)}' class Trace(Generic[T]): @@ -72,3 +78,4 @@ class Trace(Generic[T]): def __repr__(self) -> str: return f'Trace with {len(self.states)} trace points.' \ f' Environment: {repr(self.env)}' + |