ENSOFT Research

Program Analysis & Algebraic Graph Methods

ENSOFT’s research develops program analysis, graph representations, and algebraic methods for verifying and securing complex software—from operating system kernels and mobile applications to compiled binaries in safety-critical embedded systems.

XCSG / Projected Control Graph37 MLOC scale

Automated Program Analysis for Cybersecurity

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 Cybersecurity

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 →

Selected Papers

Algebra

19 November 2025

A High School Algebra Solution for the Shortest Path Problem

An algebraic framework for graph problems, demonstrated on the shortest-path problem as an alternative to traversal algorithms such as Dijkstra and Bellman–Ford. Path segments are modeled as algebraic expressions, and shortest paths—including in graphs with negative edge weights and negative cycles—are derived through equation solving and factorization rather than iterative state updates. The paper also examines “all-paths” problems where explicit graph traversal becomes intractable.

Suresh C. Kothari, Payas AwadhutkarRead the paper →

Algebraic FactorizationSolves shortest-path and all-paths formulations—including negative edge weights and negative cycles—without iterative graph traversal.

Binary

15 June 2026PowerPC · 4B fix → 139B patch

Efficient Binary Micro-Patching for Legacy and Safety-Critical Avionics Systems

In legacy aerospace and embedded systems, missing source code or build environments often make recompilation impossible, while traditional trampolining bloats the binary. This work introduces a Graph Intermediate Representation that models binary artifacts and reference relations to compute a minimal in-place patch. Demonstrated on PowerPC, where a 4-byte functional fix requires a 139-byte total patch without reassembly.

Payas Awadhutkar, Ahmed Tamrawi, Jeremías Sauceda

Computers & Security · 2022CFG Isomorphism

Control Flow Equivalence Method for Establishing Sanctity of Compiling

Rather than attempting to prove compiler correctness in the abstract, this method verifies that a compiled binary’s control flow is consistent with its source for a specific program under audit. Equivalence is established by checking control-flow graph isomorphism after semantics-preserving transformations, producing evidence suitable for manual cross-checking and tool qualification in avionics, automotive, and medical software.

Payas Awadhutkar, Ahmed Tamrawi, Ryan Goluch, Suresh Kothari

Cybersecurity

Winter Simulation Conference · 2017

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 Mathews

99.3% vs. 65.7%Of 66,609 Linux kernel lock instances verified across 12+ MLOC, uncovering 7 unsafe locks fixed by kernel developers.

Other Program Analysis

13 August 202437 MLOC · 8 Bugs

A Humane, Graph-Based Representation of Programs and Analyses

Introduces the eXtensible Common Software Graph (XCSG), a semantic graph representation and query language designed for human-machine collaboration on verification problems where standalone automation does not scale. A verification tool built on XCSG has been used to audit safety and security properties across 37 million lines of code, uncovering eight confirmed bugs.

Jon Mathews, Theodore Murdock, Jeremías Sauceda, Ahmed Tamrawi, Suresh KothariRead the paper →

Science of Computer Programming · 2018

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 Kothari

IEEE ICSME DOCGEN Challenge · 2018

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 Kothari

ICSE · 2014

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, Jeremias Sauceda, Jon Mathews