Binary reverse engineering tools are used in many security-critical areas. Those tools use binary lifters to lift machine code into a higher-level representation. Erroneously lifted machine code can lead to security-critical vulnerabilities not being detected. In this thesis, I present and evaluate a technique to test binary lifters against vendor-provided ISA semantics. That is a partial interpreter for the symbolic execution of an ISA’s Sail model. The resulting SMT formulas can be used to test binary lifters. Applying this technique to the reverse binary engineering tool angr using the RISC-V Sail model led to the discovery and ultimately the fix of three bugs. This work provides a handy tool for bug discovery in binary lifters and can be extended for various other purposes.     «

Binary reverse engineering tools are used in many security-critical areas. Those tools use binary lifters to lift machine code into a higher-level representation. Erroneously lifted machine code can lead to security-critical vulnerabilities not being detected. In this thesis, I present and evaluate a technique to test binary lifters against vendor-provided ISA semantics. That is a partial interpreter for the symbolic execution of an ISA’s Sail model. The resulting SMT formulas can be used to te...     »