Chloe Fortuna (STR), JT Paasch (STR), Sam Lasser (Draper), Philip Zucker (Draper), Chris Casinghino (Jane Street), Cody Roux (AWS)

Modifying a binary program without access to the original source code is an error-prone task. In many cases, the modified binary must be tested or otherwise validated to ensure that the change had its intended effect and no others—a process that can be labor-intensive. This paper presents CBAT, an automated tool for verifying the correctness of binary transformations. CBAT’s approach to this task is based on a differential program analysis that checks a relative correctness property over the original and modified versions of a function. CBAT applies this analysis to the binary domain by implementing it as an extension to the BAP binary analysis toolkit. We highlight several features of CBAT that contribute to the tool’s efficiency and to the interpretability of its output. We evaluate CBAT’s performance by using the tool to verify modifications to three collections of functions taken from real-world binaries.

View More Papers

PriSrv: Privacy-Enhanced and Highly Usable Service Discovery in Wireless...

Yang Yang (School of Computing and Information Systems, Singapore Management University, Singapore), Robert H. Deng (School of Computing and Information Systems, Singapore Management University, Singapore), Guomin Yang (School of Computing and Information Systems, Singapore Management University, Singapore), Yingjiu Li (Department of Computer Science, University of Oregon, USA), HweeHwa Pang (School of Computing and Information Systems,…

Read More

More Lightweight, yet Stronger: Revisiting OSCORE’s Replay Protection

Konrad-Felix Krentz (Uppsala University), Thiemo Voigt (Uppsala University, RISE Computer Science)

Read More

HEIR: A Unified Representation for Cross-Scheme Compilation of Fully...

Song Bian (Beihang University), Zian Zhao (Beihang University), Zhou Zhang (Beihang University), Ran Mao (Beihang University), Kohei Suenaga (Kyoto University), Yier Jin (University of Science and Technology of China), Zhenyu Guan (Beihang University), Jianwei Liu (Beihang University)

Read More

FitM: Binary-Only Coverage-GuidedFuzzing for Stateful Network Protocols

Dominik Maier, Otto Bittner, Marc Munier, Julian Beier (TU Berlin)

Read More