Trustworthy Systems

CakeML: A verified implementation of ML

Authors

Ramana Kumar, Magnus Myreen, Michael Norrish and Scott Owens

University of Cambridge

NICTA

University of Kent

Abstract

We have developed and mechanically verified an ML system called CakeML, which supports a substantial subset of Standard ML. CakeML is implemented as an interactive read-eval-print loop (REPL) in x86-64 machine code. Our correctness theorem ensures that, according to our model of x86-64, whatever results are printed at the REPL are permitted by the semantics of CakeML. Thus, our verification effort touches on a breadth of topics including lexing, parsing, type checking, incremental and dynamic compilation, garbage collection, arbitrary-precision arithmetic, and compiler bootstrapping.

Our contributions are twofold. The first is simply in building a system that is end-to-end verified, demonstrating that each piece of such a verification effort can in practice be composed with the others, and ensuring that none of the pieces rely on any over-simplifying assumptions. The second is developing novel approaches to some of the more challenging aspects of the verification. In particular, our formally verified compiler can bootstrap itself: we apply the verified compiler to itself to produce a verified machine-code implementation of the compiler. Additionally, our compiler proof handles diverging input programs with a lightweight approach based on logical timeout exceptions. The entire development was carried out in the HOL4 theorem prover.

BibTeX Entry

  @inproceedings{Kumar_MNO_14,
    address          = {San Diego},
    author           = {Kumar, Ramana and Myreen, Magnus and Norrish, Michael and Owens, Scott},
    booktitle        = {ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
    doi              = {10.1145/2535838.2535841},
    editor           = {{Peter Sewell}},
    keywords         = {sml, theorem-proving, verification},
    month            = jan,
    pages            = {179--191},
    paperurl         = {https://trustworthy.systems/publications/nicta_full_text/7494.pdf},
    publisher        = {ACM},
    title            = {{CakeML}: A Verified Implementation of {ML}},
    year             = {2014}
  }

Download