A Step Toward Trustworthy Binary Verification

Nov 30, 2023, 11:30-12:30 WWH 335

Many production software systems are available only in binary form. This is due to several
reasons including intellectual property and proprietary issues, outdated and decaying build
processes and environments, and third-party libraries and tools that are no longer available or
backwards compatible. Security vulnerability analysis of such software is still a necessary task
due to the need to rapidly patch program errors, especially those that can be used to create
security exploits, i.e., unintended, or malicious behaviors or leak sensitive data. A large body of
work has focused on this problem space including disassembly, decompilation, and binary
verification, among others. A common denominator of these approaches is binary lifting: raw
unstructured data is lifted to a form for reasoning over behavior and semantics. Majority of
existing binary lifting approaches are untrustworthy (e.g., misses jump targets, misidentifies
code as data), which negatively affects the trust base of techniques that rely on them.

In this talk, I will present an approach for binary lifting that simultaneously disassembles,
recovers control flow, and generates formal proofs on the correctness of the lifted
representation and a class of sanity properties including return address integrity, bounded
control flow, and calling conventIon adherence. Establishing these properIes allows the binary
to be liKed to a representatIon that contains an over-approximaIon of all possible executIon
paths of the binary. The lifted representatIon contains proof obligatIons that are sufficient to
formally prove – by exportIng to a theorem-prover – the sanity properIes and correctness of
the lifted representatIon, which removes the lifting algorithm and its implementatIon from the
trust base. We apply this approach to Linux FoundatIon’s Xen Hypervisor covering about 400K
instructIons, providing evidence of its effectiveness and scalability for trustworthy binary liKing
of off-the-shelf productIon software. I will argue that such a verified lifted representatIon not
only reduces the trust base of downstream techniques (e.g., binary verificatIon), but also
exposes novel ways for reasoning about related problems (e.g., binary patching).

Binoy Ravindran (hZps://binoyravindran.github.io) is a Professor of Electrical and Computer
Engineering and Bradley Senior Faculty Fellow Endowed Professor at Virginia Tech, where he
leads the Systems Software Research Group. He joined Virginia Tech in 1998, aKer receiving his PhD in Computer Science from the University of Texas at Arlington that same year. His research is broadly in computer systems, with a focus on programmability, performance, security, energy efficiency, and realtime. Together with his students, postdocs, and collaborators, Prof. Ravindran has published more than 320 papers, which have been honored with nine best paper awards or nominatIons. He has mentored 11 research assistant professors, 19 postdoctoral scholars, and 24 PhD students, 17 of whom are tenured or tenure-track faculty members. Dr. Ravindran is an ACM DistInguished ScientIst, was an Office of Naval Research Faculty Fellow at the US Naval Surface Warfare Center Dahlgren Division, and is (or was) an editorial board member of ACM and IEEE journals including TECS, TC, TPDS, TCC, TSUSC, and Design & Test.