nach oben

Erschienen in:

2018 | OriginalPaper | Buchkapitel

Program Verification in the Presence of I/O

Semantics, Verified Library Routines, and Verified Applications

verfasst von : Hugo Férée, Johannes Åman Pohjola, Ramana Kumar, Scott Owens, Magnus O. Myreen, Son Ho

Erschienen in: Verified Software. Theories, Tools, and Experiments

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

Software verification tools that build machine-checked proofs of functional correctness usually focus on the algorithmic content of the code. Their proofs are not grounded in a formal semantic model of the environment that the program runs in, or the program’s interaction with that environment. As a result, several layers of translation and wrapper code must be trusted. In contrast, the CakeML project focuses on end-to-end verification to replace this trusted code with verified code in a cost-effective manner.

In this paper, we present infrastructure for developing and verifying impure functional programs with I/O and imperative file handling. Specifically, we extend CakeML with a low-level model of file I/O, and verify a high-level file I/O library in terms of the model. We use this library to develop and verify several Unix-style command-line utilities: cat, sort, grep, diff and patch. The workflow we present is built around the HOL4 theorem prover, and therefore all our results have machine-checked proofs.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Vorheriges Kapitel Verified Certificate Checking for Counting Votes

Nächstes Kapitel TWAM: A Certifying Abstract Machine for Logic Programs

Nur mit Berechtigung zugänglich

https://hol-theorem-prover.org/.

https://cakeml.org/.

https://hol-theorem-prover.org/.

https://cakeml.org/vstte18/x86_binaries.zip.

The LCS is not always unique: both [a, c] and [b, c] are LCSes of [a, b, c] and [b, a, c].

There are algorithms that do better than quadratic time for practically interesting special cases [3]; we leave their verification for future work.

Note that this differs from the default behaviour of the GNU implementation of diff, which uses heuristics that do not compute the minimal list if doing so would be prohibitively expensive.

The verification is described in more detail in a blog post by Yannick Moy: https://blog.adacore.com/formal-verification-of-legacy-code.

@ appends lists.

Finding a termination proof for the kind of Brzozowski derivation we use is an open problem that is not addressed by Slind’s work nor by the present paper. See, e.g., Nipkow and Traytel [27] for a discussion.

Amani, S., et al.: Cogent: verifying high-assurance file system implementations. In: Conte, T., Zhou, Y. (eds.) Proceedings of the Twenty-First International Conference on Architectural Support for Programming Languages and Operating Systems, ASPLOS 2016, Atlanta, GA, USA, 2–6 April 2016, pp. 175–188. ACM (2016). https://doi.org/10.1145/2872362.2872404

Anand, A., et al.: CertiCoq: a verified compiler for Coq. In: Coq for Programming Languages (CoqPL) (2017)

Apostolico, A., Galil, Z. (eds.): Pattern Matching Algorithms. Oxford University Press, Oxford (1997)MATH

Appel, A.W.: Verified software toolchain. In: Barthe, G. (ed.) ESOP 2011. LNCS, vol. 6602, pp. 1–17. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-19718-5_1CrossRef

Arkoudas, K., Zee, K., Kuncak, V., Rinard, M.: Verifying a file system implementation. In: Davies, J., Schulte, W., Barnett, M. (eds.) ICFEM 2004. LNCS, vol. 3308, pp. 373–390. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-30482-1_32CrossRef

Bulwahn, L., Krauss, A., Haftmann, F., Erkök, L., Matthews, J.: Imperative functional programming with Isabelle/HOL. In: Mohamed, O.A., Muñoz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol. 5170, pp. 134–149. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-71067-7_14CrossRef

Charguéraud, A.: Characteristic formulae for the verification of imperative programs. In: Proceeding of the 16th ACM SIGPLAN International Conference on Functional Programming, ICFP 2011, pp. 418–430 (2011). https://doi.org/10.1145/2034773.2034828

Chlipala, A., et al.: The end of history? Using a proof assistant to replace language design with library design. In: Summit on Advances in Programming Languages (SNAPL). Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2017). https://doi.org/10.4230/LIPIcs.SNAPL.2017.3

Delaware, B., Pit-Claudel, C., Gross, J., Chlipala, A.: Fiat: deductive synthesis of abstract data types in a proof assistant. In: Principles of Programming Languages (POPL), pp. 689–700. ACM (2015). https://doi.org/10.1145/2676726.2677006

10.

Ernst, G., Schellhorn, G., Haneberg, D., Pfähler, J., Reif, W.: Verification of a virtual filesystem switch. In: Cohen, E., Rybalchenko, A. (eds.) VSTTE 2013. LNCS, vol. 8164, pp. 242–261. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-642-54108-7_13CrossRef

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_8CrossRef

12.

Glondu, S.: Vers une certification de lextraction de Coq. Ph.D. thesis, Universit Paris Diderot (2012)

13.

Guéneau, A., Myreen, M.O., Kumar, R., Norrish, M.: Verified characteristic formulae for CakeML. In: Yang, H. (ed.) ESOP 2017. LNCS, vol. 10201, pp. 584–610. Springer, Heidelberg (2017). https://doi.org/10.1007/978-3-662-54434-1_22CrossRef

14.

Heisel, M.: Specification of the Unix file system: a comparative case study. In: Alagar, V.S., Nivat, M. (eds.) AMAST 1995. LNCS, vol. 936, pp. 475–488. Springer, Heidelberg (1995). https://doi.org/10.1007/3-540-60043-4_72CrossRef

15.

Ho, S., Abrahamsson, O., Kumar, R., Myreen, M.O., Tan, Y.K., Norrish, M.: Proof-producing synthesis of CakeML with I/O and local state from monadic HOL functions. In: International Joint Conference on Automated Reasoning (IJCAR) (2018, to appear)

16.

Hobor, A.: Oracle Semantics. Princeton University, Princeton (2008)MATH

17.

IEEE Computer Society, The Open Group: The open group base specifications issue 7. IEEE Std 1003.1, 2016 Edition (2016)

18.

Jeannerod, N., Marché, C., Treinen, R.: A formally verified interpreter for a shell-like programming language. In: Paskevich, A., Wies, T. (eds.) VSTTE 2017. LNCS, vol. 10712, pp. 1–18. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-72308-2_1CrossRefMATH

19.

Khanna, S., Kunal, K., Pierce, B.C.: A formal investigation of Diff3. In: Arvind, V., Prasad, S. (eds.) FSTTCS 2007. LNCS, vol. 4855, pp. 485–496. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-77050-3_40CrossRefMATH

20.

Kumar, R., Myreen, M.O., Norrish, M., Owens, S.: CakeML: a verified implementation of ML. In: POPL 2014: Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 179–191. ACM Press, January 2014

21.

Lammich, P.: Refinement to Imperative/HOL. In: Urban, C., Zhang, X. (eds.) ITP 2015. LNCS, vol. 9236, pp. 253–269. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-22102-1_17CrossRef

22.

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_20CrossRefMATH

23.

Leroy, X.: A formally verified compiler back-end. J. Autom. Reason. 43(4), 363–446 (2009)MathSciNetCrossRef

24.

Letouzey, P.: Extraction in Coq: an overview. In: Beckmann, A., Dimitracopoulos, C., Löwe, B. (eds.) CiE 2008. LNCS, vol. 5028, pp. 359–369. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-69407-6_39CrossRef

25.

McCormick, J.W.: Building High Integrity Applications with Spark ADA. Cambridge University Press, Cambridge (2015)CrossRef

26.

Myreen, M.O., Owens, S.: Proof-producing translation of higher-order logic into pure and stateful ML. J. Funct. Program. 24(2–3), 284–315 (2014)MathSciNetCrossRef

27.

Nipkow, T., Traytel, D.: Unified decision procedures for regular expression equivalence. In: Klein, G., Gamboa, R. (eds.) ITP 2014. LNCS, vol. 8558, pp. 450–466. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-08970-6_29CrossRef

28.

Ntzik, G., Gardner, P.: Reasoning about the POSIX file system: local update and global pathnames. In: Aldrich, J., Eugster, P. (eds.) Proceedings of the 2015 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2015, part of SPLASH 2015, Pittsburgh, PA, USA, 25–30 October 2015, pp. 201–220. ACM (2015). https://doi.org/10.1145/2814270.2814306

29.

Owens, S., Reppy, J.H., Turon, A.: Regular-expression derivatives re-examined. J. Funct. Program. 19(2), 173–190 (2009). https://doi.org/10.1017/S0956796808007090MathSciNetCrossRefMATH

30.

Ridge, T., Sheets, D., Tuerk, T., Giugliano, A., Madhavapeddy, A., Sewell, P.: SibyLFS: formal specification and oracle-based testing for POSIX and real-world file systems. In: Miller, E.L., Hand, S. (eds.) Proceedings of the 25th Symposium on Operating Systems Principles, SOSP 2015, Monterey, CA, USA, 4–7 October 2015, pp. 38–53. ACM (2015). https://doi.org/10.1145/2815400.2815411

31.

Slind, K.L.: High performance regular expression processing for cross-domain systems with high assurance requirements. Presented at the Third Workshop on Formal Methods And Tools for Security (FMATS3) (2014)

32.

Swamy, N., et al.: Dependent types and multi-monadic effects in F*. In: 43rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pp. 256–270. ACM, January 2016. https://www.fstar-lang.org/papers/mumon/

33.

Tan, Y.K., Myreen, M.O., Kumar, R., Fox, A., Owens, S., Norrish, M.: A new verified compiler backend for CakeML. In: ICFP 2016: Proceedings of the 21th ACM SIGPLAN International Conference on Functional Programming, pp. 60–73. ACM Press, September 2016

34.

Kosmatov, N., Marché, C., Moy, Y., Signoles, J.: Static versus dynamic verification in Why3, Frama-C and SPARK 2014. In: Margaria, T., Steffen, B. (eds.) ISoLA 2016. LNCS, vol. 9952, pp. 461–478. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-47166-2_32CrossRef

Titel: Program Verification in the Presence of I/O
verfasst von: Hugo Férée
Johannes Åman Pohjola
Ramana Kumar
Scott Owens
Magnus O. Myreen
Son Ho
Verlag: Springer International Publishing
Buch: Verified Software. Theories, Tools, and Experiments
Print ISBN: 978-3-030-03591-4

Electronic ISBN: 978-3-030-03592-1

Copyright-Jahr: 2018
DOI: https://doi.org/10.1007/978-3-030-03592-1_6

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"