Are you happy with your logging solution? Would you help us out by taking a 30-second survey? Click here

mitls-fstar

TLS implemented in F*

Subscribe to updates I use mitls-fstar


Statistics on mitls-fstar

Number of watchers on Github 87
Number of open issues 67
Average time to close an issue about 2 months
Main language F#
Average time to merge a PR 2 days
Open pull requests 5+
Closed pull requests 10+
Last commit over 1 year ago
Repo Created almost 4 years ago
Repo Last Updated over 1 year ago
Size 20.3 MB
Organization / Authormitls
Contributors9
Page Updated
Do you use mitls-fstar? Leave a review!
View open issues (67)
View mitls-fstar activity
View on github
Fresh, new opensource launches 🚀🚀🚀
Trendy new open source projects in your inbox! View examples

Subscribe to our mailing list

Evaluating mitls-fstar for your project? Score Explanation
Commits Score (?)
Issues & PR Score (?)

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.

Build Status
Windows CI
Windows Nightly
Linux CI
Linux Nightly

miTLS website

More information on miTLS can be found at www.mitls.org More information on F* can be found at www.fstar-lang.org

Table of contents

Building

There are two ways to setup your build environment.

Using Docker

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 ocamlfind, batteries, stdint, and 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 .fstar (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

Caveats:

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.

Directory structure

  • src/

    • tls/ In-progress miTLS port. Most files have been ported and fully typecheck; others only lax typecheck or still need to be ported. The Makefile here has two targets that are also part of regression testing:
    • tls-ver Full type checking of files that have been ported so far (listed in variable VERIFY)
    • tls-gen OCaml code generation for files ported so far---generated files go to the output/ directory
    • mitls.exe openssl-like command line client and server. See mitls.exe --help for 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/contrib and remaining files are deprecated, DHDB remains to be ported.

    • fst F* specification
    • fs F# implementation
    • ml OCaml implementation
  • 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)>-ver verifies an individual file.
  • make <file.fst(i)>-in generates command-line arguments to use with the --in flag to verify <file.fst(i)>. This target can be used to pass appropriate arguments in fstar-mode.el using 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 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))))
mitls-fstar open issues Ask a question     (View All Issues)
  • almost 3 years C extraction from Dafny/Spartan for RSA
  • almost 3 years Crypto integration between miTLS and Spartan/Dafny extracted code
  • almost 3 years Verified crypto and Everest integration
  • almost 3 years Verified crypto algorithms
  • almost 3 years Testing Infrastructure
  • almost 3 years Improve CI
  • about 3 years Add an API to retrieve the server certificate after a TLS handshake completes
  • about 3 years Support TLS token binding
  • about 3 years Support SRTP (Secure Real-time Transport) - RFC 3711
  • about 3 years Support ALPN (Application Layer Protocol Negotation)
  • about 3 years Verified Record Layer
  • about 3 years 0-RTT and 0.5 RTT focus as part of Record layer
  • about 3 years PRF, MAC, and AEAD idealization
  • about 3 years Mathematical functional correctness of AES GCM
  • about 3 years libcurl integrated with TLS, Crypto code
  • about 3 years Side channel protection
  • about 3 years Review of ChaCha+Poly idealization
  • about 3 years Fix algorithm negotiation
  • about 3 years constant time implementation in C?
  • about 3 years Spartan: Create a build process for the crypto code
  • about 3 years Regenerate hints during nightly builds
  • about 3 years Add test suites for builds
  • about 3 years Add build versioning and archiving
  • about 3 years Implement TLS Encrypt-then-mac
  • about 3 years C extraction from Dafny for SHA, AES and RSA
  • about 3 years ECC in F*
  • about 3 years SHA in F*
  • about 3 years Implementation of AES GCM in Dafny/Spartan
  • about 3 years RSA implementation in Dafny/Spartan
  • about 3 years Improve build system
mitls-fstar open pull requests (View All Pulls)
  • Add FFI wrappers to support curl
  • Has eq impl
  • Updated negotiation logic
  • More nginx changes
  • Restructuring of wire-format modules towards QD integration
mitls-fstar list of languages used
Other projects in F#