Stephen Chapin | 20-FS-019
The objective of this project was to investigate methods aimed at improving the security of control devices used in energy delivery systems by detecting existing vulnerabilities in their firmware and preventing insertion of new vulnerabilities by malicious actors. The system we developed achieved this objective by combining binary analysis (which characterizes the behavior of firmware updates) with formal methods that provide verifiable evidence that the firmware conforms to a safety policy. This work demonstrated the feasibility of developing systems that provide formal evidence, in the form of logical proofs, of the program's behavior. For example, energy control devices could use these logical proofs to verify the behavior of software updates before installation, thus inhibiting the ability of attackers to exploit device flaws.
The results of this project form the basis of a new research thrust that we anticipate will lead towards a fully-verified software toolchain for firmware that guards against supply chain attacks that inject malware into vendor binary code or third-party libraries that operate our energy infrastructure. This work builds on and advances Lawrence Livermore National Laboratory's high-performance computing, simulation, and data science core competency, while also supporting the cybersecurity and cyber-physical resilience and the energy and resource security mission research challenges.