ENSOFT Research · DARPA STAC · 2015–2019
DARPA’s STAC program set out to find vulnerabilities in how Java software spends time and memory: small inputs that drive a loop into extreme resource consumption, and differences in running time or memory use that leak a secret. Fully automated detection amounts to solving the halting problem. The team’s answer was RULER, an intelligence-amplifying system on Atlas that pairs automated analysis with a human analyst, tested across seven DARPA engagements.
An execution path with high time or space complexity that a relatively small input can trigger. The cost comes from a loop the input controls, so the analysis has to know every loop: what ends it, what bounds it, what it calls, and whether external input reaches it.
A set of execution paths tied to a secret, where variations in running time or memory use along those paths let an attacker infer the secret. Finding one means reasoning about the paths that depend on the secret and what each of them costs.
STAC measured progress on two axes. Scale meant analyses that handle network services of hundreds of thousands of lines and systems of millions or tens of millions. Speed meant the rate at which a human analyst, helped by automated tools, works through that code. The program targeted the software the U.S. government, military, and economy depend on.
RULER runs as a set of Eclipse plug-ins on Atlas and divides the work between machine and analyst. Automation characterizes every loop and branch in the bytecode and points to suspicious code. The analyst forms a hypothesis, tests it against graphs of only the relevant behavior, and confirms it by fuzzing only the code in question. The report names the approach after Frederick Brooks’s thesis that intelligence amplification beats AI: a machine and a mind can beat a mind-imitating machine working by itself.
Figure 1 · RULER system architectureExecutive Summary →
Catalogs record 65 attributes for every loop, 44 characteristics for every branch, and the lambda loops that Java 8 lambda expressions form. Projected Control Graphs group a method’s paths into the behaviors relevant to AC and SC, taint analysis marks what external input reaches, and JDK subsystem tags show which APIs each loop touches.
Figures 1–8 · Table 1Read →
The analyst tests a hypothesis with a Dashboard of sixteen properties and smells, a PCG Builder that computes interprocedural PCGs across chosen events, a builder that keeps the loops calling into a subsystem, a decompiler view beside the Jimple, a Filter View, and eighteen Smart Views.
Figures 9–13Read →
The Mockingbird framework extracts the suspicious code with Atlas analyzers, and its Object Mocker builds the test harness automatically, so the AFL fuzzer, through Kelinci, drives just that code with binary inputs to show whether the vulnerability can be exploited. The chapter closes with the analysts’ workflows for AC and SC questions in time and space.
Mockingbird · AFL · KelinciRead →
One row per loop and one column per characteristic. Sorting a column ranks the loops, and a selection drives Atlas Smart Views.
Properties and smells computed on demand, such as recursive functions, System.exit usage, and deeply nested loops.
Events chosen across several functions become one interprocedural PCG, with ancestor and expandable functions for context.
The Jimple of the selected method beside its Java source, decompiled with CFR one method at a time.
The blue teams worked through seven DARPA engagements, live and take-home. The team’s accuracy rose with each set of challenge applications and reached 100% in E5 and E6. E7 required every team to answer every question, and accuracy dipped. The engagements exposed the approach’s weaknesses and pointed to each refinement, and the program manager recommended the IA technology for potential adoption.
Figure 14 · Engagement performanceRead →
AFRL-RI-RS-TR-2019-232 · AD1088526
The research questions behind RULER and the five categories of program analysis challenge it addresses.
The team, the program’s goals in DARPA’s words, and the three analysis guidelines.
The architecture, the four catalogs, the Loop Call Graph, the Projected Control Graph, taint analysis, and subsystem tagging.
The Dashboard, the PCG and Loop Subsystem Interactions Builders, the decompiler view, the Filter View, and the Smart Views.
The Mockingbird framework and the analysts’ workflows for AC and SC in time and space.
The seven engagements and the case for intelligence amplification in program analysis.
A journal paper, a book chapter, seventeen conference papers, eighteen keynotes and invited talks, fourteen tutorials, the references, an appendix on Atlas, and the acronyms.
Abstract: The STAC program enabled us to make significant advances. We consider the foremost advance to be intelligence amplifying (IA) technology for detecting AC and SC vulnerabilities. The report describes the challenges encountered and how we have addressed them. Our performance steadily improved with the advances we made with our approach. We achieved top performance on DARPA challenge engagements. We found the take-home and on-site engagements very useful to drive our research. The engagements enabled us to identify the weaknesses in our approach and provided concrete directions to refine our approach.
Presents DISCOVER, a three-phase human-on-the-loop tool suite for detecting Algorithmic Complexity Vulnerabilities (ACVs) in Java source and bytecode through automated loop characterization, suspicious loop filtering, and interactive audit.
Payas Awadhutkar, Ganesh Ram Santhanam, Benjamin Holland, Suresh Kothari10.1145/3338906.3341177
Defines a mathematical foundation for isolating the program behaviors relevant to a safety or security property and introduces the Projected Control Graph (PCG) to compute that projection directly, avoiding full-program path enumeration. Evaluated on Linux kernel lock verification and on interactive detection of side-channel vulnerabilities in Java bytecode.
Ahmed Tamrawi, Suresh Kothari10.1016/j.scico.2018.04.003
Examines how sophisticated cyber-physical malware (such as Industroyer) exploits sensor-driven triggers and application-specific payloads in industrial control systems, telecommunications, and mission-critical software, outlining hypothesis-driven program analysis techniques to counter behavioral explosion.
Suresh Kothari, Ganesh Ram Santhanam, Payas Awadhutkar, Benjamin Holland, Jon Mathews, Ahmed Tamrawi10.1007/978-3-319-97643-3_7
An on-demand documentation engine built on Atlas and XCSG that extracts control flow, call, and data-flow graphs alongside issue and commit history from multi-million-line codebases. Demonstrated on Apache POI, where data-flow projections exposed undocumented parameter constraints and uncovered a previously unreported defect.
Ahmed Tamrawi, Sharwan Ram, Payas Awadhutkar, Benjamin Holland, Ganesh Ram Santhanam, Suresh Kothari10.1109/DYSDOC3.2018.00009
Synthesizes the mathematical foundations, program analysis techniques, and real-world case studies needed to characterize and verify sophisticated cyber-physical malware whose sensor-driven triggers and domain-specific payloads evade traditional virus and trojan signatures.
Suresh Kothari10.1145/3183440.3183459
Presents COMB, a multi-language interactive program comprehension and verification tool that uses the Projected Control Graph (PCG) abstraction to derive relevant execution behaviors directly without enumerating all program paths. Demonstrated on C and Java case studies including Linux kernel verification.
Benjamin Holland, Payas Awadhutkar, Suresh Kothari, Ahmed Tamrawi, Jon Mathews10.1145/3183440.3183476
Introduces canonical side-channel patterns, program artifact filters, and parameterized graph models that empower analysts to formulate and verify software side-channel vulnerability (SSCV) hypotheses in time and space.
Ganesh Ram Santhanam, Benjamin Holland, Suresh Kothari, Nikhil Ranade10.1007/978-3-319-72598-7_13
Defines loop abstractions and behavioral patterns to filter complex loops with high likelihood of Algorithmic Complexity Vulnerabilities, evaluated across more than 5,000 loops from 4 open-source libraries and 18 DARPA STAC challenge applications.
Payas Awadhutkar, Ganesh Ram Santhanam, Benjamin Holland, Suresh KothariRead the paper →
An empirical verification study of 66,609 lock instances across more than 12 million lines of the Linux kernel. High-level behavior models verified 99.3% of the instances—compared to 65.7% for the Linux Driver Verification formal verification tool—exposed flaws in prior verification results, and uncovered seven unsafe locking defects confirmed and fixed by kernel developers.
Suresh Kothari, Payas Awadhutkar, Ahmed Tamrawi, Jon Mathews10.1109/WSC.2017.8247886
Presents the Android Malicious Flow Visualization Toolbox (AMFVT) for interactive exploration of complex Android semantics, reporting audit accuracy and efficiency across 77 sophisticated DARPA challenge Android applications.
Ganesh Ram Santhanam, Benjamin Holland, Suresh Kothari, Jon Mathews10.1109/VIZSEC.2017.8062197
Re-implements points-to and type-system object immutability analyses on Atlas for Java 8 source and compiled bytecode, introducing an experimentation toolbox and accuracy benchmark to evaluate precision and scalability on large real-world applications.
Benjamin Holland, Ganesh Ram Santhanam, Suresh Kothari10.1109/ICST.2017.55
Introduces the Projected Control Graph (PCG) abstraction to overcome exponential path growth and path-feasibility complexity in path-sensitive analysis. Evaluates CFG-to-PCG reduction across three versions of the Linux kernel (66,609 lock instances), revealing synchronization bugs missed by the Linux Driver Verification (LDV) tool.
Ahmed Tamrawi, Suresh Kothari10.1109/APSEC.2016.026
Combines static graph exploration on Atlas to isolate candidate loops with targeted dynamic analysis that evaluates selected loops across varied inputs to trigger and confirm excessive space/time consumption.
Benjamin Holland, Ganesh Ram Santhanam, Payas Awadhutkar, Suresh Kothari10.1109/SCAM.2016.23
Examines practical barriers to adopting formal verification in industry through an empirical audit of the Linux Driver Verification (LDV) tool, focusing on cross-checking verification results, certification evidence, and IDE integration.
Suresh Kothari, Payas Awadhutkar, Ahmed Tamrawi10.1109/ISSREW.2016.9
Presents an interactive human-machine collaboration approach on Atlas to resolve Invisible Control Flow (ICF) caused by dynamic binding, function pointers, and asynchronous callbacks, uncovering complex synchronization bugs in the Linux kernel.
Suresh Kothari, Ahmed Tamrawi, Jon Mathews10.1109/ICPC.2016.7503727
Contrasts traditional standalone formal verification with human-machine collaboration frameworks that generate compact visual evidence for human cross-checking on intractable verification problems.
Suresh Kothari, Ahmed Tamrawi, Jon Mathews10.1145/2889160.2891046
Introduces Evidence-Enabled Collaborative Verification (EECV) and the L-SAP tool on Atlas, generating Instance Verification Kits (IVKs) to verify 66,609 lock instances across three versions of the Linux kernel (37 MLOC).
Suresh Kothari, Ahmed Tamrawi, Jeremías Sauceda, Jon Mathews10.1145/2889160.2889192
Traces two decades of translating academic program analysis and modeling research into industrial tools deployed across avionics, automotive systems, NASA’s Orion spacecraft program, and the DARPA APAC and STAC cybersecurity initiatives.
Suresh C. Kothari10.1145/2897022.2897032