Skip to main content
SpringerLink
Log in
Book cover

International Conference on Tests and Proofs

TAP 2020: Tests and Proofs pp 43–58Cite as

Deductive Binary Code Verification Against Source-Code-Level Specifications

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 12165))

Abstract

There is a high demand in practical methods and tools to ensure total correctness of critical software components. A usual assumption is that the machine code (or binary code) generated by a compiler follows the semantics of the programming language. Unfortunately, modern compilers such as GCC and LLVM are too complex to be thoroughly verified, and bugs in the generated code are not uncommon. As an alternative approach, we suggest proving that the generated machine code still satisfies the functional properties expressed at the source code level. The suggested approach takes an ACSL-annotated C function along with its binary code and checks that the binary code meets the ACSL annotations. The main steps are as follows: (1) disassembling the machine code and extracting its semantics; (2) adapting the annotations to the machine level and generating the verification conditions. The implementation utilizes MicroTESK, Frama-C, Why3, and other tools. To illustrate the solution, we use the RISC-V microprocessor architecture; however, the approach is relatively independent of the target platform as it is based on formal specifications of the instruction set. It is worth noting that the presented method can be exploited as a test oracle for compiler testing.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

References

  1. Floyd, R.W.: Assigning meanings to programs. In: Proceedings of Symposia in Applied Mathematics, Mathematical Aspects of Computer Science, vol. 19, pp. 19–32 (1967). https://doi.org/10.1090/psapm/019/0235771

  2. Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576–585 (1969). https://doi.org/10.1145/363235.363259

    Article  MATH  Google Scholar 

  3. Klein, G., et al.: Comprehensive formal verification of an OS microkernel. ACM Trans. Comput. Syst. (TOCS) 32(1), 21–270 (2014). https://doi.org/10.1145/2560537

    Article  Google Scholar 

  4. Cohen, E., Paul, W., Schmaltz, S.: Theory of multi core hypervisor verification. In: van Emde Boas, P., Groen, F.C.A., Italiano, G.F., Nawrocki, J., Sack, H. (eds.) SOFSEM 2013. LNCS, vol. 7741, pp. 1–27. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-35843-2_1

    Chapter  Google Scholar 

  5. Philippaerts, P., Mühlberg, J.T., Penninckx, W., Smans, J., Jacobs, B., Piessens, F.: Software verification with verifast: industrial case studies. Sci. Comput. Program. 82, 77–97 (2014). https://doi.org/10.1016/j.scico.2013.01.006

    Article  Google Scholar 

  6. Efremov, D., Mandrykin, M., Khoroshilov, A.: Deductive verification of unmodified Linux kernel library functions. In: Margaria, T., Steffen, B. (eds.) ISoLA 2018. LNCS, vol. 11245, pp. 216–234. Springer, Cham (2018). https://doi.org/10.1007/978-3-030-03421-4_15

    Chapter  Google Scholar 

  7. Cok, D.R.: OpenJML: JML for Java 7 by extending OpenJDK. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 472–479. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-20398-5_35

    Chapter  Google Scholar 

  8. CompCert Project. http://compcert.inria.fr

  9. Sun, C., Le, V., Zhang, Q., Su, Z.: Toward understanding compiler bugs in GCC and LLVM. In: International Symposium on Software Testing and Analysis (ISSTA), pp. 294–305 (2016). https://doi.org/10.1145/2931037.2931074

  10. Schoolderman, M.: Verifying branch-free assembly code in Why3. In: Paskevich, A., Wies, T. (eds.) VSTTE 2017. LNCS, vol. 10712, pp. 66–83. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-72308-2_5

    Chapter  Google Scholar 

  11. Filliâtre, J.-C., Paskevich, A.: Why3—where programs meet provers. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 125–128. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-37036-6_8

    Chapter  Google Scholar 

  12. Myreen, M.O.: Formal Verification of Machine-Code Programs. Ph.D. Thesis. University of Cambridge (2009). 131 p

    Google Scholar 

  13. Slind, K., Norrish, M.: A brief overview of HOL4. In: Mohamed, O.A., Muñoz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol. 5170, pp. 28–32. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-71067-7_6

    Chapter  Google Scholar 

  14. Fox, A.: Formal specification and verification of ARM6. In: Basin, D., Wolff, B. (eds.) TPHOLs 2003. LNCS, vol. 2758, pp. 25–40. Springer, Heidelberg (2003). https://doi.org/10.1007/10930755_2

    Chapter  Google Scholar 

  15. Crary, K., Sarkar, S.: Foundational Certified Code in a Metalogical Framework. Technical report CMU-CS-03-108. Carnegie Mellon University (2003). 19 p

    Google Scholar 

  16. Leroy, X.: Formal certification of a compiler back-end or: programming a compiler with a proof assistant. In: Principles of Programming Languages (POPL), pp. 42–54 (2006). https://doi.org/10.1145/1111037.1111042

  17. Bertot, Y.: A short presentation of coq. In: Mohamed, O.A., Muñoz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol. 5170, pp. 12–16. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-71067-7_3

    Chapter  Google Scholar 

  18. Freericks, M.: The nML Machine Description Formalism. Technical report TR SM-IMP/DIST/08, TU Berlin CS Department (1993). 47 p

    Google Scholar 

  19. Baudin, P., et al.: ACSL: ANSI/ISO C Specification Language. Version 1.13 (2018). 114 p

    Google Scholar 

  20. Nguyen, T.M.T., Marché, C.: Hardware-dependent proofs of numerical programs. In: Jouannaud, J.-P., Shao, Z. (eds.) CPP 2011. LNCS, vol. 7086, pp. 314–329. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-25379-9_23

    Chapter  MATH  Google Scholar 

  21. Barthe, G., Rezk, T., Saabas, A.: Proof obligations preserving compilation. In: Dimitrakos, T., Martinelli, F., Ryan, P.Y.A., Schneider, S. (eds.) FAST 2005. LNCS, vol. 3866, pp. 112–126. Springer, Heidelberg (2006). https://doi.org/10.1007/11679219_9

    Chapter  Google Scholar 

  22. Frama-C Platform. http://frama-c.com

  23. GCC, the GNU Compiler Collection. https://gcc.gnu.org

  24. Tool Interface Standard (TIS) Executable and Linking Format (ELF), version 1.2 (1995)

    Google Scholar 

  25. Barrett, C., Fontaine, P., Tinelli, C.: The SMT-LIB Standard Version 2.6. Release 18 July 2017. 104 p

    Google Scholar 

  26. RISC-V Foundation. https://riscv.org

  27. MicroTESK Framework. http://www.microtesk.org

  28. Chupilko, M., Kamkin, A., Kotsynyak, A., Protsenko, A., Smolov, S., Tatarnikov, A.: Test Program Generator MicroTESK for RISC-V. In: International Workshop on Microprocessor and SOC Test and Verification (MTV) (2018). 6 p. https://doi.org/10.1109/MTV.2018.00011

  29. GNU Binutils. https://www.gnu.org/software/binutils

  30. Ottenstein, K., Ballance, R., MacCabe, A.: The program dependence web: a representation supporting control-, data-, and demand-driven interpretation of imperative languages. In: ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pp. 257–271 (1990). https://doi.org/10.1145/93542.93578

  31. Havlak, P.: Construction of thinned gated single-assignment form. In: Banerjee, U., Gelernter, D., Nicolau, A., Padua, D. (eds.) LCPC 1993. LNCS, vol. 768, pp. 477–499. Springer, Heidelberg (1994). https://doi.org/10.1007/3-540-57659-2_28

    Chapter  Google Scholar 

  32. Necula, G.C., McPeak, S., Rahul, S.P., Weimer, W.: CIL: intermediate language and tools for analysis and transformation of C programs. In: Horspool, R.N. (ed.) CC 2002. LNCS, vol. 2304, pp. 213–228. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-45937-5_16

    Chapter  Google Scholar 

  33. MicroVer Project. https://forge.ispras.ru/projects/microver

  34. Putro, P.A.: Applying high-level function loop invariants for machine code deductive verification. Proc. ISP RAS 31(3), 123–134 (2019). https://doi.org/10.15514/ISPRAS-2019-31(3)-10

    Article  Google Scholar 

  35. Churchill, B.R., Padon, O., Sharma, R., Aiken, A.: Semantic program alignment for equivalence checking. In: ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pp. 1027–1040 (2019). https://doi.org/10.1145/3314221.3314596

  36. Dahiya, M., Bansal, S.: Black-box equivalence checking across compiler optimizations. In: Asian Symposium on Programing Languages and Systems (APLAS), pp. 127–147 (2017). https://doi.org/10.1007/978-3-319-71237-6_7

  37. CVC4 Solver. https://github.com/CVC4/CVC4

  38. RISC-V GNU Compiler Toolchain. https://github.com/riscv/riscv-gnu-toolchain

Download references

Acknowledgment

The authors would like to thank Russian Foundation for Basic Research (RFBR). The reported study was supported by RFBR, research project No17-07-00734.

Author information

Authors and Affiliations

  1. Ivannikov Institute for System Programming of the Russian Academy of Sciences, Moscow, Russia

    Alexander Kamkin, Alexey Khoroshilov, Artem Kotsynyak & Pavel Putro

  2. Lomonosov Moscow State University, Moscow, Russia

    Alexander Kamkin & Alexey Khoroshilov

  3. Moscow Institute of Physics and Technology, Moscow, Russia

    Alexander Kamkin & Alexey Khoroshilov

  4. National Research University – Higher School of Economics, Moscow, Russia

    Alexander Kamkin, Alexey Khoroshilov & Pavel Putro

Authors
  1. Alexander Kamkin
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Alexey Khoroshilov
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Artem Kotsynyak
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Pavel Putro
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Alexander Kamkin .

Editor information

Editors and Affiliations

  1. Chalmers University of Technology, Gothenburg, Sweden

    Wolfgang Ahrendt

  2. Paderborn University, Paderborn, Germany

    Heike Wehrheim

Rights and permissions

Reprints and permissions

Copyright information

© 2020 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Kamkin, A., Khoroshilov, A., Kotsynyak, A., Putro, P. (2020). Deductive Binary Code Verification Against Source-Code-Level Specifications. In: Ahrendt, W., Wehrheim, H. (eds) Tests and Proofs. TAP 2020. Lecture Notes in Computer Science(), vol 12165. Springer, Cham. https://doi.org/10.1007/978-3-030-50995-8_3

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-50995-8_3

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-50994-1

  • Online ISBN: 978-3-030-50995-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation