×

VST-Floyd: a separation logic tool to verify correctness of C programs. (English) Zbl 1451.68169

Summary: The Verified Software Toolchain builds foundational machine-checked proofs of the functional correctness of C programs. Its program logic, Verifiable C, is a shallowly embedded higher-order separation Hoare logic which is proved sound in Coq with respect to the operational semantics of CompCert Clight. This paper introduces VST-Floyd, a verification assistant which offers a set of semiautomatic tactics helping users build functional correctness proofs for C programs using Verifiable C.

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)
03B70 Logic in computer science
68V15 Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)
PDFBibTeX XMLCite
Full Text: DOI Link

References:

[1] Affeldt, R., Marti, N.: Towards formal verification of TLS network packet processing written in C. In: Might, M., Van Horn, D., Abel, A., Sheard, T. (eds.) Proceedings of the 7th Workshop on Programming Languages Meets Program Verification, pp. 35-46. ACM (2013)
[2] Appel, AW, Verification of a cryptographic primitive: SHA-256, ACM Trans. Program. Lang. Syst., 37, 7:1-7:31, (2015) · doi:10.1145/2701415
[3] Appel, A.W., Dockins, R., Hobor, A., Beringer, L., Dodds, J., Stewart, G., Blazy, S., Leroy, X.: Program Logics for Certified Compilers. Cambridge University Press, Cambridge (2014) · Zbl 1298.68009 · doi:10.1017/CBO9781107256552
[4] Appel, AW; McAllester, D, An indexed model of recursive types for foundational proof-carrying code, ACM Trans. Program. Lang. Syst., 23, 657-683, (2001) · doi:10.1145/504709.504712
[5] Bengtson, J., Jensen, J.B., Birkedal, L.: Charge! a framework for higher-order separation logic in Coq. In: ITP, pp. 315-331 (2012) · Zbl 1360.68741
[6] Berdine, J., Calcagno, C., O’Hearn, P.W.: Symbolic execution with separation logic. In: Yi, K. (ed.) Programming Languages and Systems, Third Asian Symposium, APLAS 2005, Tsukuba, Japan, November 2-5, 2005, Proceedings, Volume 3780 of Lecture Notes in Computer Science, pp. 52-68. Springer (2005) · Zbl 1159.68363
[7] Beringer, L., Petcher, A., Ye, K.Q., Appel, A.W.: Verified correctness and security of OpenSSL HMAC. In: 24th USENIX Security Symposium, pp. 207-221. USENIX Assocation (2015)
[8] Bernstein, D.J., van Gastel, B., Janssen, W., Lange, T., Schwabe, P., Smetsers, S.: Tweetnacl: a crypto library in 100 tweets. In: Aranha, D.F., Menezes, A. (eds.) Progress in Cryptology—LATINCRYPT 2014—Third International Conference on Cryptology and Information Security in Latin America, Florianópolis, Brazil, September 17-19, 2014, Revised Selected Papers, Volume 8895 of Lecture Notes in Computer Science, pp. 64-83. Springer (2014) · Zbl 1378.94025
[9] Calcagno, C; Distefano, D; O’Hearn, P; Yang, H, Compositional shape analysis by means of bi-abduction, SIGPLAN Not., 44, 289-300, (2009) · Zbl 1315.68085 · doi:10.1145/1594834.1480917
[10] Chin, W-N; David, C; Nguyen, HH; Qin, S, Automated verification of shape, size and bag properties via user-defined predicates in separation logic, Sci. Comput. Program., 77, 1006-1036, (2012) · Zbl 1243.68148 · doi:10.1016/j.scico.2010.07.004
[11] Chlipala, A.: The Bedrock structured programming system: combining generative metaprogramming and Hoare logic in an extensible program verifier. In: ICFP’13: Proceedings of the 18th ACM SIGPLAN International Conference on Functional Programming (2013)
[12] Clarke, E.M., Kroening, D., Lerda, F.: A tool for checking ANSI-C programs. In Jensen, K., Podelski, A. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, 10th International Conference, TACAS 2004, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2004, Barcelona, Spain, March 29-April 2, 2004, Proceedings, Volume 2988 of Lecture Notes in Computer Science, pp. 168-176. Springer (2004) · Zbl 1126.68470
[13] Floyd, R.W.: Assigning meanings to programs. In: Proceedings of Symposium in Applied Mathematics, pp. 19-32. Providence, Rhode Island (1967) · Zbl 0189.50204
[14] Gruetter, S.: Improving the Coq proof automation tactics of the Verified Software Toolchain, based on a case study on verifying a C implementation of the AES encryption algorithm. Master thesis. Ecole Polytechnique Fédérale de Lausanne (2017)
[15] Guéneau, A., Myreen, M.O., Kumar, R., Norrish, M.: Verified characteristic formulae for CakeML. In: Programming Languages and Systems: 26th European Symposium on Programming, ESOP 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings, pp. 584-610. Springer, Berlin (2017) · Zbl 1485.68030
[16] Hoare, CAR, An axiomatic basis for computer programming, Commun. ACM, 12, 578-580, (1969) · Zbl 0179.23105 · doi:10.1145/363235.363259
[17] Hobor, A., Dockins, R., Appel, A.W.: A theory of indirection via approximation. In: Proceedings of the 37th Annual ACM Symposium on Principles of Programming Languages (POPL’10), pp. 171-185 (2010) · Zbl 1312.68060
[18] Hobor, A., Villard, J.: The ramifications of sharing in data structures. In: Giacobazzi, R., Cousot, R. (eds.) The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’13, Rome, Italy, January 23-25, 2013, pp. 523-536. ACM (2013) · Zbl 1301.68180
[19] Jung, R., Swasey, D., Sieczkowski, F., Svendsen, K., Turon, A., Birkedal, L., Dreyer, D.: Iris: monoids and invariants as an orthogonal basis for concurrent reasoning. In: Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (2015) · Zbl 1346.68135
[20] Kleymann, T.: Hoare logic and VDM: machine-checked soundness and completeness proofs. PhD thesis, University of Edinburgh, UK (1998)
[21] Krebbers, R.: The C standard formalized in Coq. PhD thesis, Radboud University (2015)
[22] Krebbers, R., Jung, R., Bizjak, A., Jourdan, J.-H., Dreyer, D., Birkedal, L.: The essence of higher-order concurrent separation logic. In: European Symposium on Programming, pp. 696-723. Springer (2017) · Zbl 1485.68069
[23] Krebbers, R., Timany, A., Birkedal, L.: Interactive proofs in higher-order concurrent separation logic. In: Castagna, G., Gordon, A.D. (eds.) Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017, pp. 205-217. ACM (2017) · Zbl 1380.68341
[24] Leino, K.R.M.: Dafny: An automatic program verifier for functional correctness. In: Clarke, E.M., Voronkov, A. (eds.) Logic for Programming, Artificial Intelligence, and Reasoning—16th International Conference, LPAR-16, Dakar, Senegal, April 25-May 1, 2010, Revised Selected Papers, Volume 6355 of Lecture Notes in Computer Science, pp. 348-370. Springer (2010) · Zbl 1253.68095
[25] Leroy, X, Formal verification of a realistic compiler, Commun. ACM, 52, 107-115, (2009) · doi:10.1145/1538788.1538814
[26] Mansky, W., Appel, A.W., Nogin, A.: A verified messaging system. In: Proceedings of the 2017 ACM International Conference on Object Oriented Programming Systems Languages & Applications, OOPSLA ’17. ACM (2017)
[27] Matthews, J., Moore, J.S., Ray, S., Vroon, D.: Verification condition generation via theorem proving. In: Hermann, M., Voronkov, A. (eds.) Logic for Programming, Artificial Intelligence, and Reasoning, 13th International Conference, LPAR 2006, Phnom Penh, Cambodia, November 13-17, 2006, Proceedings, Volume 4246 of Lecture Notes in Computer Science, pp. 362-376. Springer (2006) · Zbl 1165.68410
[28] Nipkow, T.: Hoare logics for recursive procedures and unbounded nondeterminism. In: Bradfield, J.C. (ed.) Computer Science Logic, 16th International Workshop, CSL 2002, 11th Annual Conference of the EACSL, Edinburgh, Scotland, UK, September 22-25, 2002, Proceedings, Volume 2471 of Lecture Notes in Computer Science, pp. 103-119. Springer (2002) · Zbl 1020.03029
[29] Reynolds, J.: Separation logic: a logic for shared mutable data structures. In: LICS 2002: IEEE Symposium on Logic in Computer Science, pp. 55-74 (2002)
[30] Signoles, J.: Foncteurs impératifs et composés: la notion de projets dans Frama-C. In: Schmitt, A. (ed.) JFLA 2009, Vingtièmes Journées Francophones des Langages Applicatifs, Saint Quentin sur Isère, France, January 31-February 3, 2009. Proceedings, Volume 7.2 of Studia Informatica Universalis, pp. 245-280 (2009)
[31] Wildmoser, M.: Verified proof carrying code. PhD thesis, Technical University Munich (2005)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.