Architecture of a machine code deductive verification system

I. V. Gladyshev^a, A. S. Kamkin^bcad, A. M. Kotsynyak^d, P. A. Putro^da, A. V. Khoroshilov<sup>dabc

a</sup> National Research University Higher School of Economics
^b Moscow Institute of Physics and Technology (State University)
^c Lomonosov Moscow State University
^d Ivannikov Institute for System Programming of the Russian Academy of Sciences

Abstract: In recent years, ISP RAS has been developing a system for machine (binary) code deductive verification. The motivation is rather clear: modern compilers, such as GCC and Clang/LLVM, are not free of bugs; thereby, it is not superfluous (at least for safety- and security-critical components) to check the correctness of the generated code. The key feature of the suggested approach is the ability to reuse source-code-level formal specifications (pre- and postconditions, loop invariants, lemma functions, etc.) at the machine code level. The tool is highly automated: provided that the target instruction set is formalized, it disassembles the machine code, extracts its semantics, adapts the high-level specifications, and generates the verification conditions. The system utilizes a number of third-party components including a source code analyzer (Frama-C), a machine code analyzer (MicroTESK), and an SMT solver (CVC4). The modular design enables replacing one component with another when switching an input format and/or a verification engine. In this paper, we discuss the tool architecture, describe our implementation, and present a case study on verifying the memset C library function.

Keywords: formal methods, deductive verification, binary code analysis, equivalence checking, instruction set architecture, machine code, compiler testing.

DOI: 10.15514/ISPRAS-2020-32(3)-1