Abstract
The ACSL specification language allows the verification engineer to specify almost any property they might want to verify at any given point in a given C program. For some complex properties, it can sometimes be done at the price of an extremely complex encoding, which could quickly become error-prone if written manually. To facilitate this task, a certain number of Frama-C plug-ins offer dedicated specification languages, targeting different kinds of properties, that are then translated into a set of ACSL annotations amenable to verification via the core analysis plug-ins (Eva, Wp, E-ACSL). In this chapter, we present three such plug-ins. The first of them, MetAcsl, is dedicated to pervasive properties that must be checked at each program point meeting some characteristics, for instance at each write access. A single MetAcsl annotation can thus be instantiated by a very large number of ACSL clauses. Second, RPP targets relational properties. In contrast to an ACSL function contract, which specifies what happens during a single function call, relational properties express relations over several calls of potentially different functions. Finally, Aoraï is dedicated to properties over sequences of function calls that can occur during an execution.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
- 2.
- 3.
- 4.
In the illustrative example of Fig. 10.6, the parameters are directly the vector structures. In real-life code, passing vectors by pointers would provide faster function calls.
- 5.
We assume here for simplicity that there is no arithmetic overflow inside h.
- 6.
- 7.
Recursive functions are supported by RPP likewise: during self-composition, only the calls involved in the relational property are inlined, while the recursive calls inside their bodies are not.
- 8.
Note that RPP assumes that the \(\backslash \)from clauses are correct and does not verify them. Since Wp currently does not support them, one possibility is to use MetAcsl to verify that only the provided global variables (as well as local variables) can be read by the function.
- 9.
In a future version of the tool, it is planned to use admit clauses of ACSL (see Chap. 1) to state assumptions.
- 10.
In the normalized AST of Frama-C, each function has exactly one return statement, at the end of the function (see Chap. 2).
- 11.
The full example is available in the companion repository at https://git.frama-c.com/pub/frama-c-book-companion/-/tree/main/high-level-properties.
- 12.
For the sake of clarity, the Aoraï output examples in this chapter may be given with some simplifications and reformatting.
- 13.
A limited support already exists.
References
Barthe G, Crespo JM, Kunz C (2016) Product programs and relational program logics. J Log Algebr Methods Progr. https://doi.org/10.1016/j.jlamp.2016.05.004
Barthe G, D’Argenio PR, Rezk T (2011) Secure information flow by self-composition. J Math Struct Comput Sci 21(6):1207–1252. https://doi.org/10.1017/S0960129511000193
Benton N (2004) Simple relational correctness proofs for static analyses and program transformations. In: Proceedings of the 41st symposium on principles of programming languages (POPL 2004), pp 14–25. https://doi.org/10.1145/964001.964003
Beyer D, Podelski A (2022) Software model checking: 20 years and beyond. In: Raskin JF, Chatterjee K, Doyen L, Majumdar R (eds) Principles of systems design: essays dedicated to Thomas A. Henzinger on the Occasion of his 60th Birthday, pp 554–582. Springer Nature Switzerland, Cham. https://doi.org/10.1007/978-3-031-22337-2_27
Blatter L (2019) Relational properties for specification and verification of C programs in Frama-C. PhD thesis, University Paris-Saclay. https://theses.hal.science/tel-02401884/
Blatter L, Kosmatov N, Le Gall P, Prevosto V (2017) RPP: automatic proof of relational properties by self-composition. In: Proceeding of the 23th international conference on tools and algorithms for the construction and analysis of systems (TACAS 2017), held as part of the european joint conferences on theory and practice of software (ETAPS 2017), LNCS, vol 10205, pp 391–397. Springer. https://doi.org/10.1007/978-3-662-54577-5_22
Blatter L, Kosmatov N, Le Gall P, Prevosto V, Petiot G (2018) Static and dynamic verification of relational properties on self-composed C code. In: International conference on tests and proofs (TAP), LNCS, vol 10889, pp 44–62. Springer. https://doi.org/10.1007/978-3-319-92994-1_3
Blatter L, Kosmatov N, Prevosto V, Le Gall P, The RPP plug-in manual. https://github.com/lyonel2017/Frama-C-RPP/blob/master/doc/rpp-manual.pdf
Blatter L, Kosmatov N, Prevosto V, Le Gall P (2022) Certified verification of relational properties. In: Proceedings of the 17th international conference on integrated formal methods (iFM 2022), LNCS, vol 13274, pp 86–105. Springer. https://doi.org/10.1007/978-3-031-07727-2_6
Blatter L, Kosmatov N, Prevosto V, Le Gall P (2022) An efficient VCGen-based modular verification of relational properties. In: Proceedings of the 11th international symposium on leveraging applications of formal methods, verification and validation. (ISOLA 2022), LNCS, vol 13701, pp 498–516. Springer. https://doi.org/10.1007/978-3-031-19849-6_28
Cheon Y, Perumandla A (2005) Specifying and checking method call sequences in JML. In: International conference on software engineering research and practice, pp 511–516
Cok DR (2011) OpenJML: JML for Java 7 by extending OpenJDK. In: International symposium on nasa formal methods (NFM). https://doi.org/10.1007/978-3-642-20398-5_35
Darvas A, Müller P (2006) Reasoning about method calls in JML specifications. J Object Technol 5(5):59–85
Groslambert J, Stouls N (2009) Vérification de propriétés LTL sur des programmes C par génération d’annotations. In: Approches Formelles dans l’Assistance au Développement de Logiciels (AFADL 2009). In French
Hatcliff J, Leavens GT, Leino KRM, Müller P, Parkinson M (2012) Behavioral interface specification languages. Comput Surv 44(3):16:1–16:58. https://doi.org/10.1145/2187671.2187678
Kiczales G, Lam** J, Mendhekar A, Maeda C, Lopes CV, Loingtier JM, Irwin J (1997) Aspect-oriented programming. In: European conference on object-oriented programming, LNCS, vol 1241, pp 220–242. Springer. https://doi.org/10.1007/BFb0053381
Leavens GT, Baker AL, Ruby C (1999) JML: a notation for detailed design. In: Behavioral specifications of businesses and systems, vol 523, pp 175–188. Springer. https://doi.org/10.1007/978-1-4615-5229-1_12
Leino KRM, Müller P (2008) Verification of equivalent-results methods. In: ESOP, LNCS, vol 4960, pp 307–321. https://doi.org/10.1007/978-3-540-78739-6_24
Leino KRM, Polikarpova N (2013) Verified calculations. In: Proceedings of the 5th international conference on verified software: theories, tools, experiments (VSTTE 2013), Revised selected papers, vol 8164, pp 170–190. Springer. https://doi.org/10.1007/978-3-642-54108-7_9
Leucker M, Schallhart C (2009) A brief account of runtime verification. J Log Algebr Progr 78(5):293–303
Pnueli A (1977) The temporal logic of programs. In: the 18th annual symposium on foundations of computer science (FOCS 1977), pp 46–57. IEEE Computer Society
Robles V (2022) Specifying and verifying high-level requirements on large programs: application to security of C programs. PhD thesis, University Paris-Saclay. https://theses.hal.science/tel-03626084/
Robles V, Kosmatov N, Prevosto V, Rilling L, Le Gall P (2019) MetAcsl: specification and verification of high-level properties. In: Proceedings of the 25th international conference on tools and algorithms for the construction and analysis of systems (TACAS 2019), Held as part of the European joint conferences on theory and practice of software (ETAPS 2019), LNCS, vol 11427, pp 358–364. Springer. https://doi.org/10.1007/978-3-030-17462-0_22
Robles V, Kosmatov N, Prevosto V, Rilling L, Le Gall P (2019) Tame your annotations with MetAcsl: specifying, testing and proving high-level properties. In: International conference on tests and proofs (TAP), LNCS, vol 11823, pp 167–185. Springer. https://doi.org/10.1007/978-3-030-31157-5_11
Robles V, Kosmatov N, Prevosto V, Rilling L, Le Gall P (2021) Methodology for specification and verification of high-level properties with MetAcsl. In: Proceedings of the 9th IEEE/ACM international conference on formal methods in software engineering (FormaliSE 2021), pp 54–67. IEEE. https://doi.org/10.1109/FormaliSE52586.2021.00012
Sousa M, Dillig I (2016) Cartesian Hoare logic for verifying k-safety properties. In: Proceedings of the 37th ACM SIGPLAN conference on programming language design and implementation, PLDI 2016, Santa Barbara, CA, USA, June 13–17, 2016, pp 57–69. https://doi.org/10.1145/2908080.2908092
Stouls N, Prevosto V (2023) Aoraï plug-in tutorial. https://frama-c.com/download/frama-c-aorai-manual.pdf
Trentelman K, Huisman M (2002) Extending jml specifications with temporal logic. In: International conference on algebraic methodology and software technology, LNCS, vol 2422, pp 334–348. Springer. https://doi.org/10.1007/3-540-45719-4_23
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2024 The Author(s), under exclusive license to Springer Nature Switzerland AG
About this chapter
Cite this chapter
Blatter, L., Kosmatov, N., Prevosto, V., Robles, V. (2024). Specification and Verification of High-Level Properties. In: Kosmatov, N., Prevosto, V., Signoles, J. (eds) Guide to Software Verification with Frama-C. Computer Science Foundations and Applied Logic. Springer, Cham. https://doi.org/10.1007/978-3-031-55608-1_10
Download citation
DOI: https://doi.org/10.1007/978-3-031-55608-1_10
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-031-55607-4
Online ISBN: 978-3-031-55608-1
eBook Packages: Computer ScienceComputer Science (R0)