This program is tentative and subject to change.

Tue 22 Oct 2024 11:00 - 11:30 at San Gabriel - System level analysis

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.

This program is tentative and subject to change.

Tue 22 Oct

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

11:00 - 12:30
System level analysisSAS at San Gabriel
11:00
30m
Full-paper
Lift-offline: Instruction Lifter Generators
SAS
Nicholas Coughlin Defence Science and Technology Group, Australia, Alistair Michael , Kait Lam
11:30
30m
Short-paper
Fixing Latent Unsound Abstract Operators in the eBPF Verifier of the Linux Kernel (NEAT paper)
SAS
Pre-print
12:00
30m
Short-paper
Verifying components of Arm® Confidential Computing Architecture with ESBMC (NEAT paper)
SAS
Tong Wu , Shale Xiong ARM, Edoardo Manino , Gareth Stockwell ARM, Lucas C. Cordeiro University of Manchester, UK and Federal University of Amazonas, Brazil