diff --git a/.ci/corecryptotest_reduce_keysize.sh b/.ci/corecryptotest_reduce_keysize.sh index 4439c2c77e0..a8e1de9a86c 100755 --- a/.ci/corecryptotest_reduce_keysize.sh +++ b/.ci/corecryptotest_reduce_keysize.sh @@ -2,8 +2,8 @@ set -e # For CI, use keysize_small -sed -i.bak 's/let keysize = keysize_large/let keysize = keysize_small/' ucontrib/CoreCrypto/ml/Tests.ml -sed -i.bak 's/let dh_param_size = dh_param_size_large/let dh_param_size = dh_param_size_small/' ucontrib/CoreCrypto/ml/Tests.ml +sed -i.bak 's/let keysize = keysize_large/let keysize = keysize_small/' contrib/CoreCrypto/ml/Tests.ml +sed -i.bak 's/let dh_param_size = dh_param_size_large/let dh_param_size = dh_param_size_small/' contrib/CoreCrypto/ml/Tests.ml -# We leave ucontrib/CoreCrypto/ml/Tests.ml modified, unstaged. +# We leave contrib/CoreCrypto/ml/Tests.ml modified, unstaged. # The CI teardown will forget this happened. diff --git a/.docker/emacs/.emacs b/.docker/emacs/.emacs index 1ead729e348..6b125082a2d 100644 --- a/.docker/emacs/.emacs +++ b/.docker/emacs/.emacs @@ -8,14 +8,14 @@ ;;set fstar includes, these should work for most tutorial examples, except those using hyperheap -(setq fstar-subp-prover-args '("--include" "/home/build/FStar/ucontrib/Platform/fst" "--include" "/home/build/FStar/ucontrib/CoreCrypto/fst")) +(setq fstar-subp-prover-args '("--include" "/home/build/FStar/contrib/Platform/fst" "--include" "/home/build/FStar/contrib/CoreCrypto/fst")) ;;this is what the above corresponds to on the command line: -;fstar --include /home/FStar/FStar/ucontrib/Platform/fst --include /home/FStar/FStar/ucontrib/CoreCrypto/fst +;fstar --include /home/FStar/FStar/contrib/Platform/fst --include /home/FStar/FStar/contrib/CoreCrypto/fst ;;set fstar includes, these work for the the Encrypt-then-MAC example: -;(setq fstar-subp-prover-args '("--include" "/home/FStar/FStar/ulib/hyperheap" "--include" "/home/FStar/FStar/ucontrib/Platform/fst" "--include" "/home/FStar/FStar/ucontrib/CoreCrypto/fst")) +;(setq fstar-subp-prover-args '("--include" "/home/FStar/FStar/ulib/hyperheap" "--include" "/home/FStar/FStar/contrib/Platform/fst" "--include" "/home/FStar/FStar/contrib/CoreCrypto/fst")) ;;this is what the above corresponds to on the command line: -;fstar --include /home/FStar/FStar/ulib/hyperheap --include /home/FStar/FStar/ucontrib/Platform/fst --include /home/FStar/FStar/ucontrib/CoreCrypto/fst +;fstar --include /home/FStar/FStar/ulib/hyperheap --include /home/FStar/FStar/contrib/Platform/fst --include /home/FStar/FStar/contrib/CoreCrypto/fst diff --git a/.nix/fstar.nix b/.nix/fstar.nix index 49d1a6db252..5ef0a34bd22 100644 --- a/.nix/fstar.nix +++ b/.nix/fstar.nix @@ -12,7 +12,7 @@ stdenv.mkDerivation { "doc.*" "examples.*" "src(/ocaml-output(/Makefile)?)?" - "ucontrib.*" + "contrib.*" "mk.*" ]; diff --git a/CHANGES.md b/CHANGES.md index 130ee9fab38..f5c122285db 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -872,7 +872,7 @@ Date: Mon Apr 30 16:57:21 2018 -0700 abstract alias for a 21 bit integer represented within a FStar.UInt32.t. -* ucontrib/Platform/fst/*: These modules are deprecated. Their +* contrib/Platform/fst/*: These modules are deprecated. Their functionality is now moved to FStar.Bytes, FStar.Error, FStar.Tcp, FStar.Udp, and FStar.Date. diff --git a/ucontrib/CoreCrypto/INSTALL.md b/contrib/CoreCrypto/INSTALL.md similarity index 100% rename from ucontrib/CoreCrypto/INSTALL.md rename to contrib/CoreCrypto/INSTALL.md diff --git a/contrib/CoreCrypto/fst/CoreCrypto.fst b/contrib/CoreCrypto/fst/CoreCrypto.fst index 7291e4fea51..05dfaf2afb3 100644 --- a/contrib/CoreCrypto/fst/CoreCrypto.fst +++ b/contrib/CoreCrypto/fst/CoreCrypto.fst @@ -15,9 +15,7 @@ *) module CoreCrypto -open FStar.Bytes - -assume val now: unit -> EXT UInt32.t +open Platform.Bytes (* ------------ Hashing ------------ *) type hash_alg = @@ -62,7 +60,40 @@ let blockSize = function | AES_128_CBC -> 16 | AES_256_CBC -> 16 -include CryptoTypes +(* Authenticated Encryption for TLS. + Note that their AAD contents depends on the protocol version. *) + +type aead_cipher = + | AES_128_GCM + | AES_256_GCM + | CHACHA20_POLY1305 + | AES_128_CCM // "Counter with CBC-Message Authentication Code" + | AES_256_CCM + | AES_128_CCM_8 // variant with truncated 8-byte tags + | AES_256_CCM_8 + +// the key materials consist of an encryption key, a static IV, and an authentication key. + +let aeadKeySize = function + | AES_128_CCM -> 16 + | AES_128_CCM_8 -> 16 + | AES_128_GCM -> 16 + | AES_256_CCM -> 32 + | AES_256_CCM_8 -> 32 + | AES_256_GCM -> 32 + | CHACHA20_POLY1305 -> 32 + +let aeadRealIVSize (a:aead_cipher) = 12 + +// the ciphertext ends with an authentication tag +let aeadTagSize = function + | AES_128_CCM_8 -> 8 + | AES_256_CCM_8 -> 8 + | AES_128_CCM -> 16 + | AES_256_CCM -> 16 + | AES_128_GCM -> 16 + | AES_256_GCM -> 16 + | CHACHA20_POLY1305 -> 16 //16-09-12 added precise concrete spec, matching what we implement in low-level/crypto //16-09-12 for robustness, we should at least test it when using external crypto. @@ -134,11 +165,7 @@ assume val stream_decryptor : stream_cipher -> bytes -> EXT cipher_stream assume val stream_process : cipher_stream -> bytes -> EXT bytes assume val stream_fini : cipher_stream -> EXT unit -assume val init : unit -> EXT int -assume val zero : l:nat -> EXT (lbytes l) assume val random : l:nat -> EXT (lbytes l) -assume val random32 : l:UInt32.t -> EXT (lbytes32 l) -// 18-02-25 we should probably keep just the latter assume val rsa_gen_key : int -> EXT (k:rsa_key{Some? k.rsa_prv_exp}) assume val rsa_encrypt : rsa_key -> rsa_padding -> bytes -> EXT bytes @@ -198,7 +225,7 @@ assume val ec_gen_key: p:ec_params length k.ec_point.ecx = ec_bytelen k.ec_params.curve /\ length k.ec_point.ecy = ec_bytelen k.ec_params.curve}) -//TODO: keep also abstract OpenSSL representation for efficiency? +//TODO: keep also abtsract OpenSSL representation for efficiency? type key = | KeyRSA of rsa_key | KeyDSA of dsa_key diff --git a/ucontrib/CoreCrypto/fst/CoreCrypto.fst.hints b/contrib/CoreCrypto/fst/CoreCrypto.fst.hints similarity index 100% rename from ucontrib/CoreCrypto/fst/CoreCrypto.fst.hints rename to contrib/CoreCrypto/fst/CoreCrypto.fst.hints diff --git a/contrib/CoreCrypto/fst/CryptoTypes.fst b/contrib/CoreCrypto/fst/CryptoTypes.fst deleted file mode 100644 index da38493d2fc..00000000000 --- a/contrib/CoreCrypto/fst/CryptoTypes.fst +++ /dev/null @@ -1,50 +0,0 @@ -(* - Copyright 2008-2018 Microsoft Research - - Licensed under the Apache License, Version 2.0 (the "License"); - you may not use this file except in compliance with the License. - You may obtain a copy of the License at - - http://www.apache.org/licenses/LICENSE-2.0 - - Unless required by applicable law or agreed to in writing, software - distributed under the License is distributed on an "AS IS" BASIS, - WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. - See the License for the specific language governing permissions and - limitations under the License. -*) -(* Some type definitions for F* programs that extract to OCaml and then wish to - * use LowCProvider. *) -module CryptoTypes - -type aead_cipher = - | AES_128_GCM - | AES_256_GCM - | CHACHA20_POLY1305 - | AES_128_CCM // "Counter with CBC-Message Authentication Code" - | AES_256_CCM - | AES_128_CCM_8 // variant with truncated 8-byte tags - | AES_256_CCM_8 - -// the key materials consist of an encryption key, a static IV, and an authentication key. - -let aeadKeySize = function - | AES_128_CCM -> 16 - | AES_128_CCM_8 -> 16 - | AES_128_GCM -> 16 - | AES_256_CCM -> 32 - | AES_256_CCM_8 -> 32 - | AES_256_GCM -> 32 - | CHACHA20_POLY1305 -> 32 - -let aeadRealIVSize (a:aead_cipher) = 12 - -// the ciphertext ends with an authentication tag -let aeadTagSize = function - | AES_128_CCM_8 -> 8 - | AES_256_CCM_8 -> 8 - | AES_128_CCM -> 16 - | AES_256_CCM -> 16 - | AES_128_GCM -> 16 - | AES_256_GCM -> 16 - | CHACHA20_POLY1305 -> 16 diff --git a/contrib/CoreCrypto/fst/DHDB.fst b/contrib/CoreCrypto/fst/DHDB.fst index 506afe1dd0f..6a1c5542caf 100644 --- a/contrib/CoreCrypto/fst/DHDB.fst +++ b/contrib/CoreCrypto/fst/DHDB.fst @@ -17,14 +17,14 @@ module DHDB open Platform.Bytes open CoreCrypto -type key = bytes * bytes // p, g -type value = bytes * bool // q, safe_prime? +type key = bytes & bytes // p, g +type value = bytes & bool // q, safe_prime? assume new type dhdb : Type0 assume val defaultFileName: string assume val defaultDHPrimeConfidence: int -assume val defaultPQMinLength: nat * nat +assume val defaultPQMinLength: nat & nat assume val create: string -> dhdb assume val select: dhdb -> key -> option value @@ -33,6 +33,6 @@ assume val remove: dhdb -> key -> dhdb assume val keys : dhdb -> list key assume val merge : dhdb -> string -> dhdb -assume val dh_check_params: dhdb -> int -> (int * int) -> bytes -> bytes -> option (dhdb * dh_params) +assume val dh_check_params: dhdb -> int -> (int & int) -> bytes -> bytes -> option (dhdb & dh_params) assume val dh_check_element: dh_params -> bytes -> bool -assume val load_default_params: string -> dhdb -> (int * int) -> (dhdb * dh_params) +assume val load_default_params: string -> dhdb -> (int & int) -> (dhdb & dh_params) diff --git a/ucontrib/CoreCrypto/fst/DHDB.fst.hints b/contrib/CoreCrypto/fst/DHDB.fst.hints similarity index 100% rename from ucontrib/CoreCrypto/fst/DHDB.fst.hints rename to contrib/CoreCrypto/fst/DHDB.fst.hints diff --git a/ucontrib/CoreCrypto/ml/.gitignore b/contrib/CoreCrypto/ml/.gitignore similarity index 100% rename from ucontrib/CoreCrypto/ml/.gitignore rename to contrib/CoreCrypto/ml/.gitignore diff --git a/ucontrib/CoreCrypto/ml/CoreCrypto.ml b/contrib/CoreCrypto/ml/CoreCrypto.ml similarity index 100% rename from ucontrib/CoreCrypto/ml/CoreCrypto.ml rename to contrib/CoreCrypto/ml/CoreCrypto.ml diff --git a/ucontrib/CoreCrypto/ml/CoreCrypto.mli b/contrib/CoreCrypto/ml/CoreCrypto.mli similarity index 100% rename from ucontrib/CoreCrypto/ml/CoreCrypto.mli rename to contrib/CoreCrypto/ml/CoreCrypto.mli diff --git a/ucontrib/CoreCrypto/ml/DHDB.ml b/contrib/CoreCrypto/ml/DHDB.ml similarity index 100% rename from ucontrib/CoreCrypto/ml/DHDB.ml rename to contrib/CoreCrypto/ml/DHDB.ml diff --git a/ucontrib/CoreCrypto/ml/Makefile b/contrib/CoreCrypto/ml/Makefile similarity index 100% rename from ucontrib/CoreCrypto/ml/Makefile rename to contrib/CoreCrypto/ml/Makefile diff --git a/ucontrib/CoreCrypto/ml/Tests.ml b/contrib/CoreCrypto/ml/Tests.ml similarity index 100% rename from ucontrib/CoreCrypto/ml/Tests.ml rename to contrib/CoreCrypto/ml/Tests.ml diff --git a/ucontrib/CoreCrypto/ml/db/DB.ml b/contrib/CoreCrypto/ml/db/DB.ml similarity index 100% rename from ucontrib/CoreCrypto/ml/db/DB.ml rename to contrib/CoreCrypto/ml/db/DB.ml diff --git a/ucontrib/CoreCrypto/ml/db/DB.mli b/contrib/CoreCrypto/ml/db/DB.mli similarity index 100% rename from ucontrib/CoreCrypto/ml/db/DB.mli rename to contrib/CoreCrypto/ml/db/DB.mli diff --git a/ucontrib/CoreCrypto/ml/db/DBMap.ml b/contrib/CoreCrypto/ml/db/DBMap.ml similarity index 100% rename from ucontrib/CoreCrypto/ml/db/DBMap.ml rename to contrib/CoreCrypto/ml/db/DBMap.ml diff --git a/ucontrib/CoreCrypto/ml/db/DBMap.mli b/contrib/CoreCrypto/ml/db/DBMap.mli similarity index 100% rename from ucontrib/CoreCrypto/ml/db/DBMap.mli rename to contrib/CoreCrypto/ml/db/DBMap.mli diff --git a/ucontrib/CoreCrypto/ml/db/Makefile b/contrib/CoreCrypto/ml/db/Makefile similarity index 100% rename from ucontrib/CoreCrypto/ml/db/Makefile rename to contrib/CoreCrypto/ml/db/Makefile diff --git a/ucontrib/CoreCrypto/ml/dsaparam.pem b/contrib/CoreCrypto/ml/dsaparam.pem similarity index 100% rename from ucontrib/CoreCrypto/ml/dsaparam.pem rename to contrib/CoreCrypto/ml/dsaparam.pem diff --git a/ucontrib/CoreCrypto/ml/openssl_stub.c b/contrib/CoreCrypto/ml/openssl_stub.c similarity index 100% rename from ucontrib/CoreCrypto/ml/openssl_stub.c rename to contrib/CoreCrypto/ml/openssl_stub.c diff --git a/ucontrib/CoreCrypto/ml/pki/CAFile.pem b/contrib/CoreCrypto/ml/pki/CAFile.pem similarity index 100% rename from ucontrib/CoreCrypto/ml/pki/CAFile.pem rename to contrib/CoreCrypto/ml/pki/CAFile.pem diff --git a/ucontrib/CoreCrypto/ml/pki/Makefile b/contrib/CoreCrypto/ml/pki/Makefile similarity index 100% rename from ucontrib/CoreCrypto/ml/pki/Makefile rename to contrib/CoreCrypto/ml/pki/Makefile diff --git a/ucontrib/CoreCrypto/ml/pki/config/ca.config b/contrib/CoreCrypto/ml/pki/config/ca.config similarity index 100% rename from ucontrib/CoreCrypto/ml/pki/config/ca.config rename to contrib/CoreCrypto/ml/pki/config/ca.config diff --git a/ucontrib/CoreCrypto/ml/pki/dsa/certificates/ca.crt b/contrib/CoreCrypto/ml/pki/dsa/certificates/ca.crt similarity index 100% rename from ucontrib/CoreCrypto/ml/pki/dsa/certificates/ca.crt rename to contrib/CoreCrypto/ml/pki/dsa/certificates/ca.crt diff --git a/ucontrib/CoreCrypto/ml/pki/dsa/certificates/ca.key b/contrib/CoreCrypto/ml/pki/dsa/certificates/ca.key similarity index 100% rename from ucontrib/CoreCrypto/ml/pki/dsa/certificates/ca.key rename to contrib/CoreCrypto/ml/pki/dsa/certificates/ca.key diff --git a/ucontrib/CoreCrypto/ml/pki/dsa/certificates/dh.pem b/contrib/CoreCrypto/ml/pki/dsa/certificates/dh.pem similarity index 100% rename from ucontrib/CoreCrypto/ml/pki/dsa/certificates/dh.pem rename to contrib/CoreCrypto/ml/pki/dsa/certificates/dh.pem diff --git a/ucontrib/CoreCrypto/ml/pki/dsa/certificates/dsa.cert.mitls.org.crt b/contrib/CoreCrypto/ml/pki/dsa/certificates/dsa.cert.mitls.org.crt similarity index 100% rename from ucontrib/CoreCrypto/ml/pki/dsa/certificates/dsa.cert.mitls.org.crt rename to contrib/CoreCrypto/ml/pki/dsa/certificates/dsa.cert.mitls.org.crt diff --git a/ucontrib/CoreCrypto/ml/pki/dsa/certificates/dsa.cert.mitls.org.csr b/contrib/CoreCrypto/ml/pki/dsa/certificates/dsa.cert.mitls.org.csr similarity index 100% rename from ucontrib/CoreCrypto/ml/pki/dsa/certificates/dsa.cert.mitls.org.csr rename to contrib/CoreCrypto/ml/pki/dsa/certificates/dsa.cert.mitls.org.csr diff --git a/ucontrib/CoreCrypto/ml/pki/dsa/certificates/dsa.cert.mitls.org.key b/contrib/CoreCrypto/ml/pki/dsa/certificates/dsa.cert.mitls.org.key similarity index 100% rename from ucontrib/CoreCrypto/ml/pki/dsa/certificates/dsa.cert.mitls.org.key rename to contrib/CoreCrypto/ml/pki/dsa/certificates/dsa.cert.mitls.org.key diff --git a/ucontrib/CoreCrypto/ml/pki/dsa/certificates/dsa.cert.mitls.org.p12 b/contrib/CoreCrypto/ml/pki/dsa/certificates/dsa.cert.mitls.org.p12 similarity index 100% rename from ucontrib/CoreCrypto/ml/pki/dsa/certificates/dsa.cert.mitls.org.p12 rename to contrib/CoreCrypto/ml/pki/dsa/certificates/dsa.cert.mitls.org.p12 diff --git a/ucontrib/CoreCrypto/ml/pki/dsa/certificates/dsap.pem b/contrib/CoreCrypto/ml/pki/dsa/certificates/dsap.pem similarity index 100% rename from ucontrib/CoreCrypto/ml/pki/dsa/certificates/dsap.pem rename to contrib/CoreCrypto/ml/pki/dsa/certificates/dsap.pem diff --git a/ucontrib/CoreCrypto/ml/pki/dsa/db/ca.db.certs/01.pem b/contrib/CoreCrypto/ml/pki/dsa/db/ca.db.certs/01.pem similarity index 100% rename from ucontrib/CoreCrypto/ml/pki/dsa/db/ca.db.certs/01.pem rename to contrib/CoreCrypto/ml/pki/dsa/db/ca.db.certs/01.pem diff --git a/ucontrib/CoreCrypto/ml/pki/dsa/db/ca.db.certs/40a91a44.0 b/contrib/CoreCrypto/ml/pki/dsa/db/ca.db.certs/40a91a44.0 similarity index 100% rename from ucontrib/CoreCrypto/ml/pki/dsa/db/ca.db.certs/40a91a44.0 rename to contrib/CoreCrypto/ml/pki/dsa/db/ca.db.certs/40a91a44.0 diff --git a/ucontrib/CoreCrypto/ml/pki/dsa/db/ca.db.index b/contrib/CoreCrypto/ml/pki/dsa/db/ca.db.index similarity index 100% rename from ucontrib/CoreCrypto/ml/pki/dsa/db/ca.db.index rename to contrib/CoreCrypto/ml/pki/dsa/db/ca.db.index diff --git a/ucontrib/CoreCrypto/ml/pki/dsa/db/ca.db.index.attr b/contrib/CoreCrypto/ml/pki/dsa/db/ca.db.index.attr similarity index 100% rename from ucontrib/CoreCrypto/ml/pki/dsa/db/ca.db.index.attr rename to contrib/CoreCrypto/ml/pki/dsa/db/ca.db.index.attr diff --git a/ucontrib/CoreCrypto/ml/pki/dsa/db/ca.db.index.old b/contrib/CoreCrypto/ml/pki/dsa/db/ca.db.index.old similarity index 100% rename from ucontrib/CoreCrypto/ml/pki/dsa/db/ca.db.index.old rename to contrib/CoreCrypto/ml/pki/dsa/db/ca.db.index.old diff --git a/ucontrib/CoreCrypto/ml/pki/dsa/db/ca.db.serial b/contrib/CoreCrypto/ml/pki/dsa/db/ca.db.serial similarity index 100% rename from ucontrib/CoreCrypto/ml/pki/dsa/db/ca.db.serial rename to contrib/CoreCrypto/ml/pki/dsa/db/ca.db.serial diff --git a/ucontrib/CoreCrypto/ml/pki/dsa/db/ca.db.serial.old b/contrib/CoreCrypto/ml/pki/dsa/db/ca.db.serial.old similarity index 100% rename from ucontrib/CoreCrypto/ml/pki/dsa/db/ca.db.serial.old rename to contrib/CoreCrypto/ml/pki/dsa/db/ca.db.serial.old diff --git a/ucontrib/CoreCrypto/ml/pki/ecdsa/certificates/ca.crt b/contrib/CoreCrypto/ml/pki/ecdsa/certificates/ca.crt similarity index 100% rename from ucontrib/CoreCrypto/ml/pki/ecdsa/certificates/ca.crt rename to contrib/CoreCrypto/ml/pki/ecdsa/certificates/ca.crt diff --git a/ucontrib/CoreCrypto/ml/pki/ecdsa/certificates/ca.key b/contrib/CoreCrypto/ml/pki/ecdsa/certificates/ca.key similarity index 100% rename from ucontrib/CoreCrypto/ml/pki/ecdsa/certificates/ca.key rename to contrib/CoreCrypto/ml/pki/ecdsa/certificates/ca.key diff --git a/ucontrib/CoreCrypto/ml/pki/ecdsa/certificates/dh.pem b/contrib/CoreCrypto/ml/pki/ecdsa/certificates/dh.pem similarity index 100% rename from ucontrib/CoreCrypto/ml/pki/ecdsa/certificates/dh.pem rename to contrib/CoreCrypto/ml/pki/ecdsa/certificates/dh.pem diff --git a/ucontrib/CoreCrypto/ml/pki/ecdsa/certificates/dsap.pem b/contrib/CoreCrypto/ml/pki/ecdsa/certificates/dsap.pem similarity index 100% rename from ucontrib/CoreCrypto/ml/pki/ecdsa/certificates/dsap.pem rename to contrib/CoreCrypto/ml/pki/ecdsa/certificates/dsap.pem diff --git a/ucontrib/CoreCrypto/ml/pki/ecdsa/certificates/ecdsa.cert.mitls.org.crt b/contrib/CoreCrypto/ml/pki/ecdsa/certificates/ecdsa.cert.mitls.org.crt similarity index 100% rename from ucontrib/CoreCrypto/ml/pki/ecdsa/certificates/ecdsa.cert.mitls.org.crt rename to contrib/CoreCrypto/ml/pki/ecdsa/certificates/ecdsa.cert.mitls.org.crt diff --git a/ucontrib/CoreCrypto/ml/pki/ecdsa/certificates/ecdsa.cert.mitls.org.csr b/contrib/CoreCrypto/ml/pki/ecdsa/certificates/ecdsa.cert.mitls.org.csr similarity index 100% rename from ucontrib/CoreCrypto/ml/pki/ecdsa/certificates/ecdsa.cert.mitls.org.csr rename to contrib/CoreCrypto/ml/pki/ecdsa/certificates/ecdsa.cert.mitls.org.csr diff --git a/ucontrib/CoreCrypto/ml/pki/ecdsa/certificates/ecdsa.cert.mitls.org.key b/contrib/CoreCrypto/ml/pki/ecdsa/certificates/ecdsa.cert.mitls.org.key similarity index 100% rename from ucontrib/CoreCrypto/ml/pki/ecdsa/certificates/ecdsa.cert.mitls.org.key rename to contrib/CoreCrypto/ml/pki/ecdsa/certificates/ecdsa.cert.mitls.org.key diff --git a/ucontrib/CoreCrypto/ml/pki/ecdsa/certificates/ecdsa.cert.mitls.org.p12 b/contrib/CoreCrypto/ml/pki/ecdsa/certificates/ecdsa.cert.mitls.org.p12 similarity index 100% rename from ucontrib/CoreCrypto/ml/pki/ecdsa/certificates/ecdsa.cert.mitls.org.p12 rename to contrib/CoreCrypto/ml/pki/ecdsa/certificates/ecdsa.cert.mitls.org.p12 diff --git a/ucontrib/CoreCrypto/ml/pki/ecdsa/db/ca.db.certs/01.pem b/contrib/CoreCrypto/ml/pki/ecdsa/db/ca.db.certs/01.pem similarity index 100% rename from ucontrib/CoreCrypto/ml/pki/ecdsa/db/ca.db.certs/01.pem rename to contrib/CoreCrypto/ml/pki/ecdsa/db/ca.db.certs/01.pem diff --git a/ucontrib/CoreCrypto/ml/pki/ecdsa/db/ca.db.certs/9dc02e59.0 b/contrib/CoreCrypto/ml/pki/ecdsa/db/ca.db.certs/9dc02e59.0 similarity index 100% rename from ucontrib/CoreCrypto/ml/pki/ecdsa/db/ca.db.certs/9dc02e59.0 rename to contrib/CoreCrypto/ml/pki/ecdsa/db/ca.db.certs/9dc02e59.0 diff --git a/ucontrib/CoreCrypto/ml/pki/ecdsa/db/ca.db.index b/contrib/CoreCrypto/ml/pki/ecdsa/db/ca.db.index similarity index 100% rename from ucontrib/CoreCrypto/ml/pki/ecdsa/db/ca.db.index rename to contrib/CoreCrypto/ml/pki/ecdsa/db/ca.db.index diff --git a/ucontrib/CoreCrypto/ml/pki/ecdsa/db/ca.db.index.attr b/contrib/CoreCrypto/ml/pki/ecdsa/db/ca.db.index.attr similarity index 100% rename from ucontrib/CoreCrypto/ml/pki/ecdsa/db/ca.db.index.attr rename to contrib/CoreCrypto/ml/pki/ecdsa/db/ca.db.index.attr diff --git a/ucontrib/CoreCrypto/ml/pki/ecdsa/db/ca.db.index.old b/contrib/CoreCrypto/ml/pki/ecdsa/db/ca.db.index.old similarity index 100% rename from ucontrib/CoreCrypto/ml/pki/ecdsa/db/ca.db.index.old rename to contrib/CoreCrypto/ml/pki/ecdsa/db/ca.db.index.old diff --git a/ucontrib/CoreCrypto/ml/pki/ecdsa/db/ca.db.serial b/contrib/CoreCrypto/ml/pki/ecdsa/db/ca.db.serial similarity index 100% rename from ucontrib/CoreCrypto/ml/pki/ecdsa/db/ca.db.serial rename to contrib/CoreCrypto/ml/pki/ecdsa/db/ca.db.serial diff --git a/ucontrib/CoreCrypto/ml/pki/ecdsa/db/ca.db.serial.old b/contrib/CoreCrypto/ml/pki/ecdsa/db/ca.db.serial.old similarity index 100% rename from ucontrib/CoreCrypto/ml/pki/ecdsa/db/ca.db.serial.old rename to contrib/CoreCrypto/ml/pki/ecdsa/db/ca.db.serial.old diff --git a/ucontrib/CoreCrypto/ml/pki/pki.built b/contrib/CoreCrypto/ml/pki/pki.built similarity index 100% rename from ucontrib/CoreCrypto/ml/pki/pki.built rename to contrib/CoreCrypto/ml/pki/pki.built diff --git a/ucontrib/CoreCrypto/ml/pki/rsa/certificates/ca.crt b/contrib/CoreCrypto/ml/pki/rsa/certificates/ca.crt similarity index 100% rename from ucontrib/CoreCrypto/ml/pki/rsa/certificates/ca.crt rename to contrib/CoreCrypto/ml/pki/rsa/certificates/ca.crt diff --git a/ucontrib/CoreCrypto/ml/pki/rsa/certificates/ca.key b/contrib/CoreCrypto/ml/pki/rsa/certificates/ca.key similarity index 100% rename from ucontrib/CoreCrypto/ml/pki/rsa/certificates/ca.key rename to contrib/CoreCrypto/ml/pki/rsa/certificates/ca.key diff --git a/ucontrib/CoreCrypto/ml/pki/rsa/certificates/dh.pem b/contrib/CoreCrypto/ml/pki/rsa/certificates/dh.pem similarity index 100% rename from ucontrib/CoreCrypto/ml/pki/rsa/certificates/dh.pem rename to contrib/CoreCrypto/ml/pki/rsa/certificates/dh.pem diff --git a/ucontrib/CoreCrypto/ml/pki/rsa/certificates/dsap.pem b/contrib/CoreCrypto/ml/pki/rsa/certificates/dsap.pem similarity index 100% rename from ucontrib/CoreCrypto/ml/pki/rsa/certificates/dsap.pem rename to contrib/CoreCrypto/ml/pki/rsa/certificates/dsap.pem diff --git a/ucontrib/CoreCrypto/ml/pki/rsa/certificates/rsa.cert.mitls.org.crt b/contrib/CoreCrypto/ml/pki/rsa/certificates/rsa.cert.mitls.org.crt similarity index 100% rename from ucontrib/CoreCrypto/ml/pki/rsa/certificates/rsa.cert.mitls.org.crt rename to contrib/CoreCrypto/ml/pki/rsa/certificates/rsa.cert.mitls.org.crt diff --git a/ucontrib/CoreCrypto/ml/pki/rsa/certificates/rsa.cert.mitls.org.csr b/contrib/CoreCrypto/ml/pki/rsa/certificates/rsa.cert.mitls.org.csr similarity index 100% rename from ucontrib/CoreCrypto/ml/pki/rsa/certificates/rsa.cert.mitls.org.csr rename to contrib/CoreCrypto/ml/pki/rsa/certificates/rsa.cert.mitls.org.csr diff --git a/ucontrib/CoreCrypto/ml/pki/rsa/certificates/rsa.cert.mitls.org.key b/contrib/CoreCrypto/ml/pki/rsa/certificates/rsa.cert.mitls.org.key similarity index 100% rename from ucontrib/CoreCrypto/ml/pki/rsa/certificates/rsa.cert.mitls.org.key rename to contrib/CoreCrypto/ml/pki/rsa/certificates/rsa.cert.mitls.org.key diff --git a/ucontrib/CoreCrypto/ml/pki/rsa/certificates/rsa.cert.mitls.org.p12 b/contrib/CoreCrypto/ml/pki/rsa/certificates/rsa.cert.mitls.org.p12 similarity index 100% rename from ucontrib/CoreCrypto/ml/pki/rsa/certificates/rsa.cert.mitls.org.p12 rename to contrib/CoreCrypto/ml/pki/rsa/certificates/rsa.cert.mitls.org.p12 diff --git a/ucontrib/CoreCrypto/ml/pki/rsa/db/ca.db.certs/01.pem b/contrib/CoreCrypto/ml/pki/rsa/db/ca.db.certs/01.pem similarity index 100% rename from ucontrib/CoreCrypto/ml/pki/rsa/db/ca.db.certs/01.pem rename to contrib/CoreCrypto/ml/pki/rsa/db/ca.db.certs/01.pem diff --git a/ucontrib/CoreCrypto/ml/pki/rsa/db/ca.db.certs/db930587.0 b/contrib/CoreCrypto/ml/pki/rsa/db/ca.db.certs/db930587.0 similarity index 100% rename from ucontrib/CoreCrypto/ml/pki/rsa/db/ca.db.certs/db930587.0 rename to contrib/CoreCrypto/ml/pki/rsa/db/ca.db.certs/db930587.0 diff --git a/ucontrib/CoreCrypto/ml/pki/rsa/db/ca.db.index b/contrib/CoreCrypto/ml/pki/rsa/db/ca.db.index similarity index 100% rename from ucontrib/CoreCrypto/ml/pki/rsa/db/ca.db.index rename to contrib/CoreCrypto/ml/pki/rsa/db/ca.db.index diff --git a/ucontrib/CoreCrypto/ml/pki/rsa/db/ca.db.index.attr b/contrib/CoreCrypto/ml/pki/rsa/db/ca.db.index.attr similarity index 100% rename from ucontrib/CoreCrypto/ml/pki/rsa/db/ca.db.index.attr rename to contrib/CoreCrypto/ml/pki/rsa/db/ca.db.index.attr diff --git a/ucontrib/CoreCrypto/ml/pki/rsa/db/ca.db.index.old b/contrib/CoreCrypto/ml/pki/rsa/db/ca.db.index.old similarity index 100% rename from ucontrib/CoreCrypto/ml/pki/rsa/db/ca.db.index.old rename to contrib/CoreCrypto/ml/pki/rsa/db/ca.db.index.old diff --git a/ucontrib/CoreCrypto/ml/pki/rsa/db/ca.db.serial b/contrib/CoreCrypto/ml/pki/rsa/db/ca.db.serial similarity index 100% rename from ucontrib/CoreCrypto/ml/pki/rsa/db/ca.db.serial rename to contrib/CoreCrypto/ml/pki/rsa/db/ca.db.serial diff --git a/ucontrib/CoreCrypto/ml/pki/rsa/db/ca.db.serial.old b/contrib/CoreCrypto/ml/pki/rsa/db/ca.db.serial.old similarity index 100% rename from ucontrib/CoreCrypto/ml/pki/rsa/db/ca.db.serial.old rename to contrib/CoreCrypto/ml/pki/rsa/db/ca.db.serial.old diff --git a/ucontrib/Log/fst/Log.fst b/contrib/Log/fst/Log.fst similarity index 100% rename from ucontrib/Log/fst/Log.fst rename to contrib/Log/fst/Log.fst diff --git a/ucontrib/Makefile b/contrib/Makefile similarity index 100% rename from ucontrib/Makefile rename to contrib/Makefile diff --git a/ucontrib/Platform/fst/Platform.Bytes.fst b/contrib/Platform/fst/Platform.Bytes.fst similarity index 100% rename from ucontrib/Platform/fst/Platform.Bytes.fst rename to contrib/Platform/fst/Platform.Bytes.fst diff --git a/ucontrib/Platform/fst/Platform.Bytes.fst.hints b/contrib/Platform/fst/Platform.Bytes.fst.hints similarity index 100% rename from ucontrib/Platform/fst/Platform.Bytes.fst.hints rename to contrib/Platform/fst/Platform.Bytes.fst.hints diff --git a/ucontrib/Platform/fst/Platform.Date.fst b/contrib/Platform/fst/Platform.Date.fst similarity index 100% rename from ucontrib/Platform/fst/Platform.Date.fst rename to contrib/Platform/fst/Platform.Date.fst diff --git a/ucontrib/Platform/fst/Platform.Date.fst.hints b/contrib/Platform/fst/Platform.Date.fst.hints similarity index 100% rename from ucontrib/Platform/fst/Platform.Date.fst.hints rename to contrib/Platform/fst/Platform.Date.fst.hints diff --git a/ucontrib/Platform/fst/Platform.Error.fst b/contrib/Platform/fst/Platform.Error.fst similarity index 100% rename from ucontrib/Platform/fst/Platform.Error.fst rename to contrib/Platform/fst/Platform.Error.fst diff --git a/ucontrib/Platform/fst/Platform.Error.fst.hints b/contrib/Platform/fst/Platform.Error.fst.hints similarity index 100% rename from ucontrib/Platform/fst/Platform.Error.fst.hints rename to contrib/Platform/fst/Platform.Error.fst.hints diff --git a/ucontrib/Platform/fst/Platform.Tcp.fst b/contrib/Platform/fst/Platform.Tcp.fst similarity index 100% rename from ucontrib/Platform/fst/Platform.Tcp.fst rename to contrib/Platform/fst/Platform.Tcp.fst diff --git a/ucontrib/Platform/fst/Platform.Tcp.fst.hints b/contrib/Platform/fst/Platform.Tcp.fst.hints similarity index 100% rename from ucontrib/Platform/fst/Platform.Tcp.fst.hints rename to contrib/Platform/fst/Platform.Tcp.fst.hints diff --git a/ucontrib/Platform/fst/Platform.Udp.fst b/contrib/Platform/fst/Platform.Udp.fst similarity index 100% rename from ucontrib/Platform/fst/Platform.Udp.fst rename to contrib/Platform/fst/Platform.Udp.fst diff --git a/ucontrib/Platform/fst/Platform.Udp.fst.hints b/contrib/Platform/fst/Platform.Udp.fst.hints similarity index 100% rename from ucontrib/Platform/fst/Platform.Udp.fst.hints rename to contrib/Platform/fst/Platform.Udp.fst.hints diff --git a/ucontrib/Platform/ml/Makefile b/contrib/Platform/ml/Makefile similarity index 100% rename from ucontrib/Platform/ml/Makefile rename to contrib/Platform/ml/Makefile diff --git a/ucontrib/Platform/ml/Tests.ml b/contrib/Platform/ml/Tests.ml similarity index 100% rename from ucontrib/Platform/ml/Tests.ml rename to contrib/Platform/ml/Tests.ml diff --git a/ucontrib/Platform/ml/platform.ml b/contrib/Platform/ml/platform.ml similarity index 100% rename from ucontrib/Platform/ml/platform.ml rename to contrib/Platform/ml/platform.ml diff --git a/doc/Makefile.include b/doc/Makefile.include index 0da43f8a8b1..a0563da7ef6 100644 --- a/doc/Makefile.include +++ b/doc/Makefile.include @@ -2,7 +2,7 @@ ifdef FSTAR_HOME FSTAR_ULIB=$(shell if test -d $(FSTAR_HOME)/ulib ; then echo $(FSTAR_HOME)/ulib ; else echo $(FSTAR_HOME)/lib/fstar ; fi) - FSTAR_CONTRIB=$(shell if test -d $(FSTAR_HOME)/ucontrib ; then echo $(FSTAR_HOME)/ucontrib ; else echo $(FSTAR_HOME)/share/fstar/contrib ; fi) + FSTAR_CONTRIB=$(shell if test -d $(FSTAR_HOME)/contrib ; then echo $(FSTAR_HOME)/contrib ; else echo $(FSTAR_HOME)/share/fstar/contrib ; fi) else # fstar.exe assumed to be in some bin/ directory # included in the PATH (e.g. opam package, /usr or /usr/local) diff --git a/examples/crypto/Makefile b/examples/crypto/Makefile index 9e0ce1bf021..0b9c6f9ec83 100644 --- a/examples/crypto/Makefile +++ b/examples/crypto/Makefile @@ -1,8 +1,8 @@ FSTAR_ROOT ?= ../.. include $(FSTAR_ROOT)/mk/test.mk -OTHERFLAGS += --include $(FSTAR_ROOT)/ucontrib/Platform/fst -OTHERFLAGS += --include $(FSTAR_ROOT)/ucontrib/CoreCrypto/fst +OTHERFLAGS += --include $(FSTAR_ROOT)/contrib/Platform/fst +OTHERFLAGS += --include $(FSTAR_ROOT)/contrib/CoreCrypto/fst all: # RPC.ml CntProtocol.ml diff --git a/examples/old/tls-record-layer/LowCProvider/Makefile b/examples/old/tls-record-layer/LowCProvider/Makefile index 5e08a8936df..c31d57c756f 100644 --- a/examples/old/tls-record-layer/LowCProvider/Makefile +++ b/examples/old/tls-record-layer/LowCProvider/Makefile @@ -1,5 +1,5 @@ FSTAR_HOME = ../../.. -CONTRIB=ucontrib +CONTRIB=contrib PLATFORM = $(FSTAR_HOME)/$(CONTRIB)/Platform/ml CORECRYPTO = $(FSTAR_HOME)/$(CONTRIB)/CoreCrypto/ml INCLUDE=-package batteries,zarith -I $(PLATFORM) -I $(CORECRYPTO) diff --git a/examples/old/tls-record-layer/Makefile b/examples/old/tls-record-layer/Makefile index 55209d4ef3c..3d63b057ef7 100644 --- a/examples/old/tls-record-layer/Makefile +++ b/examples/old/tls-record-layer/Makefile @@ -328,7 +328,7 @@ ocaml-test.exe: ocaml-test-extract $(OCAMLOPT) -I tmp -I crypto/ml -I $(AEAD_ODIR) $(OCAML_FILES) -o ocaml-test.exe ./ocaml-test.exe -OPENSSL_HOME=../../ucontrib/CoreCrypto/ml/openssl +OPENSSL_HOME=../../contrib/CoreCrypto/ml/openssl #OPENSSL_HOME=/usr/local/Cellar/openssl\@1.1/1.1.0c #CC=gcc-6 diff --git a/examples/old/tls-record-layer/README.md b/examples/old/tls-record-layer/README.md index 20a35ea510d..df6504031ea 100644 --- a/examples/old/tls-record-layer/README.md +++ b/examples/old/tls-record-layer/README.md @@ -1,4 +1,4 @@ To compile a 32-bit version of OpenSSL and run the tests in 32-bit mode: -jonathan@chartreuse:~/Code/fstar/ucontrib/CoreCrypto/ml/openssl ((174ec01...)) $ KERNEL_BITS=32 ./config no-asm -m32 +jonathan@chartreuse:~/Code/fstar/contrib/CoreCrypto/ml/openssl ((174ec01...)) $ KERNEL_BITS=32 ./config no-asm -m32 jonathan@chartreuse:~/Code/fstar/examples/low-level (c_record_aead) $ make test-perf.exe CFLAGS=-m32 KOPTS="-ccopt -m32" -B diff --git a/src/ocaml-output/Makefile b/src/ocaml-output/Makefile index 48bc02dad14..d3ce6ad14d9 100644 --- a/src/ocaml-output/Makefile +++ b/src/ocaml-output/Makefile @@ -80,10 +80,12 @@ install: .PHONY: install-sides install-sides: @# Then the examples (those now work from any F* installation flavor, sources, binary package or opam) - @# ucontrib is needed by examples/crypto + @# contrib is needed by examples/crypto $(call install_dir,examples,share/fstar/examples) - $(call install_dir,ucontrib,share/fstar/contrib) + $(call install_dir,contrib,share/fstar/contrib) $(call install_dir,mk,share/fstar/mk) + @echo '# This line added only for the binary package, to use the fstar.exe in the package' >> $(PREFIX)/share/fstar/mk/test.mk + @echo 'FSTAR_EXE := $$(abspath $$(FSTAR_ROOT)/../../bin/fstar.exe)' >> $(PREFIX)/share/fstar/mk/test.mk @# Then the tutorial ifeq ($(MADOKO),Madoko) @# Build the tutorial first diff --git a/tests/bug-reports/closed/Bug1052.fst b/tests/bug-reports/closed/Bug1052.fst index b97282b39af..41345ec320e 100644 --- a/tests/bug-reports/closed/Bug1052.fst +++ b/tests/bug-reports/closed/Bug1052.fst @@ -17,4 +17,4 @@ module Bug1052 open FStar.All -(* fstar.exe --fstar_home /home/hritcu/Projects/fstar/pub --include doc/tutorial/code/solutions --include ucontrib/Platform/fst --include ucontrib/CoreCrypto/fst --smt /home/hritcu/Apps/z3-4.5.0-x64-ubuntu-14.04/bin/z3 blah.fst *) +(* fstar.exe --fstar_home /home/hritcu/Projects/fstar/pub --include doc/tutorial/code/solutions --include contrib/Platform/fst --include contrib/CoreCrypto/fst --smt /home/hritcu/Apps/z3-4.5.0-x64-ubuntu-14.04/bin/z3 blah.fst *) diff --git a/ucontrib/CoreCrypto/fst/CoreCrypto.fst b/ucontrib/CoreCrypto/fst/CoreCrypto.fst deleted file mode 100644 index 05dfaf2afb3..00000000000 --- a/ucontrib/CoreCrypto/fst/CoreCrypto.fst +++ /dev/null @@ -1,247 +0,0 @@ -(* - Copyright 2008-2018 Microsoft Research - - Licensed under the Apache License, Version 2.0 (the "License"); - you may not use this file except in compliance with the License. - You may obtain a copy of the License at - - http://www.apache.org/licenses/LICENSE-2.0 - - Unless required by applicable law or agreed to in writing, software - distributed under the License is distributed on an "AS IS" BASIS, - WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. - See the License for the specific language governing permissions and - limitations under the License. -*) -module CoreCrypto - -open Platform.Bytes - -(* ------------ Hashing ------------ *) -type hash_alg = - | MD5 - | SHA1 - | SHA224 - | SHA256 - | SHA384 - | SHA512 - -let hashSize = function - | MD5 -> 16 - | SHA1 -> 20 - | SHA224 -> 28 - | SHA256 -> 32 - | SHA384 -> 48 - | SHA512 -> 64 - -(* These implementations are not pure; to be upgraded! *) -assume val hash : alg:hash_alg -> bytes -> Tot (h:bytes{length h = hashSize alg}) -assume val hmac : alg:hash_alg -> bytes -> bytes -> Tot (h:bytes{length h = hashSize alg}) - -(* Digest functions *) -assume type hash_ctx : Type0 (* SI: or assume_new_abstract_type?*) -assume val digest_create : hash_alg -> EXT hash_ctx -assume val digest_update : hash_ctx -> bytes -> EXT unit -assume val digest_final : hash_ctx -> EXT bytes - -(* --------------------------- *) - - -type sig_alg = | RSASIG | DSA | ECDSA | RSAPSS -type block_cipher = | AES_128_CBC | AES_256_CBC | TDES_EDE_CBC -type stream_cipher = | RC4_128 -type rsa_padding = | Pad_none | Pad_PKCS1 - -(* NB these constant functions must *exactly* match those in the - trusted CoreCrypto.ml. We should compile them instead! *) - -let blockSize = function - | TDES_EDE_CBC -> 8 - | AES_128_CBC -> 16 - | AES_256_CBC -> 16 - -(* Authenticated Encryption for TLS. - Note that their AAD contents depends on the protocol version. *) - -type aead_cipher = - | AES_128_GCM - | AES_256_GCM - | CHACHA20_POLY1305 - | AES_128_CCM // "Counter with CBC-Message Authentication Code" - | AES_256_CCM - | AES_128_CCM_8 // variant with truncated 8-byte tags - | AES_256_CCM_8 - -// the key materials consist of an encryption key, a static IV, and an authentication key. - -let aeadKeySize = function - | AES_128_CCM -> 16 - | AES_128_CCM_8 -> 16 - | AES_128_GCM -> 16 - | AES_256_CCM -> 32 - | AES_256_CCM_8 -> 32 - | AES_256_GCM -> 32 - | CHACHA20_POLY1305 -> 32 - -let aeadRealIVSize (a:aead_cipher) = 12 - -// the ciphertext ends with an authentication tag -let aeadTagSize = function - | AES_128_CCM_8 -> 8 - | AES_256_CCM_8 -> 8 - | AES_128_CCM -> 16 - | AES_256_CCM -> 16 - | AES_128_GCM -> 16 - | AES_256_GCM -> 16 - | CHACHA20_POLY1305 -> 16 - -//16-09-12 added precise concrete spec, matching what we implement in low-level/crypto -//16-09-12 for robustness, we should at least test it when using external crypto. -assume val aead_encryptT: - a: aead_cipher -> - k: lbytes (aeadKeySize a) -> - iv:lbytes (aeadRealIVSize a) -> - ad:bytes -> - plain:bytes -> - GTot (lbytes (length plain + aeadTagSize a)) - -assume val aead_encrypt: - a: aead_cipher -> - k: lbytes (aeadKeySize a) -> - iv:lbytes (aeadRealIVSize a) -> - ad:bytes -> - plain:bytes -> - EXT (c:bytes {c = aead_encryptT a k iv ad plain}) - -assume val aead_decrypt: - a: aead_cipher -> - k: lbytes (aeadKeySize a) -> - iv:lbytes (aeadRealIVSize a) -> - ad:bytes -> - cipher:bytes{length cipher >= aeadTagSize a} -> - EXT (o:option (b:bytes{length b + aeadTagSize a = length cipher}) - {forall (p:bytes). cipher = aead_encryptT a k iv ad p <==> (Some? o /\ Some?.v o == p) }) - - -type rsa_key = { - rsa_mod : bytes; - rsa_pub_exp : bytes; - rsa_prv_exp : option bytes; -} - -type dsa_params = { - dsa_p : bytes; - dsa_q : bytes; - dsa_g : bytes; -} - -type dsa_key = { - dsa_params : dsa_params; - dsa_public : bytes; - dsa_private : option bytes; -} - -type dh_params = { - dh_p : bytes; - dh_g : bytes; - dh_q : option bytes; - safe_prime : bool; -} - -type dh_key = { - dh_params : dh_params; - dh_public : bytes; - dh_private : option bytes; -} - -(* TODO: revisit the Tot annotations, switch to EXT when appropriate *) - -assume val block_encrypt : block_cipher -> bytes -> bytes -> bytes -> EXT bytes -assume val block_decrypt : block_cipher -> bytes -> bytes -> bytes -> EXT bytes - -assume new type cipher_stream : Type0 -assume val stream_encryptor : stream_cipher -> bytes -> EXT cipher_stream -assume val stream_decryptor : stream_cipher -> bytes -> EXT cipher_stream -assume val stream_process : cipher_stream -> bytes -> EXT bytes -assume val stream_fini : cipher_stream -> EXT unit - -assume val random : l:nat -> EXT (lbytes l) - -assume val rsa_gen_key : int -> EXT (k:rsa_key{Some? k.rsa_prv_exp}) -assume val rsa_encrypt : rsa_key -> rsa_padding -> bytes -> EXT bytes -assume val rsa_decrypt : k:rsa_key{Some? k.rsa_prv_exp} -> rsa_padding -> bytes -> EXT (option bytes) -assume val rsa_sign : option hash_alg -> k:rsa_key{Some? k.rsa_prv_exp} -> pss:bool -> bytes -> EXT bytes -assume val rsa_verify : option hash_alg -> rsa_key -> pss:bool -> bytes -> bytes -> EXT bool - -assume val dsa_gen_key : int -> EXT (k:dsa_key{Some? k.dsa_private}) -assume val dsa_sign : option hash_alg -> k:dsa_key{Some? k.dsa_private} -> bytes -> EXT bytes -assume val dsa_verify : option hash_alg -> dsa_key -> bytes -> bytes -> Tot bool - -assume val dh_gen_params : int -> EXT dh_params -assume val dh_gen_key : p:dh_params -> EXT (k:dh_key{Some? k.dh_private /\ k.dh_params = p /\ length k.dh_public <= length p.dh_p}) -assume val dh_agreement : k:dh_key{Some? k.dh_private} -> bytes -> EXT bytes - -(* type ec_prime = { ecp_prime : string; ecp_order : string; ecp_a : string; ecp_b : string; ecp_gx : string; ecp_gy : string; ecp_bytelen : int; ecp_id : bytes; } *) - -type ec_curve = - | ECC_P256 - | ECC_P384 - | ECC_P521 - | ECC_X25519 - | ECC_X448 - -(* Bytelen of field elements *) -val ec_bytelen: ec_curve -> Tot (n:nat{n <= 127}) -let ec_bytelen = function - | ECC_P256 -> 32 - | ECC_P384 -> 48 - | ECC_P521 -> 66 (* ceil(521/8) *) - | ECC_X25519 -> 32 - | ECC_X448 -> 56 - -type ec_params = { - curve: ec_curve; - point_compression: bool; -} - -type ec_point = { - ecx : bytes; - ecy : bytes; -} - -type ec_key = { - ec_params : ec_params; - ec_point : ec_point; - ec_priv : option bytes; -} - -assume val ec_is_on_curve: ec_params -> ec_point -> Tot bool -assume val ecdh_agreement: k:ec_key{Some? k.ec_priv} -> ec_point -> EXT bytes - -assume val ecdsa_sign: option hash_alg -> k:ec_key{Some? k.ec_priv} -> bytes -> EXT bytes -assume val ecdsa_verify: option hash_alg -> ec_key -> bytes -> bytes -> EXT bool -assume val ec_gen_key: p:ec_params - -> EXT (k:ec_key{Some? k.ec_priv /\ k.ec_params = p /\ - length k.ec_point.ecx = ec_bytelen k.ec_params.curve /\ - length k.ec_point.ecy = ec_bytelen k.ec_params.curve}) - -//TODO: keep also abtsract OpenSSL representation for efficiency? -type key = - | KeyRSA of rsa_key - | KeyDSA of dsa_key - | KeyECDSA of ec_key - -// If we are careless we can cause openssl segfaults when signing or encrypting -// with keys that are missing the "private" field. -// The only has_priv keys are the ones loaded with load_key and or generated with gen_key -let has_priv : key -> Type0 = function - | KeyRSA k -> Some? k.rsa_prv_exp - | KeyDSA k -> Some? k.dsa_private - | KeyECDSA k -> Some? k.ec_priv - -assume val validate_chain: der_list:list bytes -> for_signing:bool -> hostname:option string -> ca_file:string -> Tot bool -assume val get_key_from_cert: bytes -> Tot (option key) -assume val hash_and_sign: k:key{has_priv k} -> hash_alg -> bytes -> Tot bytes -assume val verify_signature: key -> hash_alg -> tbs:bytes -> sigv:bytes -> Tot bool -assume val load_chain: pemfile:string -> Tot (option (list bytes)) -assume val load_key: keyfile:string -> Tot (option (k:key{has_priv k})) diff --git a/ucontrib/CoreCrypto/fst/DHDB.fst b/ucontrib/CoreCrypto/fst/DHDB.fst deleted file mode 100644 index 6a1c5542caf..00000000000 --- a/ucontrib/CoreCrypto/fst/DHDB.fst +++ /dev/null @@ -1,38 +0,0 @@ -(* - Copyright 2008-2018 Microsoft Research - - Licensed under the Apache License, Version 2.0 (the "License"); - you may not use this file except in compliance with the License. - You may obtain a copy of the License at - - http://www.apache.org/licenses/LICENSE-2.0 - - Unless required by applicable law or agreed to in writing, software - distributed under the License is distributed on an "AS IS" BASIS, - WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. - See the License for the specific language governing permissions and - limitations under the License. -*) -module DHDB -open Platform.Bytes -open CoreCrypto - -type key = bytes & bytes // p, g -type value = bytes & bool // q, safe_prime? - -assume new type dhdb : Type0 - -assume val defaultFileName: string -assume val defaultDHPrimeConfidence: int -assume val defaultPQMinLength: nat & nat - -assume val create: string -> dhdb -assume val select: dhdb -> key -> option value -assume val insert: dhdb -> key -> value -> dhdb -assume val remove: dhdb -> key -> dhdb -assume val keys : dhdb -> list key -assume val merge : dhdb -> string -> dhdb - -assume val dh_check_params: dhdb -> int -> (int & int) -> bytes -> bytes -> option (dhdb & dh_params) -assume val dh_check_element: dh_params -> bytes -> bool -assume val load_default_params: string -> dhdb -> (int & int) -> (dhdb & dh_params)