Bounded Model Checking of RISC-V Machine Code with Context-Free-Language Ordered Binary Decision Diagrams

TL;DR

This paper introduces a novel approach to bounded model checking of RISC-V machine code by utilizing context-free-language ordered binary decision diagrams, aiming to improve scalability and efficiency of symbolic execution at the machine code level.

Contribution

The paper presents two new tools, rotor and bitme, that leverage CFLOBDDs and BDDs for scalable, bit-precise reasoning directly on machine code, reducing reliance on SMT solvers.

Findings

CFLOBDDs show potential for improved scalability over ADDs.

SMT solvers are less effective on complex models, but BDD-based methods speed up analysis.

Experimental results indicate promising directions for scalable machine code analysis.

Abstract

Symbolic execution is a powerful technique for analyzing the behavior of software yet scalability remains a challenge due to state explosion in control and data flow. Existing tools typically aim at managing control flow internally, often at the expense of completeness, while offloading reasoning over data flow to SMT solvers. Moreover, reasoning typically happens on source code or intermediate representation level to leverage structural information, making machine code generation part of the trust base. We are interested in changing the equation in two non-trivial ways: pushing reasoning down to machine code level, and then offloading reasoning entirely into SMT solvers and other, possibly more efficient solver technology. In more abstract terms, we are asking if bit-precise reasoning technology can be made scalable on software, and not just hardware. For this purpose, we developed two tools called rotor and bitme for model generation and bounded model checking, respectively. We chose RISC-V restricted to integer arithmetic as modeling target for rotor since RISC-V integer semantics is essentially equivalent to established SMT semantics over bitvectors and arrays of bitvectors. While state-of-the-art SMT solvers struggle in our experiments, we have evidence that there is potential for improvement. To show the potential, we have slightly generalized and then implemented in bitme two types of binary decision diagrams (BDDs): algebraic decision diagrams (ADDs) and context-free-language ordered binary decision diagrams (CFLOBDDs). Bitme uses BDDs to propagate program input through models, essentially generalizing constant propagation to domain propagation. SMT solvers only get involved when model input cannot be propagated, significanly speeding up SMT solving. We then study the impact on state explosion of CFLOBDDs, which are potentially more scalable than ADDs.