Paper notes: Automating information flow analysis of low level code

Title: Automating information flow analysis of low level code
PDF: 68d4b37e9623d0c67e7b856b76ebe4a1.pdf

Uses BAP to lift ARMv7 code to BIL (BAP’s intermediate representation language) with the HOL4 model of ARMv7 and does forward symbolic execution to build a logical formula that describes several executions. At interesting execution points (called observation points in the paper), such as writes, offloading to SMT solving is used to verify that relational properties hold. Loops are handled by manually finding relational invariants and using them to decorate the loops aiding the verification.