KOMPARE

As part of my master's degree in computer science, I wrote a master's thesis on KOMPARE, my work to extend the KLEE symbolic execution engine for patch verification. KOMPARE's analysis demonstrates that a patch to a program does not introduce any new bugs nor affect the program's behavior in any unintended ways.

KOMPARE symbolically executes a patched program to generate program inputs. Then, concrete executions are performed using the generated inputs on both the patched and original versions of the program. During these concrete executions, KOMPARE records and compares the externally visible outputs of the program to determine if the behaviors of the two versions match. KOMPARE additionally performs an analysis of differences between the two programs (as represented in LLVM bitcode), which is then used to direct symbolic execution towards the differences in the programs, increasing the efficiency of KOMPARE's analysis.

Links: