FUNPAC: Firmware Updates Need Proof-Accompanied Code

Project Overview

The FUNPAC project addressed the need for strong verification of firmware updates against security and safety properties established by the consumer of the software. This project evaluated the state of the art for formal verification of binary software and techniques for verification of formal evidence by firmware consumers independent of the firmware producers.  The results of this project identified key gaps in the area of formal verification of binary software. In particular, we need 1) tools to analyze binaries and correlate them to high-level structures in the source code where verification conditions are defined, and 2) fully specified instruction semantics in formal reasoning systems that can be integrated with external toolchains. 

The key gap that was identified relates to problem of correlating components of binary artifacts (either static code structure or dynamic behavior with respect to memory and control) to the high-level purposes that they implement. Such a system is not reliably implementable with current compiler or binary analysis technology. Compilation tools discard too much information during the process of lowering code to binary, and binary analysis and reverse engineering tools cannot reliably reconstruct the higher-level program that the binary corresponds to. Furthermore, we identified gaps in the tooling required to implement the proof verification components of this project such that they can serve as a trusted infrastructure at edge devices. Both limitations have motivated follow-on research in the form of both LDRD and non-LDRD sponsored projects that started mid-FY2023.

Mission Impact

This project exposed significant gaps in current techniques for applied software verification that limit the adoption of formal verification in production-level (high TRL) systems designed and maintained by people outside the formal verification research community. This research meets NNSA’s goal of applying the science and technology capabilities of the Laboratory to address evolving national security threats. This project also addresses Livermore’s Mission area of Multi-Domain Deterrence because supply chain security and the concurrent problem of securely updating devices already in the field are critical components to cybersecurity for control systems in the energy sector.