Our CircuitBot project explored the idea of using a deep supply of game players available on the Internet to solve -- indirectly -- difficult verification problems. The project was sponsored by DARPA I2O under its Crowd Source Formal Verification (CSFV) program.
DARPA Press Release 12/4/2013
Mining and Understanding Software Enclaves (MUSE).
DARPA describes the MUSE program as follows:
As computing devices become more pervasive, the software systems that control them have become increasingly more complex and sophisticated. Consequently, despite the tremendous resources devoted to making software more robust and resilient, ensuring that programs are correct—especially at scale—remains a difficult and challenging endeavor. Unfortunately, uncaught errors triggered during program execution can lead to potentially crippling security violations, unexpected runtime failure or unintended behavior, all of which can have profound negative consequences on economic productivity, reliability of mission-critical systems, and correct operation of important and sensitive cyber infrastructure.
Vulnerabilities manifest when implementations do not conform to design. Determining program correctness thus fundamentally requires a precise understanding of a program’s intended behavior, and a means to convey this understanding unambiguously in a form suitable for automated inspection. Having useful, comprehensible and efficiently checkable program specifications is therefore critical for gaining high assurance and confidence of complex software systems. Often, however, the behaviors exposed by a program's implementation do not match those defined by the program's specification, in large part because the task of writing useful, correct and efficiently checkable specifications is often as hard as the task of writing the implementations that purport to satisfy it.
To help overcome these challenges, DARPA has created the Mining and Understanding Software Enclaves (MUSE) program. MUSE seeks to make significant advances in the way software is built, debugged, verified, maintained and understood. Central to its approach is the creation of a community infrastructure built around a large, diverse and evolving corpus of software drawn from the hundreds of billions of lines of open source code available today.
An integral part of the envisioned infrastructure would be a continuously operational specification mining engine. This engine would leverage deep program analyses and foundational ideas underlying big data analytics to populate and refine a database containing inferences about useful properties, behaviors and vulnerabilities of the program components in the corpus. The collective knowledge gleaned from this effort would facilitate new mechanisms for dramatically improving software reliability, and help develop radically different approaches for automatically constructing and repairing complex software.
Among the many envisioned benefits of the program are scalable automated mechanisms to identify and repair program errors, and specification-based tools to create and synthesize new, custom programs from existing corpus elements based on properties discovered from this mining activity.
Space/Time Analysis for Cybersecurity (STAC).
DARPA describes the STAC program as follows:
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.
The Space/Time Analysis for Cybersecurity (STAC) program aims to develop new program analysis techniques and tools for identifying vulnerabilities related to the space and time resource usage behavior of algorithms, specifically, vulnerabilities to algorithmic complexity and side channel attacks. STAC seeks to enable analysts to identify algorithmic resource usage vulnerabilities in software at levels of scale and speed great enough to support a methodical search for them in the software upon which the U.S. government, military, and economy depend.
Software systems can be vulnerable to algorithmic complexity attacks in situations where an adversary can efficiently construct an input that causes one part of that system to consume super-linear space or time processing the input. The adversary’s goal is to deny service to the system’s benign users, or to otherwise disable the system by choosing a worst-case input that causes the system to attempt a computation requiring an impractically-large amount of space or time.
Side-channels are unintended indirect information flows that cause a software system to reveal secrets to an adversary. While the software may prevent the adversary from directly observing the secret, it permits the adversary to observe outputs whose varying space and time characteristics are controlled by computations involving that secret. Given sufficient knowledge of how these computations work, the adversary can deduce the secret by observing some number of outputs.
Because algorithmic resource usage vulnerabilities are the consequence of problems inherent in algorithms themselves rather than the consequence of traditional implementation flaws, traditional defensive technologies such as Address Space Layout Randomization, Data Execution Prevention, Reference Count Hardening, Safe Unlinking, and even Type-Safe programming languages do nothing to mitigate them.
The STAC program seeks advances along two main performance axes: scale and speed. Scale refers to the need for analyses that are capable of considering larger pieces of software, from those that implement network services typically in the range of hundreds of thousands of lines of source code to even larger systems comprising millions or tens of millions of lines of code. Speed refers to the need to increase the rate at which human analysts can analyze software with the help of automated tools, from thousands of lines of code per hour to tens of thousands, hundreds of thousands or millions of lines of code per hour.