Defense Advanced Research Projects AgencyTagged Content List

Formal Methods (Software)

Mathematical techniques for verification of hardware and software systems

Showing 11 results for Formal + Trust RSS
12/04/2013
Ever more sophisticated cyber attacks exploit software vulnerabilities in the Commercial Off-the-Shelf (COTS) IT systems and applications upon which military, government and commercial organizations rely. The most rigorous way to thwart these attacks is formal verification, an analysis process that helps ensure that software is free from exploitable flaws and vulnerabilities. Traditional formal methods, however, require specially trained engineers to manually scour software—a process that up to now has been too slow and costly to apply beyond small software components.
| Cyber | Formal | Trust |
05/03/2019
Military systems are increasingly using software to support functionality, new capabilities, and beyond. Before a new piece of software can be deployed within a system however, its functional safety and compliance with certain standards must be verified and ultimately receive certification. As the rapid rate of software usage continues to grow, it is becoming exceedingly difficult to assure that all software considered for military use is coded correctly and then tested, verified, and documented appropriately.
November 14-16, 2018,
Hilton Washington Dulles Airport
DARPA’s Information Innovation Office is co-hosting the first annual seL4 Summit along with the Air Force Research Laboratory and General Dynamics C4 Systems. seL4 is an open-source, high-assurance, high-performance microkernel; its implementation is formally proven correct against its specification. The three-day seL4 Summit will focus on maturing seL4 kernel technology, stabilizing software distribution, expanding user adoption, and transitioning the technology into various applications. Attendees will also have the opportunity to receive hands-on training for the microkernel.
| Cyber | Formal | Trust |
To be effective, Department of Defense (DoD) cybersecurity solutions require rapid development times. The shelf life of systems and capabilities is sometimes measured in days. Thus, to a greater degree than in other areas of defense, cybersecurity solutions require that DoD develops the ability to build quickly, at scale and over a broad range of capabilities.
The process of determining that a software system’s risk is acceptable is referred to as “certification.” Current certification practices within the Department of Defense (DoD) are antiquated and unable to scale with the amount of software deployed. Two factors prevent scaling: (a) the use of human evaluators to determine if the system meets certification criteria, and (b) the lack of a principled means to decompose evaluations.
| Cyber | Formal | Trust |