search

project-everest / mitls-fstar

Verified implementation of TLS 1.3 in F*
https://www.mitls.org
Other
173 stars 16 forks source link

Makefile upgrade for quic2c to support (some) verification #195

Closed wintersteiger closed 6 years ago

wintersteiger commented 6 years ago

Added new "Model" flavor for verification. Replaced --lax and .checked.lax files with --admit_smt_queries true and .checked files. Successfully extracts and builds both OCaml and Kremlin flavors.

Currently still uses separate caches of .checked files for each flavor. The long-term plan is to replace them with one cache of actually verified .checked files (with few, well-controlled exceptions if absolutely necessary).

fournet commented 6 years ago

Thanks! The goal is to have nearly-identical Makefiles for all active branches of mitls-fstar, with some branch customization e.g. FLAVOR?=model for verify. We will also update https://github.com/mitls/mitls-papers/wiki/The-build-system-of-Everest once we converge on this PR.

msprotz commented 6 years ago

Note that I missed up my review and posted a mix of single-line comments and review comments... all are relevant.

wintersteiger commented 6 years ago

(All comments addressed.) The only thing open for me at this point are the prerequisites in libs/ffi and src/pki. What's the best way to build those automatically without asking the user to do it manually?

wintersteiger commented 6 years ago

@msprotz Thanks for the comments! It seems I can't comment on them this time though. Anyways, all done. I'll try to fix the OCaml dependency problem, after that we should be all set.

wintersteiger commented 6 years ago

Alright @s-zanella figured out the dependency problem, so I declare this finished! The CI runs through and correctly extracts OCaml and Kremlin flavors. All the features are there, so I'll merge now. We're now looking into ways to save and reuse the .checked files, but that will be a separate PR.