Defense Advanced Research Projects AgencyTagged Content List

Formal Methods (Software)

Mathematical techniques for verification of hardware and software systems

Showing 5 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 |
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.
| Cyber | Formal | Trust |
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.
Government agencies and the military rely upon many kinds of Commercial Off-the-Shelf (COTS) commodity Information Technology (IT) devices, including mobile phones, printers, computer workstations and many other everyday items. Each of these devices is the final product of long supply chains involving many vendors from many nations providing various components and subcomponents, including considerable amounts of software and firmware. Long supply chains provide adversaries with opportunities to insert hidden malicious functionality into this software and firmware that adversaries can exploit to accomplish harmful objectives, including exfiltration of sensitive data and sabotage of critical operations.
Program Manager
Dr. Raymond “Ray” Richards joined DARPA in January 2016. His research interests focus on high assurance software and systems.
| Cyber | Formal | Trust |