ENSOFT Research · DARPA Programs

DARPA Cybersecurity Programs

ENSOFT’s multi-year DARPA cybersecurity research programs cover DARPA APAC (Automated Program Analysis for Cybersecurity) and DARPA STAC (Space/Time Analysis for Cybersecurity).

APAC · STACAFRL Technical Reports

Automated Program Analysis for Cybersecurity5 Publications ↓

DARPA APAC

Detecting novel malware in Android applications, where malicious behavior is concealed across event-driven callbacks, multithreading, and framework libraries. The program produced a comprehension-driven analysis platform on Atlas, an interactive Android Security Toolbox, and FlowMiner for mining compact information-flow summaries from large libraries. Top-performing Blue team in Phase I and top three in Phase II.

Final technical report AFRL-RI-RS-TR-2015-186, July 2015Read the report →

Space/Time Analysis for Cybersecurity18 Publications ↓

DARPA STAC

Identifying algorithmic complexity and side-channel vulnerabilities in Java bytecode. Algorithmic complexity attacks force execution paths into extreme time or memory consumption from small inputs; side-channel attacks infer secrets from resource variations across execution paths. The program produced RULER, combining loop and branch catalogs, Projected Control Graphs, and targeted dynamic analysis across seven DARPA challenge engagements.

Final technical report AFRL-RI-RS-TR-2019-232, December 2019Read the report →

AFRL-RI-RS-TR-2015-186 · ADA621995

DARPA APAC Publications

IEEE/ACM ICSE · 2015Android Security Toolbox

Security Toolbox for Detecting Novel and Sophisticated Android Malware

Demonstrates the DARPA APAC Android Security Toolbox built on Atlas, enabling human-in-the-loop malware auditing across Android source and Java bytecode against Red-team adversarial applications.

Benjamin Holland, Tom Deering, Suresh Kothari, Jon Mathews, Nikhil Ranade10.1109/ICSE.2015.235

2015Comprehension-Driven Auditing

Comprehension-Driven Program Analysis for Malware Detection in Android Apps

Formulates the comprehension-driven, human-in-the-loop malware detection methodology developed under the DARPA APAC program to vet DoD and commercial mobile marketplaces against adversarial Red-team Android malware.

Suresh Kothari, Tom Deering, Ben Holland, Ahmed Tamrawi, Akshay Deepak, Sandeep Krishnan, Damanjit Singh, Vani Bojja, Ganesh Santhanam, Jeremías Sauceda, Jon Mathews, Nikhil RanadeRead the paper →

IEEE SMC · 2014Amplified Reasoning

A “Human-in-the-Loop” Approach for Resolving Complex Software Anomalies

Presents an interactive human-in-the-loop reasoning approach for diagnosing and resolving complex cross-cutting software anomalies where fully automated static analysis produces excessive false positives or fails to scale.

Suresh Kothari, Akshay Deepak, Ahmed Tamrawi, Benjamin Holland, Sandeep Krishnan10.1109/SMC.2014.6974210

ICSE · 2014Atlas Platform

Atlas: A New Way to Explore Software, Build Analysis Tools

Presents the Atlas software analysis platform, which decouples program indexing from domain-specific analysis: polynomial-time static analyzers build an attributed graph database of the program, which engineers then query interactively or through analysis scripts. Validated on Linux kernel synchronization verification and Android malware detection.

Tom Deering, Suresh Kothari, Jeremías Sauceda, Jon Mathews10.1145/2591062.2591065

ACM/IEEE MODELS (EduSymp) · 2013Simulink & Atlas Modeling

Multi-faceted Practical Modeling Education for Software Engineering

Introduces a problem-driven modeling curriculum combining domain-specific graphical modeling in Simulink and SimDiff with program-graph query modeling in Atlas—applying two-event graph models to operating-system memory leaks, Linux kernel lock pairing, and DARPA APAC Android malware detection.

Suresh Kothari, Jeremías SaucedaRead the paper →

AFRL-RI-RS-TR-2019-232 · AD1088526

DARPA STAC Publications

ACM ESEC/FSE · 2019Algorithmic Complexity

DISCOVER: Detecting Algorithmic Complexity Vulnerabilities

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

Science of Computer Programming · 2018PCG Journal Paper

Projected Control Graph for Computing Relevant Program Behaviors

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

Springer · 2018ICS & Cyber-Physical Systems

Catastrophic Cyber-Physical Malware

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

IEEE ICSME DOCGEN Challenge · 2018Best Tool Award

DynaDoc: Automated On-Demand Context-Specific Documentation

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

ACM/IEEE ICSE Companion · 2018Technical Briefing

Demystifying Cyber-Physical Malware

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

ICSE · 2018PCG Toolbox

COMB: Computing Relevant Program Behaviors

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

Springer ICISS · 2017Side-Channel Vulnerabilities

Human-on-the-Loop Automation for Detecting Software Side-Channel Vulnerabilities

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

IEEE APSEC · 20175,000 Loops · 18 DARPA Apps

Intelligence Amplifying Loop Characterizations for Detecting Algorithmic Complexity Vulnerabilities

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 →

Winter Simulation Conference · 201766,609 Linux Locks

Modeling Lessons from Verifying Large Software Systems for Safety and Security

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

IEEE VizSec · 201777 DARPA Android Apps

Interactive Visualization Toolbox to Detect Sophisticated Android Malware

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

IEEE ICST · 2017Java Immutability Benchmark

Transferring State-of-the-Art Immutability Analyses: Experimentation Toolbox and Accuracy Benchmark

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

APSEC · 2016Path-Sensitive Analysis

Projected Control Graph for Accurate and Efficient Analysis of Safety and Security Vulnerabilities

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

IEEE SCAM · 2016Statically-Informed Dynamic Analysis

Statically-Informed Dynamic Analysis Tools to Detect Algorithmic Complexity Vulnerabilities

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

IEEE ISSRE Workshops (FVPE) · 2016Formal Verification Practice

Insights for Practicing Engineers from a Formal Verification Study of the Linux Kernel

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

IEEE ICPC · 2016Invisible Control Flow

Human-Machine Resolution of Invisible Control Flow

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

ACM ICSE Companion · 2016Human-Machine Collaboration

Rethinking Verification: Accuracy, Efficiency and Scalability through Human-Machine Collaboration

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

ACM ICSE Companion · 201637 MLOC · L-SAP

Let’s Verify Linux: Accelerated Learning of Analytical Reasoning through Automation and Collaboration

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

ACM/IEEE SER&IP · 2016Best Paper Award

Software Engineering Research Lab to Airplanes, Orion and Beyond

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