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

On Requirements and Concepts for TT&C Link Key Management

Christoph Bader (Airbus Defence & Space GmbH)

Read More

On the Feasibility of CubeSats Application Sandboxing for Space...

Gabriele Marra (CISPA Helmholtz Center for Information Security), Ulysse Planta (CISPA Helmholtz Center for Information Security and Saarbrücken Graduate School of Computer Science), Philipp Wüstenberg (Chair of Space Technology, Technische Universität Berlin), Ali Abbasi (CISPA Helmholtz Center for Information Security)

Read More

Exploring the Influence of Prompts in LLMs for Security-Related...

Weiheng Bai (University of Minnesota), Qiushi Wu (IBM Research), Kefu Wu, Kangjie Lu (University of Minnesota)

Read More

Securing Lidar Communication through Watermark-based Tampering Detection (Long)

Michele Marazzi, Stefano Longari, Michele Carminati, Stefano Zanero (Politecnico di Milano)

Read More