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.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
References
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
Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576–585 (1969). https://doi.org/10.1145/363235.363259
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
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
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
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
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
CompCert Project. http://compcert.inria.fr
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
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
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
Myreen, M.O.: Formal Verification of Machine-Code Programs. Ph.D. Thesis. University of Cambridge (2009). 131 p
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
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
Crary, K., Sarkar, S.: Foundational Certified Code in a Metalogical Framework. Technical report CMU-CS-03-108. Carnegie Mellon University (2003). 19 p
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
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
Freericks, M.: The nML Machine Description Formalism. Technical report TR SM-IMP/DIST/08, TU Berlin CS Department (1993). 47 p
Baudin, P., et al.: ACSL: ANSI/ISO C Specification Language. Version 1.13 (2018). 114 p
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
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
Frama-C Platform. http://frama-c.com
GCC, the GNU Compiler Collection. https://gcc.gnu.org
Tool Interface Standard (TIS) Executable and Linking Format (ELF), version 1.2 (1995)
Barrett, C., Fontaine, P., Tinelli, C.: The SMT-LIB Standard Version 2.6. Release 18 July 2017. 104 p
RISC-V Foundation. https://riscv.org
MicroTESK Framework. http://www.microtesk.org
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
GNU Binutils. https://www.gnu.org/software/binutils
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
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
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
MicroVer Project. https://forge.ispras.ru/projects/microver
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
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
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
CVC4 Solver. https://github.com/CVC4/CVC4
RISC-V GNU Compiler Toolchain. https://github.com/riscv/riscv-gnu-toolchain
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
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2020 Springer Nature Switzerland AG
About this paper
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)