miTLS: A verified reference implementation of TLS
This repository contains the new F* development a port of the stable F# development to F* 0.9.
Table of contents
There are two ways to setup your build environment.
Head over to https://github.com/mitls/mitls-fstar/wiki/Setting-up-a-Docker-based-Development-environment for instructions on setup
Custom setup using Cygwin and OCaml
There are numerous dependencies. Follow the instructions at https://github.com/protz/ocaml-installer/wiki to have a working Cygwin and OCaml setup. In addition to
zarith, you will also need to install the
sqlite3 package (hint:
opam install sqlite3). To build CoreCrypto, you will need to install
libssl-dev. On Windows, you can use
opam depext ssl to install the appropriate Cygwin packages.
Once this is done, head over to https://github.com/mitls/mitls-fstar/wiki/Development-environment for some tips on our development environment, including how to attain happiness with Cygwin & Git on Windows (hopefully).
After the setup is done, check that you have the F* compiler set up and running in
git submodule update --init if you need to). Note: we do not support the F# build of F*; please use the OCaml build of F* (i.e.
make -C .fstar/src/ocaml-output).
To verify the current miTLS:
cd src/tls make all-ver -j N
where N is the number of parallel jobs to use.
To build the mitls.exe command line tool:
cd src/tls make mitls.exe ./mitls.exe -v 1.2 google.com ./mitls.exe -s 0.0.0.0 4443 & ./mitls.exe 127.0.0.1 4443
There is a script that detects if the
fstar module has changed since the last build, and rebuilds it. If you get strange errors, the script may have failed to reubild
fstar properly, and the main
Makefile keeps attempting to extract/verify using an outdated version of F*. In that case, it's a good idea to run
make -C .fstar/src/ocaml-output clean all.
tls/In-progress miTLS port. Most files have been ported and fully typecheck; others only lax typecheck or still need to be ported. The
Makefilehere has two targets that are also part of regression testing:
tls-verFull type checking of files that have been ported so far (listed in variable
tls-genOCaml code generation for files ported so far---generated files go to the
mitls.exeopenssl-like command line client and server. See
mitls.exe --helpfor details on how to use the tool.
fstar_proof/an independent POPL'16 example, verifying the state machine in F* (out of date, JK is the expert; it could be moved to FStarLang/FStar).
mipki/Antoine's development on certificate management.
flex/WIP port of flexTLS to F*
Legacy, imported from mitls-f7
apps/Sample apps built on top of miTLS --- not ported yet.
data/Persistent data used by miTLS, e.g. the OpenSSL root certificate store; sample chains for the test server; a DH parameter cache --- not ported yet.
libs/miTLS libraries; CoreCrypto and Platform had been moved to
FStarLang/FStar/contriband remaining files are deprecated, DHDB remains to be ported.
scripts/Legacy scripts for distribution-management.
tests/Legacy test suit
VS/miTLS Visual Studio solution, for browsing/building the old F# files in
src/tls-fs--- used to build as reference; currently broken.
Configuring Emacs mode
The Makefile in
src/tls has the following targets:
make <file.fst(i)>-ververifies an individual file.
make <file.fst(i)>-ingenerates command-line arguments to use with the
--inflag to verify
<file.fst(i)>. This target can be used to pass appropriate arguments in
fstar-mode.elusing this snippet:
(defun my-fstar-compute-prover-args-using-make () "Construct arguments to pass to F* by calling make." (with-demoted-errors "Error when constructing arg string: %S" (let* ((fname (file-name-nondirectory buffer-file-name)) (target (concat fname "-in")) (argstr (car (process-lines "make" "--quiet" target)))) (split-string argstr)))) (setq fstar-subp-prover-args #'my-fstar-compute-prover-args-using-make)
If you use F* for other projects that lack a Makefile with a <file.fst(i)-in> target, you may want to use some default list of command-line arguments if
make <file.fst(i)-in> fails, using, e.g.
(defun my-fstar-compute-prover-args-using-make () "Construct arguments to pass to F* by calling make." (with-demoted-errors "Error when constructing arg string: %S" (let* ((fname (file-name-nondirectory buffer-file-name)) (target (concat fname "-in")) (argstr (condition-case nil (car (process-lines "make" "--quiet" target)) (error "--debug Low")))) (split-string argstr))))