Architecture of a Machine Code Deductive Verification System
Ilya Vladimirovich GLADYSHEV,
Alexander Sergeevich KAMKIN,
Artem Mikhailovich KOTSYNYAK,
Pavel Andreevich PUTRO,
Alexey Vladimirovich KHOROSHILOV https://doi.org/10.15514/ISPRAS-2020-32(3)-1
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
Supporting agencies: The research was carried out with funding from the Ministry of Science and Higher Education of the Russian Federation (the project unique identifier is RFMEFI60719X0295).
About the Authors
Ilya Vladimirovich GLADYSHEV
National Research University Higher School of Economics
Russian Federation
Master's student studying system programming
Russian Federation
Master's student studying system programming
Alexander Sergeevich KAMKIN
Ivannikov Institute for System Programming of RAS, Moscow State University (MSU), Moscow Institute of Physics and Technology (MIPT), and Higher School of Economics (HSE)
Russian Federation
Leading researcher at the Software Engineering Department of Ivannikov Institute for System Programming of the Russian Academy of Sciences (ISP RAS). He is also a lecturer at Moscow State University (MSU), Moscow Institute of Physics and Technology (MIPT), and Higher School of Economics (HSE)
Russian Federation
Leading researcher at the Software Engineering Department of Ivannikov Institute for System Programming of the Russian Academy of Sciences (ISP RAS). He is also a lecturer at Moscow State University (MSU), Moscow Institute of Physics and Technology (MIPT), and Higher School of Economics (HSE)
Artem Mikhailovich KOTSYNYAK
Ivannikov Institute for System Programming of the Russian Academy of Sciences
Russian Federation
Junior researcher at the Software Engineering Department
Russian Federation
Junior researcher at the Software Engineering Department
Pavel Andreevich PUTRO
Ivannikov Institute for System Programming of the Russian Academy of Sciences
Russian Federation
Received a bachelor's degree in software engineering and a master’s degree in system programming from the National Research University Higher School of Economics, Moscow, Russia, works at the Ivannikov Institute for System Programming of the RAS
Russian Federation
Received a bachelor's degree in software engineering and a master’s degree in system programming from the National Research University Higher School of Economics, Moscow, Russia, works at the Ivannikov Institute for System Programming of the RAS
Alexey Vladimirovich KHOROSHILOV
Ivannikov Institute for System Programming of RAS, Moscow State University (MSU), Moscow Institute of Physics and Technology (MIPT), and Higher School of Economics (HSE)
Russian Federation
Leading Researcher, Ph.D. in Physics and Mathematics, Director of the Linux OS Verification Center at ISP RAS, Associate Professor of System Programming Departments at Moscow State University, the Higher School of Economics, and Moscow Institute of Physics and Technology
Russian Federation
Leading Researcher, Ph.D. in Physics and Mathematics, Director of the Linux OS Verification Center at ISP RAS, Associate Professor of System Programming Departments at Moscow State University, the Higher School of Economics, and Moscow Institute of Physics and Technology
References
1. R.W. Floyd. Assigning Meanings to Programs. Mathematical Aspects of Computer Science. Proceedings of Symposia in Applied Mathematics, vol. 19, 1967, pp. 19-32.
2. C.A.R. Hoare. An Axiomatic Basis for Computer Programming. Communications of the ACM, vol. 12, issue 10, 1969, pp. 576-585.
3. G. Klein, J. Andronick, K. Elphinstone, T. Murray, T. Sewell, R. Kolanski, G. Heiser. Comprehensive Formal Verification of an OS Microkernel. ACM Transactions on Computer Systems (TOCS), vol. 32, issue 1, 2014, pp. 2:1-2:70.
4. E. Cohen, W. Paul, S. Schmaltz. Theory of Multi Core Hypervisor Verification. Lecture Notes in Computer Science, vol. 7741, 2013, pp. 1-27.
5. P. Philippaerts, J.T. Mühlberg, W. Penninckx, J. Smans, B. Jacobs, F. Piessens. Software Verification with VeriFast: Industrial Case Studies. Science of Computer Programming, vol. 82, 2014, pp. 77-97.
6. D. Efremov, M. Mandrykin, A. Khoroshilov. Deductive Verification of Unmodified Linux Kernel Library Functions. Lecture Notes in Computer Science, vol. 11245, 2018, pp. 216-234.
7. D.R. Cok. OpenJML: JML for Java 7 by Extending OpenJDK. Lecture Notes in Computer Science, vol. 6617, 2011, pp. 472-479.
8. A. Kamkin, A. Khoroshilov, A. Kotsynyak, P. Putro. Deductive Binary Code Verification Against Source-Code-Level Specifications. Lecture Notes in Computer Science, vol. 12165, 2020, pp. 43-58.
9. CompCert Project. Available at: http://compcert.inria.fr, accessed 12.07.2020.
10. C. Sun, V. Le, Q. Zhang, Z. Su. Toward Understanding Compiler Bugs in GCC and LLVM. In Proc. of the International Symposium on Software Testing and Analysis (ISSTA), 2016, pp. 294-305.
11. M. Schoolderman. Verifying Branch-Free Assembly Code in Why3. Lecture Notes in Computer Science, vol. 10712, 2017, pp. 66-83.
12. J.-C. Filliˆatre, A. Paskevich. Why3 – Where Programs Meet Provers. Lecture Notes in Computer Science, vol. 7792, 2013, pp. 125-128.
13. M. Freericks. The nML Machine Description Formalism. Technical Report TR SM-IMP/DIST/08, TU Berlin CS Department, 1993, 47 p.
14. M.O. Myreen. Formal Verification of Machine-Code Programs. Ph.D. Thesis. University of Cambridge, 2009, 131 p.
15. K. Slind, M. Norrish. A Brief Overview of HOL4. Lecture Notes in Computer Science, vol. 5170, 2008, pp. 28-32. DOI: 10.1007/978-3-540-71067-7 6.
16. A. Fox. Formal Specification and Verification of ARM6. Lecture Notes in Computer Science, vol. 2758, 2003, pp. 25-40.
17. K. Crary, S. Sarkar. Foundational Certified Code in a Metalogical Framework. Technical Report CMU-CS-03-108. Carnegie Mellon University, 2003, 19 p.
18. X. Leroy. Formal Certification of a Compiler Back-End or: Programming a Compiler with a Proof Assistant. In Proc. of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of programming languages (POPL), 2006, pp. 42-54, DOI: 10.1145/1111037.1111042.
19. Y. Bertot. A Short Presentation of Coq. Lecture Notes in Computer Science, vol. 5170, 2008, pp. 12-16.
20. P. Baudin, P. Cuoq, J.-C. Filliˆatre, C. March´e, B. Monate, Y. Moy, V. Prevosto. ACSL: ANSI/ISO C Specification Language. Version 1.13, 2018, 114 p.
21. T.M.T. Nguyen, C. March´e. Hardware-Dependent Proofs of Numerical Programs. Lecture Notes in Computer Science, vol. 7086, pp. 314-329.
22. G. Barthe, T. Rezk, A. Saabas. Proof Obligations Preserving Compilation. Lecture Notes in Computer Science, vol. 3866, pp. 112-126.
23. GNU Binutils. Available at: https://www.gnu.org/software/binutils, accessed 12.07.2020
24. C. Barrett, P. Fontaine, C. Tinelli. The SMT-LIB Standard Version 2.6. Release 2017-07-18. 104 p.
25. M. Dahiya, S. Bansal. Black-Box Equivalence Checking Across Compiler Optimizations. Lecture Notes in Computer Science, vol. 10695, pp. 127-147.
26. B. Churchill, O. Padon, R. Sharma, A. Aiken. Semantic Program Alignment for Equivalence Checking. In Proc. of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), 2019, pp. 1027-1040.
27. RISC-V Foundation. Available at: https://riscv.org, accessed 12.07.2020.
28. Results of memset binary code verification. Available at: https://forge.ispras.ru/attachments/7472, accessed 12.07.2020.
29. Executable and Linkable Format (ELF. Available at: http://www.skyfree.org/linux/references/ELF Format.pdf, accessed 12.07.2020.
30. M. Chupilko, A. Kamkin, A. Kotsynyak, A. Protsenko, S. Smolov, A. Tatarnikov. Test Program Generator MicroTESK for RISC-V. In Proc. of the International Workshop on Microprocessor and SOC Test and Verification (MTV), 2018, 6 p.
31. MicroTESK Framework. Available at: http://www.microtesk.org, accessed 12.07.2020.
32. Frama-C Platform. Available at: http://frama-c.com, accessed 12.07.2020.
33. MicroVer Project. Available at: https://forge.ispras.ru/projects/microver, accessed 12.07.2020.
34. CVC4 Solver. Available at: https://github.com/CVC4/CVC4, accessed 12.07.2020.
Review
For citations:
GLADYSHEV I.V., KAMKIN A.S., KOTSYNYAK A.M., PUTRO P.A., KHOROSHILOV A.V. Architecture of a Machine Code Deductive Verification System. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2020;32(3):7-19. (In Russ.) https://doi.org/10.15514/ISPRAS-2020-32(3)-1
Email this article 