Defense Advanced Research Projects AgencyTagged Content List

Formal Methods (Software)

Mathematical techniques for verification of hardware and software systems

Showing 4 results for Formal + Automation RSS
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.
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.
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.