Tue 22 Oct 2024 12:00 - 12:30 at San Gabriel - Tracing bugs and flaws Chair(s): Aditya V. Thakur

Binary analysis techniques depend on instruction lifters to map instruction encodings to their semantic effects. Existing work has demonstrated automatic methods to extract such semantics from trustworthy architecture specifications, on a per-instruction basis. We extend these results to extract the semantics of all instructions at once, effectively generating an instruction lifter. We attain this result through the offline partial evaluation of formal architecture specifications, along with their analysis via instruction opcode sensitive abstract domains. To illustrate the approach, we generate a generic instruction lifter for ARMv8 and specialise it to a series of use cases. In addition to the static analysis of architecture specifications, this approach permits the static analysis of the generated lifter. We exploit this to establish bounds on lifter behaviours and its produced semantics.

Tue 22 Oct

Displayed time zone: Pacific Time (US & Canada) change

11:00 - 12:30
Tracing bugs and flawsSAS at San Gabriel
Chair(s): Aditya V. Thakur University of California at Davis
11:00
60m
Keynote
Measuring data lineage: when program analysis meets data science
SAS
12:00
30m
Full-paper
Lift-offline: Instruction Lifter Generators
SAS
Nicholas Coughlin Defence Science and Technology Group, Australia, Alistair Michael , Kait Lam
Pre-print