Advertisement

Runtime Assertion Checking and Static Verification: Collaborative Partners

  • Fonenantsoa Maurica
  • David R. CokEmail author
  • Julien Signoles
Conference paper
First Online:
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11245)

Abstract

Runtime assertion checking aspires to a similar level of sound and complete checking of software as does static deductive verification. Furthermore, for the same source language and specification language, runtime and static checking should implement as closely as possible the same semantics. We describe here the architecture used by two different systems to achieve this goal. We accompany that with descriptions of novel designs and implementations that add new capabilities to runtime assertion checking, bringing it closer to the feature coverage of static verification.

This is a preview of subscription content, log in to check access.

Notes

Acknowledgements

This work is done in the context of project VESSEDIA, which has received funding from the European Union’s 2020 Research and Innovation Program under grant agreement No. 731453.

References

  1. 1.
    Abrial, J.-R., Hoare, A., Chapron, P.: The B-Book: Assigning Programs to Meanings. Cambridge University Press, Cambridge (1996)CrossRefGoogle Scholar
  2. 2.
    Ahrendt, W., Beckert, B., Bubel, R., Hähnle, R., Schmitt, P.H., Ulbrich, M. (eds.): Deductive Software Verification – The KeY Book. LNCS, vol. 10001. Springer, Cham (2016).  https://doi.org/10.1007/978-3-319-49812-6CrossRefGoogle Scholar
  3. 3.
    Barnes, J.: Spark: The Proven Approach to High Integrity Software. Altran Praxis, UK (2012). http://www.altran.co.uk
  4. 4.
    Barnett, M., Fähndrich, M., Leino, K.R.M., Müller, P., Schulte, W., Venter, H.: Specification and verification: the Spec# experience. Commun. ACM 54(6), 81–91 (2011)CrossRefGoogle Scholar
  5. 5.
    Barrett, C., Stump, A., Tinelli, C.: The SMT-LIB standard: version 2.0. In: Gupta, A., Kroening, D. (eds.) Proceedings of the 8th International Workshop on Satisfiability Modulo Theories (Edinburgh, England) (2010)Google Scholar
  6. 6.
    Bartocci, E., Falcone, Y., Francalanza, A., Reger, G.: Introduction to runtime verification. In: Bartocci, E., Falcone, Y. (eds.) Lectures on Runtime Verification. LNCS, vol. 10457, pp. 1–33. Springer, Cham (2018).  https://doi.org/10.1007/978-3-319-75632-5_1CrossRefGoogle Scholar
  7. 7.
    Baudin, P., et al.: ACSL: ANSI/ISO C Specification LanguageGoogle Scholar
  8. 8.
    Blazy, S., Bühler, D., Yakobowski, B.: Structuring abstract interpreters through state and value abstractions. In: Bouajjani, A., Monniaux, D. (eds.) VMCAI 2017. LNCS, vol. 10145, pp. 112–130. Springer, Cham (2017).  https://doi.org/10.1007/978-3-319-52234-0_7CrossRefzbMATHGoogle Scholar
  9. 9.
    Brahmi, A., Delmas, D., Essoussi, M.H., Randimbivololona, F., Atki, A., Marie, T.: Formalise to automate: deployment of a safe and cost-efficient process for avionics software. In: Embedded Real-Time Software and Systems (ERTS2 2018), January 2018Google Scholar
  10. 10.
    Burdy, L., et al.: An overview of JML tools and applications. In: Arts, T., Fokkink, W. (eds.) Eighth International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2003). Electronic Notes in Theoretical Computer Science (ENTCS), vol. 80, pp. 73–89. Elsevier, June 2003Google Scholar
  11. 11.
    Chalin, P.: Logical foundations of program assertions: what do practitioners want? In: Third IEEE International Conference on Software Engineering and Formal Methods (SEFM 2005), pp. 383–393 (2005)Google Scholar
  12. 12.
    Chalin, P.: A sound assertion semantics for the dependable systems evolution verifying compiler. In: International Conference on Software Engineering (ICSE 2007), pp. 23–33, May 2007Google Scholar
  13. 13.
    Cok, D.R.: Improved usability and performance of SMT solvers for debugging specifications. STTT 12, 467–481 (2010)CrossRefGoogle Scholar
  14. 14.
    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_35CrossRefGoogle Scholar
  15. 15.
    Cok, D.R.: OpenJML: software verification for Java 7 using JML, OpenJDK, and Eclipse. In: Workshop on Formal Integrated Development Environment (F-IDE 2014). EPTCS, vol. 149, pp. 79–92, 06 April 2014, Grenoble, France (2014)CrossRefGoogle Scholar
  16. 16.
    Cok, D.R., Kiniry, J.R.: ESC/Java2: uniting ESC/Java and JML. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol. 3362, pp. 108–128. Springer, Heidelberg (2005).  https://doi.org/10.1007/978-3-540-30569-9_6CrossRefGoogle Scholar
  17. 17.
    Correnson, L., Signoles, J.: Combining analyses for C program verification. In: Stoelinga, M., Pinger, R. (eds.) FMICS 2012. LNCS, vol. 7437, pp. 108–130. Springer, Heidelberg (2012).  https://doi.org/10.1007/978-3-642-32469-7_8CrossRefGoogle Scholar
  18. 18.
    Darulova, E., Kuncak, V.: Sound compilation of reals. In: The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2014, San Diego, CA, USA, 20–21 January 2014, pp. 235–248 (2014)Google Scholar
  19. 19.
    Delahaye, M., Kosmatov, N., Signoles, J.: Common specification language for static and dynamic analysis of C programs. In: Symposium on Applied Computing (SAC 2013), March 2013Google Scholar
  20. 20.
    Fähndrich, M., Barnett, M., Leijen, D., Logozzo, F.: Integrating a set of contract checking tools into visual studio. In: TOPI@ICSE (2012)Google Scholar
  21. 21.
    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_8CrossRefGoogle Scholar
  22. 22.
    Garland, S.J., Guttag, J.V.: A guide to LP, the larch prover. Technical report 82, Digital Equipment Corporation, Systems Research Center, 130 Lytton Avenue, Palo Alto, CA 94301, December 1991. Order from src-report@src.dec.comGoogle Scholar
  23. 23.
    Gowland, P., Lester, D.: A survey of exact arithmetic implementations. In: Blanck, J., Brattka, V., Hertling, P. (eds.) CCA 2000. LNCS, vol. 2064, pp. 30–47. Springer, Heidelberg (2001).  https://doi.org/10.1007/3-540-45335-0_3CrossRefGoogle Scholar
  24. 24.
    Hatcliff, J., Leavens, G.T., Leino, K.R.M., Müller, P., Parkinson, M.: Behavioral interface specification languages. Technical report CS-TR-09-01, University of Central Florida, School of EECS, Orlando, FL, March 2009Google Scholar
  25. 25.
    Jakobsson, A., Kosmatov, N., Signoles, J.: Rester statique pour devenir plus rapide, plus précis et plus mince (French). In: Journées Francophones des Langages Applicatifs, JFLA 2015, January 2015. In FrenchGoogle Scholar
  26. 26.
    Kirchner, F., Kosmatov, N., Prevosto, V., Signoles, J., Yakobowski, B.: Frama-C: a software analysis perspective. Formal Aspects Comput. 27(3), 573–609 (2015)MathSciNetCrossRefGoogle Scholar
  27. 27.
    Le, V.H., Correnson, L., Signoles, J., Wiels, V.: Verification coverage for combining test and proof. In: Dubois, C., Wolff, B. (eds.) TAP 2018. LNCS, vol. 10889, pp. 120–138. Springer, Cham (2018).  https://doi.org/10.1007/978-3-319-92994-1_7CrossRefGoogle Scholar
  28. 28.
    Leino, K.R.M.: Dafny: an automatic program verifier for functional correctness. In: Clarke, E.M., Voronkov, A. (eds.) LPAR 2010. LNCS (LNAI), vol. 6355, pp. 348–370. Springer, Heidelberg (2010).  https://doi.org/10.1007/978-3-642-17511-4_20CrossRefzbMATHGoogle Scholar
  29. 29.
    Meyer, B.: Object-oriented Software Construction. Prentice Hall, New York (1988)Google Scholar
  30. 30.
    Müller, N.T.: The iRRAM: exact arithmetic in C++. In: Blanck, J., Brattka, V., Hertling, P. (eds.) CCA 2000. LNCS, vol. 2064, pp. 222–252. Springer, Heidelberg (2001).  https://doi.org/10.1007/3-540-45335-0_14CrossRefGoogle Scholar
  31. 31.
    Petiot, G., Kosmatov, N., Botella, B., Giorgetti, A., Julliand, J.: Your proof fails? testing helps to find the reason. In: Aichernig, B.K.K., Furia, C.A.A. (eds.) TAP 2016. LNCS, vol. 9762, pp. 130–150. Springer, Cham (2016).  https://doi.org/10.1007/978-3-319-41135-4_8CrossRefGoogle Scholar
  32. 32.
    Richardson, D.: Some undecidable problems involving elementary functions of a real variable. J. Symbolic Logic 33(4), 514–520 (1968)MathSciNetCrossRefGoogle Scholar
  33. 33.
    Serebryany, K., Bruening, D., Potapenko, A., Vyukov, D.: AddressSanitizer: a fast address sanity checker. In: Annual Technical Conference (ATC 2012), June 2012Google Scholar
  34. 34.
    Seward, J., Nethercote, N.: Using valgrind to detect undefined value errors with bit-precision. In: Annual Technical Conference (ATC 2005), April 2005Google Scholar
  35. 35.
    Signoles, J.: E-ACSL: Executable ANSI/ISO C Specification Language. http://frama-c.com/download/e-acsl/e-acsl.pdf
  36. 36.
    Signoles, J., Kosmatov, N., Vorobyov, K.: E-ACSL, a runtime verification tool for safety and security of C programs. Tool paper. In: International Workshop on Competitions, Usability, Benchmarks, Evaluation, and Standardisation for Runtime Verification Tools (RV-CuBES 2017), September 2017Google Scholar
  37. 37.
    Spivey, J.M.: The Z notation: A Reference Manual. Prentice Hall International (UK) Ltd. (1992)Google Scholar
  38. 38.
    Titolo, L., Muñoz, C.A., Feliu, M.A., Moscato, M.M.: Eliminating Unstable Tests in Floating-Point Programs. ArXiv e-prints, August 2018. To appear in the proceedings of LOPSTR 2018Google Scholar
  39. 39.
    Alan Mathison Turing: On computable numbers, with an application to the entscheidungsproblem. Proc. Lond. Math. Soc. 2(1), 230–265 (1937)MathSciNetCrossRefGoogle Scholar
  40. 40.
    Vorobyov, K., Kosmatov, N., Signoles, J.: Detection of security vulnerabilities in C code using runtime verification: an experience report. In: Dubois, C., Wolff, B. (eds.) TAP 2018. LNCS, vol. 10889, pp. 139–156. Springer, Cham (2018).  https://doi.org/10.1007/978-3-319-92994-1_8CrossRefGoogle Scholar
  41. 41.
    Vorobyov, K., Signoles, J., Kosmatov, N.: Shadow state encoding for efficient monitoring of block-level properties. In: International Symposium on Memory Management (ISMM 2017), pp. 47–58, June 2017Google Scholar
  42. 42.

Copyright information

© Springer Nature Switzerland AG 2018

Authors and Affiliations

  • Fonenantsoa Maurica
    • 1
  • David R. Cok
    • 1
    Email author
  • Julien Signoles
    • 1
  1. 1.CEA, LIST, Software Safety and Security Laboratory, PC 174Gif-sur-YvetteFrance

Personalised recommendations

Cite paper

Buy options