One of our previous projects explored how flaws in the design and implementation of systems can introduce “weird machines” that make them vulnerable to exploitation.
Now we have begun a follow-up project, Synthesizing Evidence of Emergent Computation (SEEC). SEEC is part of DARPA’s Artificial Intelligence Mitigations of Emergent Execution (AIMEE) program, whose goal is to anticipate the potential for emergent computations early in a system’s design.
SEEC’s objective is to develop tools that allow users to:
- Analyze system designs to determine if they allow emergent computation,
- Generate concrete examples of emergent computation,
- Identify which computations pose the greatest risk of exploitation from attackers, and
- Prototype mitigations that prevent emergent computations.
SEEC is innovative because of its program synthesis approach, which automatically searches for vulnerable components and the programmable behaviors they enable. SEEC is being built upon Rosette, a Racket dialect with support for solver-aided programming.
Theoretical applications of SEEC might include prototyping novel platforms such as the secure hardware being developed by DARPA’s SSITH program.
Another application could be evaluating compiler mitigations against speculation vulnerabilities such as Spectre and Meltdown. Directly testing for the presence of information leaks that lead to these vulnerabilities is challenging. SEEC can potentially identify residual vulnerabilities after a mitigation is applied because SEEC would automatically reason about differences in possible behaviors between an ideal model of a system and a potential implementation with mitigations. Plus, SEEC performs these functions without requiring the designer to think of all possible workarounds or new exploits.
The end result of this project will be a framework that helps designers avoid costly security problems before a system or vulnerability mitigation is implemented, rather than reacting to the discovery of highly exploitable vulnerabilities in a system once it has been deployed.
For more information on SEEC, see our project page: https://galois.com/project/seec/
Approved for public release; distribution is unlimited.
This material is based upon work supported by the Defense Advanced Research Projects Agency (DARPA) under Agreement NO. HR00112090030.