Formal Methods for Provably Secure Software & Firmware

This project addresses a gap observed in verifying the programming in embedded devices used in international arms control: namely verifying that embedded programming in an arms control device does exactly what it is supposed to do, no more and no less, every time without fail, and without disclosing unauthorized information accidentally or intentionally. In critical military, aerospace, and industrial safety systems this problem is sometimes addressed using formal methods (FM). This multi-year project seeks to identify formal methods toolsets useable in arms control regimes, with emphasis on applicability, ease of use, long term availability, and support. Formal methods encompass a broad range of tools, techniques, and approaches that can be applied to computer source code before it is compiled into a binary executable. Some source code is designed to be compiled into a binary executable and executed on a desktop computer, laptop, or mobile device while others are designed to be placed into an embedded device and executed by a microprocessor or FPGA. Formal methods tools, techniques, and approaches exist for each type of source code and provide different degrees of confidence that the code will run as expected. Applying a formal method to source code typically requires programmers to spend extra time and effort. In general, the quicker and easier a formal method approach and toolset is to implement the less confidence it can give, and conversely one that is harder and more time consuming to implement usually can give greater confidence. In its first year, this project surveyed existing formal method toolsets and selected a subset suitable for code destined to execute in a microprocessor to test. Now in its second year, the project has implemented, tested, and evaluated those toolsets on exemplar source code expected in radiation detection devices. The goal is to determine whether there exists one or more formal method toolset usable in arms control devices enabling trustable embedded programming with high confidence but without being so burdensome as to be infeasible. This paper shares results to date.