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

Rapid Vulnerability Mitigation with Security Workarounds

Zhen Huang (Pennsylvania State University), Gang Tan (Pennsylvania State University)

Read More

ShapFuzz: Efficient Fuzzing via Shapley-Guided Byte Selection

Kunpeng Zhang (Shenzhen International Graduate School, Tsinghua University), Xiaogang Zhu (Swinburne University of Technology), Xi Xiao (Shenzhen International Graduate School, Tsinghua University), Minhui Xue (CSIRO's Data61), Chao Zhang (Tsinghua University), Sheng Wen (Swinburne University of Technology)

Read More

EyeSeeIdentity: Exploring Natural Gaze Behaviour for Implicit User Identification...

L Yasmeen Abdrabou (Lancaster University), Mariam Hassib (Fortiss Research Institute of the Free State of Bavaria), Shuqin Hu (LMU Munich), Ken Pfeuffer (Aarhus University), Mohamed Khamis (University of Glasgow), Andreas Bulling (University of Stuttgart), Florian Alt (University of the Bundeswehr Munich)

Read More