Binary Code Analysis

Existing binary analysis tools cannot verify the security of safety-critical embedded systems — automotive brake controllers, implantable cardiac devices, defence-grade avionics. Source-level auditing is not enough, because compiler optimizations open a semantic gap between the written source and the compiled binary that actually runs on the hardware.

A two-phase programme. 

Phase 1 tests existing tools (OOAnalyzer/Pharos, Ramblr/Angr) against increasingly complex compiled C++ binaries and shows they fail to resolve polymorphic, vtable-dispatched calls. 

Phase 2 proposes a binary-native formal verification framework combining abstract interpretation on machine code, Three-Valued Abstraction Refinement (TVAR), and SMT-based translation validation — achieving 100% detection of injected semantic faults, zero false positives, and zero runtime overhead, validated on a RISC-V SystemC TLM-2.0 virtual prototype.