Synthesizing Evidence of Emergent Computation (SEEC)

Bits of apparently harmless code or minor software bugs can allow bad actors control over entire systems. When researchers examine how an attack occurred, they often find that the affected computer system works differently in practice from how it was designed to work. Emergent computations – or behaviors of a system resulting from subtle complexities of its implementation – often arise from the difference between the implementation and the system designers’ intention. In many cases, emergent computations enabled by a vulnerability in a system can be combined in a programmable way. This leads many security researchers to describe the process of exploitation as an exercise in “programming a weird machine.”

Currently, only good luck prevents exploits that leverage emergent computations. After a vulnerability is exposed, researchers may develop tools to find similar errors in other systems, but these solutions are only effective for the discovered threat. There is a real need for systems to have secure designs from the outset – but there currently are no effective tools to help designers determine whether their designs allow unexpected emergent computation.

Discover, Analyze, Generate, and Identify

DARPA created the Artificial Intelligence Mitigations of Emergent Execution (AIMEE) program to anticipate the potential for emergent computations early in a system’s design. 

Galois’s project, as part of the AIMEE program, is Synthesizing Evidence of Emergent Computation (SEEC). SEEC aims 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.

Do Emergent Computations Dream of Weird Machines?

SEEC’s theoretical framework is based on our previous work (available on arxiv) on understanding weird machines, which provides a formal approach for identifying when a system allows emergent computation.

SEEC aims to analyze both a high-level design and lower-level implementation of a system to identify emergent computations; it identifies compositional structures that would make those computations programmable.

The SEEC framework uses syntax-guided synthesis to find potentially vulnerable components and generate example emergent computations by combining rule-based reasoning with example-driven learning. While existing tools use synthesis techniques to generate exploits, SEEC is innovative because it uses synthesis techniques to identify any emergent computations that may have programmable structure, rather than focusing on specific, human-engineered computations that target known vulnerabilities.

SEEC is being built upon Rosette, a Racket dialect with support for solver-aided programming. SEEC users will be able to model a wide variety of system designs, allowing designers to both avoid emergent computations in the design of new systems, and explore potential mitigations to vulnerabilities and exploit techniques discovered in existing systems.

A Framework to Eliminate the Need for Costly Custom Tools

If successful, SEEC will do the following: 

• Define a theory of emergent computation with unambiguous criteria for evaluating weird machine programmability.
• Demonstrate the feasibility of program synthesis for identifying whether a system design can admit emergent computations.
• Develop a reusable reasoning framework that can prototype programs and vulnerability mitigations.

SEEC has many potential applications for industry and government-based technologists. SEEC could primarily provide system designers with powerful new abilities to design systems that are resilient to emergent computations. Secondly, SEEC could give designers and researchers the capability to evaluate numerous mitigation possibilities. 

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. 

This project’s end result 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.

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.