Formal Methods for Provably Secure Software and Firmware

Abstract

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.