ENSOFT Research · Binary & Compilers

Binary & Compiler Assurance

ENSOFT’s binary and compiler research covers minimal in-place binary micro-patching, compiler sanctity via control-flow equivalence, and binary vulnerability analysis for safety-critical systems.

Graph IR · CFG isomorphism4B fix → 139B patch

Binary Micro-Patching, Compiler Equivalence & Legacy Binary Security

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

4B fix → 139B patchMinimal in-place PowerPC binary patch computed via Graph IR without source recompilation or trampoline bloat.

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 →

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