Automating Information Flow Analysis of Low Level Code

Low level code is challenging: It lacks structure, it uses jumps and symbolic addresses, the control flow is often highly optimized, and registers and memory locations may be reused in ways that make typing extremely challenging. Informa-tion flow properties create additional complications: They are hyperproperties relating multiple executions, and the possibility of interrupts and concurrency, and use of devices and features like memory-mapped I/O requires a departure from the usual initial-state final-state account of noninterfer-ence. In this work we propose a novel approach to relational verification for machine code. Verification goals are ex-pressed as equivalence of traces decorated with observation points. Relational verification conditions are propagated be-tween observation points using symbolic execution, and dis-charged using first-order reasoning. We have implemented an automated tool that integrates with SMT solvers to au-tomate the verification task. The tool transforms ARMv7 binaries into an intermediate, architecture-independent for-mat using the BAP toolset by means of a verified translator. We demonstrate the capabilities of the tool on a separation kernel system call handler, which mixes hand-written assem-bly with gcc-optimized output, a UART device driver and a crypto service modular exponentiation routine