Binary Interface Compatibility for Library Integration in C++

Abstract

Shared libraries evolve, and when a new version changes its binary interface in a way that an already-compiled consumer depends on, the program can fail at load time or silently misbehave at runtime. These application binary interface (ABI) breaks are easy to introduce and hard to diagnose, and in a large software stack a single missed break can force costly recompilation across many components. This thesis presents veriabi, an ABI compatibility checker for C++ shared libraries whose decision procedure is formally verified. Compatibility is specified as an explicit predicate over three layers of the Itanium C++ ABI, covering exported symbols, function and object signatures, and type layout. For each rule a decision procedure is defined in the Rocq proof assistant and proved sound and complete against the specification. The verified core is extracted to OCaml and paired with an unverified C++ front-end that reads ELF and DWARF from two compiled libraries. An optional consumer-aware extension takes the consumer’s compiled LLVM IR and narrows the verdict to the breaks that consumer can observe, with the filtering proved sound with respect to the strict result. On a controlled corpus with known ground truth, veriabi catches every in-scope break (18 of 18), while the established tools abidiff and abi_compliance_checker each miss two to three mainstream changes, such as a base-class reorder or a strong-to-weak binding change. On a 554 MB production library from ASML it completes in about four minutes against more than two hours for the closest comparable tool, and produces a report two orders of magnitude smaller. The work shows that ABI compatibility checking can be given an explicit specification, a decision procedure, and a machine-checked proof that the two agree, at a cost low enough to run on real industrial libraries.