GitPlanet

Cheap and reliable Node.js hosting starts at $3/month, and $1/month static HTML hosting

Created with love in Canada, visit hostnodejs.com today

Feel like to post an Ad? Learn Details
All Projects → FStarLang → Kremlin

FStarLang / Kremlin

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

Programming Languages

ocaml
1615 projects

Labels

cryptographyverification

Projects that are alternatives of or similar to Kremlin

Stp
Simple Theorem Prover, an efficient SMT solver for bitvectors
Stars: ✭ 341 (+19.65%)
Mutual labels:  cryptography, verification
Ssri
Standard Subresource Integrity library for Node.js
Stars: ✭ 69 (-75.79%)
Mutual labels:  cryptography, verification
Ed25519 Dalek
Fast and efficient ed25519 signing and verification in Rust.
Stars: ✭ 383 (+34.39%)
Mutual labels:  cryptography, verification
Hacl Star
HACL*, a formally verified cryptographic library written in F*
Stars: ✭ 1,360 (+377.19%)
Mutual labels:  cryptography, verification
Cryptominisat
An advanced SAT solver
Stars: ✭ 502 (+76.14%)
Mutual labels:  cryptography, verification
Brightid
Reference mobile app for BrightID
Stars: ✭ 101 (-64.56%)
Mutual labels:  cryptography, verification
cryptography
Cryptography course slides at Harbin Institute of Technology
Stars: ✭ 86 (-69.82%)
Mutual labels:  cryptography
Verifier
Package verifier provides simple defensive programing primitives.
Stars: ✭ 264 (-7.37%)
Mutual labels:  verification
Tangram.Bamboo
Tangram Bamboo CLI Wallet
Stars: ✭ 14 (-95.09%)
Mutual labels:  cryptography
pqcrypto
👻 Post-quantum cryptography for Python.
Stars: ✭ 15 (-94.74%)
Mutual labels:  cryptography
Riscv
RISC-V CPU Core (RV32IM)
Stars: ✭ 272 (-4.56%)
Mutual labels:  verification
Kcp Go
A Crypto-Secure, Production-Grade Reliable-UDP Library for golang with FEC
Stars: ✭ 3,177 (+1014.74%)
Mutual labels:  cryptography
My Talks
List of my talks and workshops: security engineering, applied cryptography, secure software development
Stars: ✭ 261 (-8.42%)
Mutual labels:  cryptography
flame
Flame is an ActionScript library that provides a number of useful UI controls, collections, cryptographic services, and utilities to work with the Flex SDK.
Stars: ✭ 18 (-93.68%)
Mutual labels:  cryptography
Seahorn
SeaHorn Verification Framework
Stars: ✭ 270 (-5.26%)
Mutual labels:  verification
virgil-sdk-cpp
Virgil Core SDK allows developers to get up and running with Virgil Cards Service API quickly and add end-to-end security to their new or existing digital solutions to become HIPAA and GDPR compliant and more.
Stars: ✭ 18 (-93.68%)
Mutual labels:  cryptography
Concuerror
Concuerror is a stateless model checking tool for Erlang programs.
Stars: ✭ 277 (-2.81%)
Mutual labels:  verification
interbit
To the end of servers
Stars: ✭ 23 (-91.93%)
Mutual labels:  cryptography
Mcl
a portable and fast pairing-based cryptography library
Stars: ✭ 252 (-11.58%)
Mutual labels:  cryptography
Masterkey
secure interactive password manager with xchacha20poly1305, argon2id, and Go
Stars: ✭ 271 (-4.91%)
Mutual labels:  cryptography
View All Similar Projects ➔

KreMLin

Linux Windows
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.

Trying out KreMLin

KreMLin requires OCaml (>= 4.05.0, < 4.10.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 sedlex process fix wasm.1.0.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.

File a bug if things don't work!

Documentation

The --help flag contains a substantial amount of information.

$ ./krml --help

License

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

Note that the project description data, including the texts, logos, images, and/or trademarks, for each open source project belongs to its rightful owner. If you wish to add or remove any projects, please contact us at [email protected].