P14_22: Formal Security Evaluation of Executing Untrusted Binaries on Embedded Processors
Topic Areas: System-Level Security Solutions
Principal investigator: Dr. Kevin Hamlen, University of Texas at Dallas
Co-Principal investigator(s): Dr. Yiorgos Makris, University of Texas at Dallas
Machine-verified formal reasoning on computer programs is a powerful methodology to ensure their correctness, safety and trust, backed by mathematical theorems and proofs. As a result, this method has been applied on systems which require high assurance of correctness, safety and security. While formal reasoning is commonly performed on high-level source code, such as C or C++, there are many instances where the source code is unavailable or impossible to be analyzed. To fill this gap, the PI developed the PicinÆ platform to perform semi-automated, machine-verified formal reasoning on binary native programs. To assure system security, however, it is necessary to also extend security evaluation down to the hardware implementation. In this regard, the proof-carrying hardware intellectual property (PCHIP) framework, developed by the co-PI, provides capabilities to reason on the hardware description language (HDL). However, PCHIP uses a different formal representation than PicinÆ, which makes the unification of these two frameworks challenging and difficult. Therefore, this project seeks to enhance these frameworks and develop a unified platform, capable of semi-automatic reasoning on binary programs being executed on a specific microprocessor implementation provided as HDL code. In the first two years of this project, we improved PCHIP-V2 framework to enable it to handle more complicated security properties of microprocessor implementation. Also, to improve the usability of PicinÆ, a powerful simplifier has been developed to reason over binary integer arithmetic in hardware and software models, with a proof of soundness. In the last year of this project, we propose to (i) develop an HDL-to-Coq converter to automatically convert scripts supported by PCHIP-V2 following generic conversion rules we defined, and (ii) extend the platform to support formal analysis of multi-cycle hardware logic.