Paper: Automating Information Flow Analysis of Low Level Code | BOT24

Paper: 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. Information
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 noninterference.
In this work we propose a novel approach to relational
verification for machine code. Verification goals are expressed
as equivalence of traces decorated with observation
points. Relational verification conditions are propagated between
observation points using symbolic execution, and discharged
using first-order reasoning. We have implemented
an automated tool that integrates with SMT solvers to automate
the verification task. The tool transforms ARMv7
binaries into an intermediate, architecture-independent format
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 assembly
with gcc-optimized output, a UART device driver and a
crypto service modular exponentiation routine

more here.................

Share on Google Plus

About Bradley Susser

    Blogger Comment
    Facebook Comment


Post a Comment