Formal Analysis Tools for Cyber Security
funded by Boeing
researcher: Grigore Rosu
This effort is developing a set of cyber security enhancing tools rooted in trusted and provably correct formal semantics. The effort is supporting an initiative to increase assurance of developed software applications.
As a result of the way current compilers optimize software, formal verifiers have been known to "prove" that compiled software is correct, when in fact it is incorrect. A consequence of the lack of formal language semantics is that the results of costly testing and Verification and Validation (V&V) efforts cannot be trusted when moving to a different platform or using a different compiler. The problem is exacerbated when software is executed on embedded systems and is safety-critical.
This project will enable development of a series of powerful formal analysis tools, such as a functional program verifier, as well as a broad range of testing tools and techniques, such as semantics-based test-case generation. The goals of this work include increased trust and assurance of software and embedded software from in-house and from our supply-chain partners, and enabling of the adoption of formal methods for cyber security and ways to prove trustworthiness of software through the use of trusted tools.