Defense Advanced Research Projects AgencyTagged Content List

Formal Methods (Software)

Mathematical techniques for verification of hardware and software systems

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