Combining ACSL Specifications and Machine Code
https://doi.org/10.15514/ISPRAS-2018-30(4)-6
Abstract
When developing programs in high-level languages, developers have to make assumptions about the correctness of the compiler. However, this may be unacceptable for critical systems. As long as there are no full-fledged formally verified compilers, the author proposes to solve this problem by proving the correctness of the generated machine code by deductive verification. To achieve this goal, it is required to combine the pre- and postcondition specifications with the machine code behavior model. The paper presents an approach how to combine them for the case of C functions without loops. The essence of the approach is to build models, both machine code and its specifications in a single logical language, and use target processor ABI to bind machine registers with the parameters of the high-level function. For the successful implementation of this approach, you have to take a number of measures to ensure the compatibility of the high-level specification model with the machine code behavior model. Such measures include the use of a register type in the high-level specifications and the translation of the pre- and postconditions into the abstract predicates. Also in the paper the choice of logical language for building models is made and justified, the most suitable tools for implementing the approach of merging specifications are selected and the evaluation of the system of deductive verification of machine code built on the basis of the proposed approach is made using test examples obtained by compiling C programs without loops.
About the Author
P. A. Putro
National Research University Higher School of Economics
Russian Federation
Russian Federation
References
1. MicroVer – Deductive Verification Tool for Machine Code. Available at: https://forge.ispras.ru/projects/microver, accessed 20.07.2018
2. Leroy Xavier. A Formally Verified Compiler Back-end. Journal of Automated Reasoning, vol. 43, issue 4, 2009, pp 363-446
3. CompCert – The CompCert C compiler. Available at: compcert.inria.fr, accessed 13-02-2018
4. GCC Releases. Available at: http://www.gnu.org/software/gcc/releases.html, accessed 13-02-2018
5. Butterfield A., Ngondi G., Kerr A. A Dictionary of Computer Science (ed. 7), Oxford University Press, 2016, 608 p.
6. ACSL specification. Available at: http://frama-c.com/acsl.html, accessed 13-02-2018
7. Kamkin A., Tatarnikov A. MicroTESK: An ADL-Based Reconfigurable Test Program Generator for Microprocessors. In Proceedings of the 6th Spring/Summer Young Researchers’ Colloquium on Software Engineering (SYRCoSE), 2012
8. C Barrett, R Sebastiani, S Seshia, and C Tinelli. Satisfiability Modulo Theories. In Handbook of Satisfiability, vol. 185 of Frontiers in Artificial Intelligence and Applications, IOS Press, Feb. 2009, pp. 825–885
9. EREF: A Programmer’s Reference Manual for Freescale Power Architecture Processors, Rev. 1 (EIS 2.1). Available at: http://cache.freescale.com/files/32bit/doc/ref_manual/EREF_RM.pdf, accessed 13-02-2018
10. Filliâtre JC., Paskevich A. Why3 – Where Programs Meet Provers. Lecture Notes in Computer Science, vol. 7792, 2013, pp. 125-128
11. M. Mandrykin, A. Khoroshilov. A Memory Model for Deductively Verifying Linux Kernel Modules. Lecture Notes in Computer Sciences. vol. 10742, 2018, pp. 256-275
12. Florent Kirchner, Nikolai Kosmatov, Virgile Prevosto, Julien Signoles, Boris Yakobowsk. Frama-c: A Software Analysis Perspective. Formal Aspects of Computing, vol. 27, issue 3, 2015, pp 573–609
13. Jessie3 at Why3 source repository. Available at: https://gitlab.inria.fr/why3/why3/tree/master/src/jessie, accessed 12.04.2018.
14. Barrett C., Fontaine P., Tinelli C. The SMT-LIB Standard Version 2.6. Available at: http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdf, accessed 12.04.2018
15. Clark Barrett, Christopher L. Conway, Morgan Deters, Liana Hadarean, Dejan Jovanović, Tim King, Andrew Reynolds. CVC4. Lecture Notes in Computer Science, vol. 6806, 2011, pp. 171-177
16. Schoolderman M. Verifying Branch-Free Assembly Code in Why3. Lecture Notes in Computer Science, vol. 10712, 2017, pp. 66-83
17. Why3-avr project repository. Availible at: https://gitlab.science.ru.nl/sovereign/why3-avr, accessed 12.04.2018.
18. Myreen M.O.: Formal verification of machine-code programs. Ph.D. thesis, University of Cambridge, 2009
19. Konrad Slind and Michael Norrish. A brief overview of HOL4. Lecture Notes in Computer Science, vol. 5170, 2008, pp. 28-32
20. Anthony Fox. Formal specification and verification of ARM6. Lecture Notes in Computer Science, vol. 2758, 2003, pp 25-40
21. Karl Crary and Susmit Sarkar. Foundational certified code in a metalogical framework. Technical Report CMU-CS-03-108, Carnegie Mellon University, 2003.
22. Xavier 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, 2006, pp. 42-54
23. Yves Bertot. A short presentation of Coq. Lecture Notes in Computer Science, vol. 5170, 2008, pp. 12-16
24. B. Berard, M. Bidoit, A. Finkel, F. Laroussinie, A. Petit, L. Petrucci, P. Schnoebelen. Systems and Software Verification: Model-Checking Techniques and Tools. Springer, 2001, 190 p.
25. Edelman Joseph R. Machine Code Verification Using the Bogor Framework. Master Thesis, Brigham Young University, 2008
26. Bogor framework homepage. Available at: http://bogor.projects.cs.ksu.edu, accessed: 13.02.2018
Review
For citations:
Putro P.A. Combining ACSL Specifications and Machine Code. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2018;30(4):95-106. https://doi.org/10.15514/ISPRAS-2018-30(4)-6
Email this article 