Function Equivalence with Symbolic Execution

April 16, 2021 | 12 – 1 pm EDT | LINK

Kennon Bittick
Research Scientist – GTRI CIPHER

Cybersecurity and Privacy Virtual Lecture Series
Co-sponsored by the School of Cybersecurity and Privacy and the Institute for Information Security and Privacy


Abstract:

Summarizing and comparing basic blocks or functions across different binaries or between binary and source code has many applications for program verification including verifying compilation, source or binary transformations, identifying patched code, and identifying library functions. This talk will present IRAD research on using static symbolic execution to prove source and binary function equivalence, with a focus on how breaking up functions or basic blocks into smaller, composable units can make the analysis tractable and bypass many common issues with symbolic execution.

Speaker Bio:

Kennon Bittick is a research scientist in the Software Assurance branch of GTRI. He has been a key technical lead and performer on security analyses of enterprise and embedded systems and has expertise in manual reverse engineering and system analysis, application of enterprise-focused static and dynamic analysis techniques to the embedded domain, and hybrid human-computer software analysis. Kennon holds a Master’s Degree in Computer Science from Georgia Tech and is the principal investigator on a number of internal and sponsored research programs.