Stony Brook University Computer Science

Dr. Binoy Ravindran from Virginia Tech will present a talk titled "A Step Toward Trustworthy Binary Verification".

The details of the seminar are as follow:

Title: A Step Toward Trustworthy Binary Verification

Date: Wednesday, November 27, 2024

Time: 1 PM

Venue: C105

Abstract

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 liKed representatIon contains proof obligatIons that are sufficient to formally prove – by exportIng to a theorem-prover – the sanity properIes and correctness of the liKed representatIon, which removes the liKing 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 liKed 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).

Speaker Bio

Binoy Ravindran 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 real time. Together with his students, postdocs, and collaborators, Prof. Ravindran has published more than 330 papers, which have been honored with nine best paper awards or nominations. He has mentored 11 research assistant professors, 19 postdoctoral scholars, and 25 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.