Top

Published in:

2017 | OriginalPaper | Chapter

Verified Characteristic Formulae for CakeML

Authors : Armaël Guéneau, Magnus O. Myreen, Ramana Kumar, Michael Norrish

Published in: Programming Languages and Systems

Publisher: Springer Berlin Heidelberg

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

Abstract

Characteristic Formulae (CF) offer a productive, principled approach to generating verification conditions for higher-order imperative programs, but so far the soundness of CF has only been considered with respect to an informal specification of a programming language (OCaml). This leaves a gap between what is established by the verification framework and the program that actually runs. We present a fully-fledged CF framework for the formally specified CakeML programming language. Our framework extends the existing CF approach to support exceptions and I/O, thereby covering the full feature set of CakeML, and comes with a formally verified soundness theorem. Furthermore, it integrates with existing proof techniques for verifying CakeML programs. This validates the CF approach, and allows users to prove end-to-end theorems for higher-order imperative programs, from specification to language semantics, within a single theorem prover.

Dont have a licence yet? Then find out more about our products and how to get one now:

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!

inform now

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!

inform now

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!

inform now

previous chapter APLicative Programming with Naperian Functors

next chapter Unified Reasoning About Robustness Properties of Symbolic-Heap Separation Logic

CakeML’s module system is also supported in our CF framework, but supporting modules did not require extending the original ideas of CFML.

To be precise: Myreen and Owens [18] show that the tool can also be used for production of stateful CakeML code that maintains a hard-coded invariant over a hard-coded number of references. CF allows for much more flexibility.

We have recently switched to using strings for port names, while numbers were used previously [26] for FFI port names. Johannes Åman Pohjola made this improvement.

We would have liked to use a type variable instead of

https://static-content.springer.com/image/chp%3A10.1007%2F978-3-662-54434-1_22/442829_1_En_22_IEq185_HTML.gif

, but a type variable would have been shared between all partitions. Such sharing would need to be done across FFI partitions which goes against the design goal of local specifications and local reasoning. This is a restriction imposed by the HOL type system, which we could have avoided by using a variant of HOL with quantifiers for type variables [13].

Our use of projection functions and updates at both a concrete and abstract view of the state bears some resemblance to lenses [21]. Note however that lenses must have get and putback functions. Our set up lacks the putback functions, i.e., we only project in one direction. Our initial formalisation had a putback function, but we decided to simplify the definitions and arrived at the current solution with only a get function, which we call

https://static-content.springer.com/image/chp%3A10.1007%2F978-3-662-54434-1_22/442829_1_En_22_IEq195_HTML.gif

Anand, A., Appel, A., Morrisett, G., Paraskevopoulou, Z., Pollack, R., Belanger, O.S., Sozeau, M., Weaver, M.: CertiCoq: a verified compiler for Coq. In: The Third International Workshop on Coq for Programming Languages (CoqPL) (2017). http://conf.researchr.org/event/CoqPL-2017/main-certicoq-a-verified-compiler-for-coq

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

Bevier, W.R., Hunt Jr., W.A., Moore, J.S., Young, W.D.: An approach to systems verification. J. Autom. Reason. 5(4), 411–428 (1989). doi:10.1007/BF00243131CrossRef

Charguéraud, A.: Characteristic formulae for mechanized program verification. Ph.D. thesis, Université Paris-Diderot (2010). http://arthur.chargueraud.org/research/2010/thesis/

Charguéraud, A.: Program verification through characteristic formulae. In: Hudak, P., Weirich, S. (eds.) International Conference on Functional programming (ICFP). ACM (2010)

Charguéraud, A.: Characteristic formulae for the verification of imperative programs. In: Chakravarty, M.M.T., Hu, Z., Danvy, O. (eds.) International Conference on Functional Programming (ICFP). ACM (2011). doi:10.1145/2034773.2034828

Charguéraud, A., Pottier, F.: Machine-checked verification of the correctness and amortized complexity of an efficient union-find implementation. In: Urban, C., Zhang, X. (eds.) ITP 2015. LNCS, vol. 9236, pp. 137–153. Springer, Heidelberg (2015). doi:10.1007/978-3-319-22102-1_9CrossRef

Chen, H., Ziegler, D., Chajed, T., Chlipala, A., Kaashoek, M.F., Zeldovich, N.: Using crash hoare logic for certifying the FSCQ file system. In: Gulati, A., Weatherspoon, H. (eds.) USENIX Annual Technical Conference. USENIX Association (2016)

Chlipala, A.: The bedrock structured programming system: combining generative metaprogramming and hoare logic in an extensible program verifier. In: Morrisett, G., Uustalu, T. (eds.) International Conference on Functional Programming (ICFP). ACM (2013). http://doi.acm.org/10.1145/2500365.2500592, doi:10.1145/2500365.2500592

10.

Chlipala, A., Malecha, J.G., Morrisett, G., Shinnar, A., Wisnesky, R.: Effective interactive proofs for higher-order imperative programs. In: Hutton, G., Tolmach, A.P. (eds.) International conference on Functional programming (ICFP). ACM (2009). http://doi.acm.org/10.1145/1596550.1596565, doi:10.1145/1596550.1596565

11.

Delaware, B., Pit-Claudel, C., Gross, J., Chlipala, A.: Fiat: deductive synthesis of abstract data types in a proof assistant. In: Rajamani, S.K., Walker, D., (eds.) Principles of Programming Languages (POPL). ACM (2015). http://doi.acm.org/10.1145/2676726.2677006, doi:10.1145/2676726.2677006

12.

Greenaway, D., Lim, J., Andronick, J., Klein, G.: Don’t sweat the small stuff: formal verification of C code without the pain. In: ACM SIGPLAN Conference on Programming Language Design and Implementation, Edinburgh, UK, pp. 429–439. ACM, June 2014. doi:10.1145/2594291.2594296

13.

Homeier, P.V.: The HOL-omega logic. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 244–259. Springer, Heidelberg (2009). doi:10.1007/978-3-642-03359-9_18CrossRef

14.

Klein, G., Elphinstone, K., Heiser, G., Andronick, J., Cock, D., Derrin, P., Elkaduwe, D., Engelhardt, K., Kolanski, R., Norrish, M., Sewell, T., Tuch, H., Winwood, S.: seL4: formal verification of an OS kernel. In: ACM Symposium on Operating Systems Principles, Big Sky, MT, USA, pp. 207–220. ACM, October 2009

15.

Kumar, R., Myreen, M.O., Norrish, M., Owens, S.: CakeML: a verified implementation of ML. In: Jagannathan, S., Sewell, P. (eds.) Principles of Programming Languages (POPL) (2014). doi:10.1145/2535838.2535841

16.

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

17.

Lammich, P.: Refinement based verification of imperative data structures. In: Avigad, J., Chlipala, A. (eds.) Conference on Certified Programs (CPP). ACM (2016). http://dl.acm.org/citation.cfm?id=2854065, doi:10.1145/2854065.2854067

18.

Myreen, M.O., Owens, S.: Proof-producing translation of higher-order logic into pure and stateful ML. J. Funct. Program. 24(2-3) (2014). doi:10.1017/S0956796813000282

19.

O’Connor, L., Chen, Z., Rizkallah, C., Amani, S., Lim, J., Murray, T.C., Nagashima, Y., Sewell, T., Klein, G.: Refinement through restraint: bringing down the cost of verification. In: Garrigue, J., Keller, G., Sumii, E. (eds.) International Conference on Functional Programming (ICFP). ACM (2016). http://doi.acm.org/10.1145/2951913.2951940, doi:10.1145/2951913.2951940

20.

Owens, S., Myreen, M.O., Kumar, R., Tan, Y.K.: Functional big-step semantics. In: Thiemann, P. (ed.) ESOP 2016. LNCS, vol. 9632, pp. 589–615. Springer, Heidelberg (2016). doi:10.1007/978-3-662-49498-1_23CrossRef

21.

Pierce, B.C.: The weird world of bi-directional programming. ETAPS Invited Talk, March 2006

22.

Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: Logic in Computer Science (LICS). IEEE Computer Society (2002)

23.

Schirmer, N.: Verification of sequential imperative programs in Isabelle/HOL. Ph.D. thesis, Technische Universitat Munchen (2006). http://arthur.chargueraud.org/research/2010/thesis/

24.

Strub, P., Swamy, N., Fournet, C., Chen, J.: Self-certification: bootstrapping certified typecheckers in F* with Coq. In: Field, J., Hicks, M. (eds.) Principles of Programming Languages (POPL). ACM (2012). http://doi.acm.org/10.1145/2103656.2103723, doi:10.1145/2103656.2103723

25.

Swamy, N., Hritcu, C., Keller, C., Rastogi, A., Delignat-Lavaud, A., Forest, S., Bhargavan, K., Fournet, C., Strub, P., Kohlweiss, M., Zinzindohoue, J.K., Béguelin, S.Z.: Dependent types and multi-monadic effects in F. In: Bodík, R., Majumdar, R. (eds.) Principles of Programming Languages (POPL). ACM (2016). http://doi.acm.org/10.1145/2837614.2837655, doi:10.1145/2837614.2837655

26.

Tan, Y.K., Myreen, M.O., Kumar, R., Fox, A., Owens, S., Norrish, M.: A new verified compiler backend for CakeML. In: International Conference on Functional Programming (ICFP). ACM Press (2016)

27.

Urban, C., Zhang, X. (eds.): ITP 2015. LNCS, vol. 9236. Springer, Heidelberg (2015)

28.

Vytiniotis, D., Jones, S.L.P., Claessen, K., Rosén, D.: HALO: haskell to logic through denotational semantics. In: Giacobazzi, R., Cousot, R. (eds.) Principles of Programming Languages (POPL). ACM (2013). http://doi.acm.org/10.1145/2429069.2429121, doi:10.1145/2429069.2429121

Title: Verified Characteristic Formulae for CakeML
Authors: Armaël Guéneau
Magnus O. Myreen
Ramana Kumar
Michael Norrish
Publisher: Springer Berlin Heidelberg
Book: Programming Languages and Systems
Print ISBN: 978-3-662-54433-4

Electronic ISBN: 978-3-662-54434-1

Copyright Year: 2017
DOI: https://doi.org/10.1007/978-3-662-54434-1_22

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner