Formal Methods (Software)

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.

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.

Unreliable software places huge costs on both the military and the civilian economy. Currently, most Commercial Off-the-Shelf (COTS) software contains about one to five bugs per thousand lines of code. Formal verification of software provides the most confidence that a given piece of software is free of errors that could disrupt military and government operations. Unfortunately, traditional formal verification methods do not scale to the size of software found in modern computer systems. Formal verification also currently requires highly specialized engineers with deep knowledge of software technology and mathematical theorem-proving techniques.

Embedded systems form a ubiquitous, networked, computing substrate that underlies much of modern technological society. Such systems range from large supervisory control and data acquisition (SCADA) systems that manage physical infrastructure to medical devices such as pacemakers and insulin pumps, to computer peripherals such as printers and routers, to communication devices such as cell phones and radios, to vehicles such as airplanes and satellites. Such devices have been networked for a variety of reasons, including the ability to conveniently access diagnostic information, perform software updates, provide innovative features, lower costs, and improve ease of use.

As new defensive technologies make old classes of vulnerability difficult to exploit successfully, adversaries move to new classes of vulnerability. Vulnerabilities based on flawed implementations of algorithms have been popular targets for many years. However, once new defensive technologies make vulnerabilities based on flawed implementations less common and more difficult to exploit, adversaries will turn their attention to vulnerabilities inherent in the algorithms themselves.