Skip to content
forked from FStarLang/karamel

KreMLin is a tool for extracting low-level F* programs to readable C code

License

Notifications You must be signed in to change notification settings

psumbera/kremlin

 
 

Repository files navigation

KreMLin

Build Status

KreMLin is a tool that extracts an F* program to readable C code. If the F* program verifies against a low-level memory model that talks about the stack and the heap; if it is first-order; if it obeys certain restrictions (e.g. non-recursive data types) then KreMLin will turn it into C.

  • DESIGN.md has a technical overview of the different transformation passes performed by KreMLin
  • MANUAL.md contains some tips&tricks when working with KreMLin.

This work has been formalized on paper. We state that the compilation of such F* programs to C preserves semantics. We start from Low*, a subset of F*, and relate its semantics to CompCert's Clight.

  • the ICFP 2017 Paper provides an overview of KreMLin as well as a paper formalization of our compilation toolchain

We have written 20,000 lines of low-level F* code, implementing the TLS 1.3 record layer. As such, KreMLin is a key component of Project Everest.

  • HACL*, our High Assurance Crypto Library, provides numerous cryptographic primitives written in F*; these primitives enjoy memory safety, functional correctness, and some degree of side-channel resistance -- they extract to C via KreMLin.

Trying out KreMLin

Make sure you run opam update first, so that by running the opam install command below you get process-0.2.1 (process version 0.2 doesn't work on Windows). Install all of the packages below, on Windows possibly following instructions from https://github.com/protz/ocaml-installer/wiki for "difficult" packages (e.g. ppx_deriving).

$ opam install ppx_deriving_yojson zarith pprint menhir ulex process fix wasm

To build just run make from this directory.

Note: KreMLin's master branch runs against F*'s stable branch, and KreMLin's fstar-master branch runs against F*'s master branch.

Note: on OSX, KreMLin is happier if you have greadlink installed (brew install coreutils).

If you have the right version of F* and fstar.exe is in your PATH then you can run the KreMLin test suite by doing make test.

File a bug if things don't work!

Documentation

The simple example from the ML Workshop Paper is available in test/ML16.fst and you can compile it with make ML16.exe.

Also check out the --help flag:

$ ./krml --help

License

Kremlin is released under the Apache 2.0 license; see LICENSE for more details.

About

KreMLin is a tool for extracting low-level F* programs to readable C code

Resources

License

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published

Languages

  • OCaml 85.0%
  • C 8.4%
  • JavaScript 3.6%
  • Makefile 1.4%
  • Standard ML 1.0%
  • Shell 0.5%
  • Batchfile 0.1%