Proving Safety and Security of Binary Programs
Time: Fri 2023-06-02 09.00
Video link: https://kth-se.zoom.us/j/68807417997
Subject area: Computer Science
Doctoral student: Andreas Lindner , Teoretisk datalogi, TCS
Opponent: Dr Tamara Rezk, National Institute for Research in Digital Science and Technology (INRIA), Sophia Antipolis Cedex, France
Supervisor: Associate professor Roberto Guanciale, Teoretisk datalogi, TCS; Professor Mads Dam, Teoretisk datalogi, TCS
With the increasing ubiquity of computing devices, their correct and secure operation is of growing importance. In particular, critical components that provide core functionalities or process sensitive data have to operate as intended. Examples are operating systems that must provide proper isolation among applications, device drivers that must reliably communicate with the hardware, crypto routines that must avoid leakage of sensitive information, and low-level security mechanisms that must be implemented correctly to be effective. All these make use of hardware functionalities that are beyond plain software execution. Therefore, they should ideally be verified at binary level to accurately account for the effects their execution has on the underlying hardware systems.
Verifying properties of binary code is challenging because of its lack of structure in terms of control flows and memory representations, and the complex hardware specifics involved. In this thesis, we aim to improve the precision and trustworthiness of binary code analyses by basing the analyses on interactive theorem proving. We contribute with the new HolBA framework for binary analysis, which is built on top of the HOL4 theorem prover. This allows all implemented algorithms to produce machine-checked correctness proofs for their results. We applied this to implement translation procedures into the intermediate language BIR to facilitate analyses. The proof-producing analysis procedures we provide for program verification are the weakest precondition propagation and symbolic execution. We evaluated the framework with a number of binaries and a larger case study, which is the control software for a balancing robot. The latter has been used as an analysis target to establish execution time bounds using symbolic execution.
Since verification is carried out on models of hardware, the applicability of the verification results hinges on how well the used models reflect the actual hardware. In particular, in the context of security applications, where an attacker tries to exploit traits of hardware execution, this has received less attention in the formal methods community. We contribute with the new Scam-V methodology and tool for differential testing to discover possible instances where the attacker-exploitable behavior of a model and a real hardware system diverge. In a number of case studies with real processors, we found a number of new types of leakage that could be exploited by an attacker. Additionally, our validation exercises revealed a number of modeling issues.