P15_21: 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: 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 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 year of this project, in addition to making enhancements to Picin, we developed a new PCHIP framework, namely PCHIP-V2, which follows the formal representation in Picin more closely and facilitates their unification. By the end of the first year, we will have demonstrated this unified framework on a single cycle RISC-V processor using proofs developed manually. For the second year of this project, we propose to (i) extend PCHIP-V2 with a tactic library to enable semi-automatic proof-writing and (ii) extend the platform to a more complex (e.g., pipelined) RISC-V implementation. By enabling unified formal reasoning across binary code and microprocessor design, the proposed 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.