Automating Information Flow Analysis of Low Level Code
2014 (English)In: Proceedings of CCS’14, November 3–7, 2014, Scottsdale, Arizona, USA, Association for Computing Machinery (ACM), 2014Conference paper (Refereed)
Low level code is challenging: It lacks structure, it uses jumps and symbolic addresses, the control ow is often highly optimized, and registers and memory locations may be reused in ways that make typing extremely challenging. Information ow 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 nal-state account of noninterference. In this work we propose a novel approach to relational verication for machine code. Verication goals are expressed as equivalence of traces decorated with observation points. Relational verication conditions are propagated between observation points using symbolic execution, and discharged using rst-order reasoning. We have implemented an automated tool that integrates with SMT solvers to automate the verication task. The tool transforms ARMv7 binaries into an intermediate, architecture-independent format using the BAP toolset by means of a veried translator. We demonstrate the capabilities of the tool on a separation kernel system call handler, which mixes hand-written assembly with gcc-optimized output, a UART device driver and a crypto service modular exponentiation routine.
Place, publisher, year, edition, pages
Association for Computing Machinery (ACM), 2014.
Information Flow Security, Formal Verification, Symbolic Execution;, Machine Code
IdentifiersURN: urn:nbn:se:kth:diva-150489DOI: 10.1145/2660267.2660322ScopusID: 2-s2.0-84910645826ISBN: 978-1-4503-2957-6OAI: oai:DiVA.org:kth-150489DiVA: diva2:743673
CCS’14, November 3–7, 2014, Scottsdale, Arizona, USA
QC 201409052014-09-042014-09-042014-09-08Bibliographically approved