Skip to content
Flexible and Constant Time Programming Language
OCaml C Standard ML Shell Dockerfile Makefile
Branch: master
Clone or download
Latest commit 3de0124 Jun 23, 2019
Permalink
Type Name Latest commit message Commit time
Failed to load latest commit information.
Unity @ 994779f change `Private` to `Secret` Jan 18, 2017
docker produces factc instead of fact.byte Feb 20, 2019
example example dir Feb 22, 2019
src
test syntax in failing test Jun 5, 2019
.gitattributes oops Apr 15, 2018
.gitignore produces factc instead of fact.byte Feb 20, 2019
.gitmodules
.merlin
FaCT_extended.pdf extended paper Apr 17, 2019
LICENSE Create LICENSE Mar 19, 2018
Makefile better make command Feb 22, 2019
README.md
_oasis produces factc instead of fact.byte Feb 20, 2019
_tags produce native binaries Feb 20, 2019
guidelines.md cleanup repo files May 8, 2018
myocamlbuild.ml WIP: add optimization checker Dec 30, 2017
ocamlswitch.txt installed z3 Sep 13, 2018

README.md

FaCT

This is the compiler for the Flexible and Constant Time cryptographic programming language. FaCT is a domain-specific language that aids you in writing constant-time code for cryptographic routines that need to be free from timing side channels.

Useful links:

Building

To build the compiler, you can either build from source or download a pre-built release. We recommend building from source if possible.

Virtual machine image

You can download a VM image pre-configured for building the FaCT compiler and case studies. The file fact.ova should have a SHA256 sum of 089398c85c5074d911c2f2b67ca22df453235e8733f1eb283c71717cf70f714c.

Using Docker

If you have docker installed, you can load our docker image with the build environment already installed:

cd docker/
./run.sh

Once inside the docker shell, run the following to finish setting up the environment:

cd FaCT/
eval $(opam config env)

Setting up the build environment

FaCT is developed using OCaml 4.06.0 and LLVM 6.0.

Using a local environment

Building FaCT has been tested on Ubuntu 16.04, 18.04, and macOS.

1. Install System Dependencies

Ubuntu (16.04 & 18.04)

sudo apt install llvm-6.0 clang-6.0 cmake libgmp-dev m4 pkg-config

macOS

These instructions require Homebrew

brew install cmake gmp m4 pkg-config
brew install llvm@6 --with-toolchain

Note: This does not put the proper version of clang on your PATH. You will need to run:

export PATH="$(brew --prefix llvm@6)/bin:$PATH"

2. Install OCaml + packages

We recommend installing the opam package manager to manage OCaml and package dependencies:

sh <(curl -sL https://raw.githubusercontent.com/ocaml/opam/master/shell/install.sh)

Then, install OCaml and the libraries:

opam init
eval $(opam config env)
opam switch create 4.06.0
eval $(opam config env)
opam switch import ocamlswitch.txt

Finally, make sure the Z3 lib is available to the OCaml compiler:

export LD_LIBRARY_PATH="$HOME/.opam/4.06.0/lib/z3:$LD_LIBRARY_PATH"

3. Configure Paths

The FaCT compiler depends on the LLVM 6.0 toolchain at runtime, and expects binaries with -6.0 suffixes. Ensure that clang-6.0 is in your PATH:

clang-6.0 --version

Compiling FaCT

You can now build the compiler:

oasis setup
make

This will produce the factc executable.

Usage

Basic Usage

Run ./factc <source files> to compile a FaCT program.

Link to a C library

FaCT is designed to be called from C code. Compiling FaCT source files will output an object file, which can then be linked to a C file. As an example:

cd example/
../factc -generate-header example.fact
clang-6.0 -c main.c
clang-6.0 -o final main.o example.o

You can then run the executable:

./final

Debugging

Many debugging options and intermediate data structures are available. Run ./factc -help for all options.

Acknowledgements

We thank the anonymous PLDI and PLDI AEC reviewers for their suggestions and insightful comments.

You can’t perform that action at this time.