Defense Advanced Research Projects AgencyTagged Content List

Cyber

Relating to digital systems and information

Showing 12 results for Cyber + 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 |
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.