ENSOFT Research · Cybersecurity

Cybersecurity & Vulnerability Analysis

ENSOFT’s cybersecurity research detects algorithmic complexity and side-channel vulnerabilities, catalogs loop termination patterns for deep fuzzing, and analyzes cyber-physical and Android malware—alongside binary remediation for legacy and safety-critical systems.

Loop pattern · Δ side channel · Projected flow
Loop termination · Side channel · Projected flow5,000+ loops

Algorithmic Complexity, Fuzzing, Side Channels & Malware Analysis

IEEE/AIAA DASC · 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 SaucedaIEEE/AIAA DASC 2026 · Best of Session

SAE AeroTech / Technical Paper 2026-01-0088 · 2026Localized Binary Rewriting

Minimal Binary Patching for Safety-Critical Systems

Presents a binary-rewriting method that computes the exact binary-level impact of a source change to generate localized byte-level patches rather than regenerating the entire executable—capturing changes that would alter thousands of bytes upon recompilation in only a few bytes to reduce OTA bandwidth and minimize disruption to certified aerospace and automotive software.

Payas Awadhutkar, Jeremías Sauceda, Ahmed Tamrawi10.4271/2026-01-0088

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

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 →

July 2022Loop Termination Patterns

Deep Fuzzing Through Cataloging Common Loop Termination Patterns

Introduces a backwards-searching fuzzing approach informed by an empirical catalog of common loop termination patterns. Rather than treating loops like ordinary branches—which exhausts traditional fuzzers around 15–20% coverage—pattern-aware loop summaries allow test generation to navigate complex loops and reach deep control-flow states.

Jeremías Sauceda, Payas Awadhutkar, Tim FraserRead the paper →

5,000+ Loops CatalogedUses empirical loop termination pattern catalogs and backwards symbolic search to penetrate past traditional fuzzer bottlenecks.
Springer · 2018DARPA STAC · ICS & 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

ACM/IEEE ICSE Companion · 2018DARPA STAC · Technical 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

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

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

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

2015DARPA APAC · Comprehension-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 →

12 November 2013Order-Preserving CFG Reductions

Reduction-Based Transformations on Control Flow Graphs

Models software vulnerabilities—including unsafe thread synchronization, memory leaks, and smartphone data exfiltration—as ordered occurrences of event nodes along control-flow paths, and defines size-reducing graph transformations that collapse exponential CFGs while preserving vulnerability-relevant ordering.

Akshay Deepak, Ahmed Tamrawi, Suresh KothariRead the paper →