VeriBin: Adaptive Verification of Patches at the Binary Level
Hongwei Wu
Network and Distributed System Security (NDSS) Symposium 2025 · Day 3 · Binary Analysis
In the critical realm of software security, maintaining vulnerabilities without introducing new issues is a perpetual challenge. The adage "if it ain't broke, don't fix it" often dictates vendor behavior, particularly in high-reliability domains such as automotive or medical devices, where even minor regressions can have catastrophic consequences. The fear of inadvertently breaking existing functionality or injecting unintended changes frequently leads vendors to hesitate in applying crucial security patches. While advanced tools like Sim, Spider, and ARD have made significant strides in semantic equivalence and patch verification, their reliance on readily available source code or a complete build chain presents a substantial limitation. In many real-world scenarios, especially when dealing with third-party components or legacy systems, this crucial information is simply inaccessible.
AI review
Solid academic systems paper with a real contribution: formal, source-free patch verification at the binary level with a clean solution to the compiler-offset noise problem and a practically motivated adaptive loop. The exitus backdoor case study — detecting a supply-chain injection that survives source code review — is exactly the kind of real-world anchor that earns credibility.