Information Trust Institute block of abstract images
Information Trust Institute block of abstract images

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.