October 22, 2024
Conference Paper

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.

Published: October 22, 2024

Citation

Whyatt M.V., C.B. Powers, E.L. Pollans, B.J. Van Vaerenbergh, J.A. Peterson, and R.Y. Martinez. 2024. Formal Methods for Provably Secure Software and Firmware. In Proceedings of the 65th Annual Meeting of the Institute of Nuclear Materials Management, July 21-25, 2024, Portland, OR. Mount Laurel, New Jersey:Institute of Nuclear Materials Management. PNNL-SA-200727.

Research topics