P9_20: 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
PI Email
Abstract:
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. Closed-source libraries and components, and low-level binary runtime libraries are some examples of such a case. To fill this gap, the PI developed PicinÆ, a new platform for performing semi-automated, machine-verified formal reasoning on binary native programs and transformations over them. PicinÆ relies on an abstract representation of the processor executing the code, which may not necessarily be accurate or trusted, due to inaccurate microprocessor specification, incomplete translation of the specification to the abstract representation, or existence of possible security bugs and/or hardware Trojans in its implementation. Since the hardware can no longer be considered as the root of trust, in order to assure the security of the system, it is necessary to extend security evaluation all the way down to the hardware implementation as well. 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) code of hardware designs, including microprocessors. While PCHIP enables the development of machine-verifiable proofs of security and correctness for hardware designs, it uses a different formal representation than PicinÆ, which makes the unification of these two frameworks challenging and difficult. Therefore, this project aims 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. By enabling unified formal reasoning across binary code and microprocessor design, this unified framework can eliminate the current boundary between the software security and hardware trust evaluation, and will be able to provide a much higher level of security assurance for mission-critical systems utilizing embedded microprocessors.