ENSOFT Research · Verification

Large-Scale Software Verification

ENSOFT’s research verifies the Linux kernel at scale—37 million lines and 66,609 lock instances—and develops certification evidence schemas, invisible control flow resolution, compiler equivalence, and human-machine collaboration.

LUEVIDENCE KITlock / unlock · multi-MLOC call graph · evidence kit
Linux Kernel Verification66,609 Lock Instances

Large-Scale Verification, Certification Evidence & Human-Machine Collaboration

SAE Technical Paper 2025-01-8088 · 2025Legacy Embedded Security

Detecting Cyber-Security Vulnerabilities in Legacy Safety-Critical Software with Tight Performance Constraints

Adapts software verification and comprehension techniques originally developed for the Department of Defense (DoD) to detect cybersecurity vulnerabilities in legacy automotive and embedded software operating under tight real-time performance and small memory-footprint constraints.

Payas Awadhutkar, Ahmed Tamrawi, Jeremías Sauceda10.4271/2025-01-8088

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 →

15 July 2023Path Algebra · Soft Infinity

Path Algebra for Scalable and Transparent Software Security

Introduces Path Algebra, a non-commutative ring built on SymPy and integrated into Atlas to represent the “soft infinity” of execution behaviors without enumerating paths. Execution paths are modeled as products of variables, branches as sums, and loops as divisions with loop bodies represented once—enabling scalable, transparent verification and vulnerability analysis across C, C++, Java, Simulink, bytecode, and binaries.

Suresh KothariRead the paper →

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 Kothari10.1016/j.cose.2022.102608

Science of Computer Programming · 2018DARPA STAC

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

ICSE · 2018DARPA STAC · PCG 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

Winter Simulation Conference · 2017DARPA STAC

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

99.3% vs. 65.7%Of 66,609 Linux kernel lock instances verified across 12+ MLOC, uncovering 7 unsafe locks fixed by kernel developers.
APSEC · 2016DARPA STAC · Path-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

ICSE · 2014DARPA APAC

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

4 April 201499% Path Reduction · EFG

Event-Flow Graphs for Efficient Path-Sensitive Analyses

Partitions control-flow graph paths into equivalence classes via a linear-time transformation into an Event-Flow Graph (EFG), a compact CFG derivative whose paths preserve all property-relevant event traces. Evaluated on the Linux kernel (v3.12) for spin safe-synchronization, achieving close to 99% reduction for CFGs with a large number of paths and demonstrating human comprehensibility in a controlled experiment.

Ahmed Tamrawi, Suresh KothariRead the paper →