| Linux | Windows |
|---|---|
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.
The best way to learn about KreMLin is its work-in-progress tutorial. Pull requests and feedback are welcome!
- DESIGN.md has a technical overview of the different transformation passes performed by KreMLin, and is slightly out of date.
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.
KreMLin requires OCaml (>= 4.08.0, <= 4.12.0), OPAM, and a recent version of GNU make.
Regarding GNU make: On OSX, this may require you to install a recent GNU
make via homebrew, and invoke gmake instead of make.
Regarding OCaml: Install OPAM via your package manager, then:
$ opam install ppx_deriving_yojson zarith pprint "menhir>=20161115" sedlex process fix "wasm>=1.1.1" visitors ctypes-foreign ctypes
Next, make sure you have an up-to-date F*, and that you ran make in the
ulib/ml directory of F*. The fstar.exe executable should be on your PATH
and FSTAR_HOME should point to the directory where F* is installed.
To build just run make from this directory.
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.
KreMLin is also available on OPAM, by running opam install kremlin.
If you installed the latest version of F* through OPAM, using opam pin add fstar --dev-repo,
you can also install the most up-to-date version of KreMLin by running opam pin add kremlin --dev-repo.
File a bug if things don't work!
The --help flag contains a substantial amount of information.
$ ./krml --help
Kremlin is released under the Apache 2.0 license; see LICENSE for more details.