Defense Advanced Research Projects AgencyTagged Content List

Formal Methods (Software)

Mathematical techniques for verification of hardware and software systems

Showing 14 results for Formal 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.
07/30/2020
Defense and commercial systems alike are riddled with legacy software that is difficult to modernize, enhance, and re-engineer, largely due to a lack of effective understanding of the underlying legacy code, which makes predicting the effect of modifications a challenge. From a defense perspective, there is a growing need to enhance or replace components of existing software in critical platforms and systems with more secure and performant code, as well as a desire to use legacy software on new hardware to improve system performance. When introducing enhancements or replacements into large legacy code bases however, there is a high risk that the new code will not safely compose with the rest of the system. Existing means of verifying that updated software is correct-by-construction focus on clean-slate software development, essentially limiting their effectiveness to software that is developed from scratch. Further, these methods assume an existing formal specification that is typically not available for a legacy system, and they require a certain level of expertise in formal methods not readily found in most developers.
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 |
July 29, 2020, from 12:00 PM to 4:00 PM (ET),
Webinar
The Information Innovation Office (I2O) is holding a Proposers Day to provide information to potential proposers on the objectives of the Verified Security and Performance Enhancement of Large Legacy Software (V-SPELLS) program in anticipation of a planned Broad Agency Announcement. The goal of the V-SPELLS program is to create a developer-accessible capability for piece-by-piece enhancement of software components with new verified code that is both correct-by-construction and compatible-by-construction, i.e., safely composable with the rest of the system.