|Number of watchers on Github||87|
|Number of open issues||67|
|Average time to close an issue||about 2 months|
|Average time to merge a PR||2 days|
|Open pull requests||5+|
|Closed pull requests||10+|
|Last commit||over 2 years ago|
|Repo Created||over 4 years ago|
|Repo Last Updated||over 2 years ago|
|Organization / Author||mitls|
|Do you use mitls-fstar? Leave a review!|
|View open issues (67)|
|View mitls-fstar activity|
|View on github|
|Fresh, new opensource launches 🚀🚀🚀|
Software engineers: It's time to get promoted. Starting NOW! Subscribe to my mailing list and I will equip you with tools, tips and actionable advice to grow in your career.
This repository contains the new F* development a port of the stable F# development to F* 0.9.
More information on miTLS can be found at www.mitls.org More information on F* can be found at www.fstar-lang.org
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
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*
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.
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.
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
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))))