TY - GEN
T1 - Proving LTL Properties of Bitvector Programs and Decompiled Binaries
AU - Liu, Yuandong Cyrus
AU - Pang, Chengbin
AU - Dietsch, Daniel
AU - Koskinen, Eric
AU - Le, Ton Chanh
AU - Portokalidis, Georgios
AU - Xu, Jun
N1 - Publisher Copyright:
© 2021, Springer Nature Switzerland AG.
PY - 2021
Y1 - 2021
N2 - There is increasing interest in applying verification tools to programs that have bitvector operations. SMT solvers, which serve as a foundation for these tools, have thus increased support for bitvector reasoning through bit-blasting and linear arithmetic approximations. In this paper we show that similar linear arithmetic approximation of bitvector operations can be done at the source level through transformations. Specifically, we introduce new paths that over-approximate bitvector operations with linear conditions/constraints, increasing branching but allowing us to better exploit the well-developed integer reasoning and interpolation of verification tools. We show that, for reachability of bitvector programs, increased branching incurs negligible overhead yet, when combined with integer interpolation optimizations, enables more programs to be verified. We further show this exploitation of integer interpolation in the common case also enables competitive termination verification of bitvector programs and leads to the first effective technique for linear temporal logic (LTL) verification of bitvector programs. Finally, we provide an in-depth case study of decompiled (“lifted”) binary programs, which emulate X86 execution through frequent use of bitvector operations. We present a new tool DarkSea, the first tool capable of verifying reachability, termination and LTL of lifted binaries.
AB - There is increasing interest in applying verification tools to programs that have bitvector operations. SMT solvers, which serve as a foundation for these tools, have thus increased support for bitvector reasoning through bit-blasting and linear arithmetic approximations. In this paper we show that similar linear arithmetic approximation of bitvector operations can be done at the source level through transformations. Specifically, we introduce new paths that over-approximate bitvector operations with linear conditions/constraints, increasing branching but allowing us to better exploit the well-developed integer reasoning and interpolation of verification tools. We show that, for reachability of bitvector programs, increased branching incurs negligible overhead yet, when combined with integer interpolation optimizations, enables more programs to be verified. We further show this exploitation of integer interpolation in the common case also enables competitive termination verification of bitvector programs and leads to the first effective technique for linear temporal logic (LTL) verification of bitvector programs. Finally, we provide an in-depth case study of decompiled (“lifted”) binary programs, which emulate X86 execution through frequent use of bitvector operations. We present a new tool DarkSea, the first tool capable of verifying reachability, termination and LTL of lifted binaries.
UR - http://www.scopus.com/inward/record.url?scp=85118175295&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85118175295&partnerID=8YFLogxK
U2 - 10.1007/978-3-030-89051-3_16
DO - 10.1007/978-3-030-89051-3_16
M3 - Conference contribution
AN - SCOPUS:85118175295
SN - 9783030890506
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 285
EP - 304
BT - Programming Languages and Systems - 19th Asian Symposium, APLAS 2021, Proceedings
A2 - Oh, Hakjoo
T2 - 19th Asian Symposium on Programming Languages and Systems, APLAS 2021
Y2 - 17 October 2021 through 18 October 2021
ER -