Hongwei Wu (Purdue University), Jianliang Wu (Simon Fraser University), Ruoyu Wu (Purdue University), Ayushi Sharma (Purdue University), Aravind Machiry (Purdue University), Antonio Bianchi (Purdue University)

Vendors are often provided with updated versions of a piece of software, fixing known security issues.
However, the inability to have any guarantee that the provided patched software does not break the functionality of its original version often hinders patch deployment.
This issue is particularly severe when the patched software is only provided in its compiled binary form.
In this case, manual analysis of the patch's source code is impossible, and existing automated patch analysis techniques, which rely on source code, are not applicable.
Even when the source code is accessible, the necessity of binary-level patch verification is still crucial, as highlighted by the recent XZ Utils backdoor.

To tackle this issue, we propose VeriBin, a system able to compare a binary with its patched version and determine whether the patch is ''Safe to Apply'', meaning it does not introduce any modification that could potentially break the functionality of the original binary.
To achieve this goal, VeriBin checks functional equivalence between the original and patched binaries.
In particular, VeriBin first uses symbolic execution to systematically identify patch-introduced modifications.
Then, it checks if the detected patch-introduced modifications respect specific properties that guarantee they will not break the original binary's functionality.
To work without source code, VeriBin's design solves several challenges related to the absence of semantic information (removed during the compilation process) about the analyzed code and the complexity of symbolically executing large functions precisely.
Our evaluation of VeriBin on a dataset of 86 samples shows that it achieves an accuracy of 93.0% with no false positives, requiring only minimal analyst input.
Additionally, we showcase how VeriBin can be used to detect the recently discovered XZ Utils backdoor.

View More Papers

Attributing Open-Source Contributions is Critical but Difficult: A Systematic...

Jan-Ulrich Holtgrave (CISPA Helmholtz Center for Information Security), Kay Friedrich (CISPA Helmholtz Center for Information Security), Fabian Fischer (CISPA Helmholtz Center for Information Security), Nicolas Huaman (Leibniz University Hannover), Niklas Busch (CISPA Helmholtz Center for Information Security), Jan H. Klemmer (CISPA Helmholtz Center for Information Security), Marcel Fourné (Paderborn University), Oliver Wiese (CISPA Helmholtz Center…

Read More

CounterSEVeillance: Performance-Counter Attacks on AMD SEV-SNP

Stefan Gast (Graz University of Technology), Hannes Weissteiner (Graz University of Technology), Robin Leander Schröder (Fraunhofer SIT, Darmstadt, Germany and Fraunhofer Austria, Vienna, Austria), Daniel Gruss (Graz University of Technology)

Read More

Decoupling Permission Management from Cryptography for Privacy-Preserving Systems

Ruben De Smet (Department of Engineering Technology (INDI), Department of Electronics and Informatics (ETRO), Vrije Universiteit Brussel), Tom Godden (Department of Engineering Technology (INDI), Vrije Universiteit Brussel), Kris Steenhaut (Department of Engineering Technology (INDI), Department of Electronics and Informatics (ETRO), Vrije Universiteit Brussel), An Braeken (Department of Engineering Technology (INDI), Vrije Universiteit Brussel)

Read More

Cascading Spy Sheets: Exploiting the Complexity of Modern CSS...

Leon Trampert (CISPA Helmholtz Center for Information Security), Daniel Weber (CISPA Helmholtz Center for Information Security), Lukas Gerlach (CISPA Helmholtz Center for Information Security), Christian Rossow (CISPA Helmholtz Center for Information Security), Michael Schwarz (CISPA Helmholtz Center for Information Security)

Read More