Merge remote-tracking branch 'origin/master' into merge_fstar_master_…

…20180510
project-everest · May 18, 2018 · 32a397b · 32a397b
2 parents e2c6bed + 8d978af
commit 32a397b
Show file tree

Hide file tree

Showing 32 changed files with 4,207 additions and 98 deletions.
diff --git a/apps/cmitls/cmitls.c b/apps/cmitls/cmitls.c
@@ -451,7 +451,11 @@ int Configure(mitls_state **pstate)
     }
 
     if (option_alpn) {
-        r = FFI_mitls_configure_alpn(state, option_alpn);
+	mitls_alpn alpn = {
+          .alpn = (unsigned char*)option_alpn,
+	  .alpn_len = strlen(option_alpn)
+	};
+        r = FFI_mitls_configure_alpn(state, &alpn, 1);
         if (r == 0) {
             printf("FFI_mitls_configure_alpn(%s) failed.\n", option_alpn);
             return 2;

diff --git a/apps/quicMinusNet/Makefile b/apps/quicMinusNet/Makefile
@@ -35,7 +35,7 @@ else ifeq ($(UNAME),Linux)
   LIBMITLS=libmitls.so
   LIBQC=libquicprovider.so
   LIBPKI=libmipki.so
-  CFLAGS+=-lpthread
+  CFLAGS+=-lpthread -pthread
   LIBPATHS=$(EVERCRYPT_HOME)/out:$(MITLS_HOME)/src/pki:$(MITLS_HOME)/src/tls/extract/Kremlin-Library:$(HACL_HOME)/secure_api/out/runtime_switch:$(MLCRYPTO_HOME)/openssl
   LD_LIBRARY_PATH := $(LIBPATHS):$(LD_LIBRARY_PATH)
   export LD_LIBRARY_PATH

diff --git a/apps/quicMinusNet/quic.c b/apps/quicMinusNet/quic.c
@@ -247,10 +247,16 @@ int main(int argc, char **argv)
     }
   };
 
+  mitls_alpn alpn = {
+    .alpn = "hq-10",
+    .alpn_len = 5
+  };
+
   quic_config config = {
     .is_server = 1,
     .host_name = "",
-    .alpn = "hq-08",
+    .alpn = &alpn,
+    .alpn_count = 1,
     .server_ticket = NULL,
     .exts = client_qtp,
     .exts_count = 1,

diff --git a/libs/ffi/ffi.c b/libs/ffi/ffi.c
@@ -20,6 +20,7 @@
 #define MITLS_FFI_LIST \
   MITLS_FFI_ENTRY(Config) \
   MITLS_FFI_ENTRY(SetTicketKey) \
+  MITLS_FFI_ENTRY(SetSealingKey) \
   MITLS_FFI_ENTRY(SetCipherSuites) \
   MITLS_FFI_ENTRY(SetSignatureAlgorithms) \
   MITLS_FFI_ENTRY(SetNamedGroups) \
@@ -223,16 +224,17 @@ static int configure_common_caml(/* in */ mitls_state *state, const char * str,
 }
 
 // The OCaml runtime system must be acquired before calling this
-static int ocaml_set_ticket_key(const char *alg, const unsigned char *ticketkey, size_t klen)
+static int ocaml_set_global_key(int sealing, const char *alg, const unsigned char *ticketkey, size_t klen)
 {
     int ret;
+    value *setter = sealing ? g_mitls_FFI_SetSealingKey : g_mitls_FFI_SetTicketKey;
     CAMLparam0();
     CAMLlocal3(r, a, tkey);
     tkey = caml_alloc_string(klen);
     memcpy(String_val(tkey), ticketkey, klen);
 
     a = caml_copy_string(alg);
-    r = caml_callback2_exn(*g_mitls_FFI_SetTicketKey, a, tkey);
+    r = caml_callback2_exn(*setter, a, tkey);
 
     if (Is_exception_result(r)) {
       report_caml_exception(r);
@@ -248,7 +250,18 @@ int MITLS_CALLCONV FFI_mitls_set_ticket_key(const char *alg, const unsigned char
     int ret;
     caml_c_thread_register();
     caml_acquire_runtime_system();
-    ret = ocaml_set_ticket_key(alg, tk, klen);
+    ret = ocaml_set_global_key(0, alg, tk, klen);
+    caml_release_runtime_system();
+    caml_c_thread_unregister();
+    return ret;
+}
+
+int MITLS_CALLCONV FFI_mitls_set_sealing_key(const char *alg, const unsigned char *tk, size_t klen)
+{
+    int ret;
+    caml_c_thread_register();
+    caml_acquire_runtime_system();
+    ret = ocaml_set_global_key(1, alg, tk, klen);
     caml_release_runtime_system();
     caml_c_thread_unregister();
     return ret;
@@ -287,12 +300,49 @@ int MITLS_CALLCONV FFI_mitls_configure_named_groups(/* in */ mitls_state *state,
     return ret;
 }
 
-int MITLS_CALLCONV FFI_mitls_configure_alpn(/* in */ mitls_state *state, const char *apl)
+static value alpn_list_of_array(const mitls_alpn *alpn, size_t alpn_count)
+{
+  CAMLparam0();
+  CAMLlocal3(apl, cur, str);
+  apl = Val_int(0);
+
+  for(int i = (alpn_count & 255) - 1; i >= 0; i--)
+  {
+    cur = caml_alloc(2, 0);
+    str = caml_alloc_string(alpn[i].alpn_len);
+    memcpy(String_val(str), alpn[i].alpn, alpn[i].alpn_len);
+    Field(cur, 0) = str;
+    Field(cur, 1) = apl;
+    apl = cur;
+  }
+
+  CAMLreturn(apl);
+}
+
+static int ocaml_set_alpn(/* in */ mitls_state *state, const mitls_alpn *alpn, size_t alpn_count)
+{
+    CAMLparam0();
+    CAMLlocal2(config, camlvalue);
+    int ret = 0;
+
+    camlvalue = alpn_list_of_array(alpn, alpn_count);
+    config = caml_callback2_exn(*g_mitls_FFI_SetALPN, state->fstar_state, camlvalue);
+    if (Is_exception_result(config)) {
+        report_caml_exception(config);
+    } else {
+        state->fstar_state = config;
+        ret = 1;
+    }
+
+    CAMLreturnT(int,ret);
+}
+
+int MITLS_CALLCONV FFI_mitls_configure_alpn(/* in */ mitls_state *state, const mitls_alpn *alpn, size_t alpn_count)
 {
     int ret;
     caml_c_thread_register();
     caml_acquire_runtime_system();
-    ret = configure_common_caml(state, apl, g_mitls_FFI_SetALPN);
+    ret = ocaml_set_alpn(state, alpn, alpn_count);
     caml_release_runtime_system();
     caml_c_thread_unregister();
     return ret;
@@ -852,16 +902,16 @@ static int FFI_mitls_quic_create_caml(quic_state **st, quic_config *cfg)
        }
     }
 
-    if(cfg->alpn) {
-      if(!configure_common_caml(&ms, cfg->alpn, g_mitls_FFI_SetALPN))
+    if(cfg->alpn && cfg->alpn_count) {
+      if(!ocaml_set_alpn(&ms, cfg->alpn, cfg->alpn_count))
       {
         report_error("FFI_mitls_quic_create_caml: failed to set application-level protocols");
         CAMLreturnT(int, 0);
       }
     }
 
     if(cfg->ticket_enc_alg && cfg->ticket_key) {
-       if(!ocaml_set_ticket_key(cfg->ticket_enc_alg, cfg->ticket_key, cfg->ticket_key_len))
+       if(!ocaml_set_global_key(0, cfg->ticket_enc_alg, cfg->ticket_key, cfg->ticket_key_len))
        {
          report_error("FFI_mitls_quic_create_caml: set ticket key");
          CAMLreturnT(int, 0);
@@ -981,7 +1031,8 @@ static quic_result FFI_mitls_quic_process_caml(
         report_caml_exception(result);
     } else {
         int rc = Int_val(Field(result, 0));
-        int errorcode = Int_val(Field(result, 1));
+//        int errorcode = Int_val(Field(result, 1));
+//        FIXME: interpret error code
         if (rc <= TLS_server_complete) {
             ret = (quic_result) rc;
         }

diff --git a/libs/ffi/mitlsffi.h b/libs/ffi/mitlsffi.h
@@ -34,6 +34,11 @@ typedef struct {
   size_t ext_data_len;
 } mitls_extension;
 
+typedef struct {
+  const unsigned char *alpn;
+  size_t alpn_len;
+} mitls_alpn;
+
 typedef enum {
   TLS_hash_MD5 = 0,
   TLS_hash_SHA1 = 1,
@@ -104,12 +109,18 @@ extern void MITLS_CALLCONV FFI_mitls_set_trace_callback(pfn_mitls_trace_callback
 // Perform one-time initialization
 extern int MITLS_CALLCONV FFI_mitls_init(void);
 
+// Set the global ticket encryption key (used on the server side for tickets and cookies)
+// and sealing key (used on the client side to seal session information for resumption)
+// alg is one of "AES128-GCM", "AES256-GCM", "CHACHA20-POLY1305", klen must account for
+// the key and IV (e.g. 32 + 12). If these keys are not set, fresh random keys will be used.
+extern int MITLS_CALLCONV FFI_mitls_set_ticket_key(const char *alg, const unsigned char *ticketkey, size_t klen);
+extern int MITLS_CALLCONV FFI_mitls_set_sealing_key(const char *alg, const unsigned char *sealingkey, size_t klen);
+
 // Perform one-time termination
 extern void MITLS_CALLCONV FFI_mitls_cleanup(void);
 
 // Configure miTLS ahead of connecting
 extern int MITLS_CALLCONV FFI_mitls_configure(/* out */ mitls_state **state, const char *tls_version, const char *host_name);
-extern int MITLS_CALLCONV FFI_mitls_set_ticket_key(const char *alg, const unsigned char *ticketkey, size_t klen);
 
 // Configure a ticket to resume (client only). Can be called more than once to offer multiple 1.3 PSK
 extern int MITLS_CALLCONV FFI_mitls_configure_ticket(mitls_state *state, const mitls_ticket *ticket);
@@ -118,7 +129,7 @@ extern int MITLS_CALLCONV FFI_mitls_configure_ticket(mitls_state *state, const m
 extern int MITLS_CALLCONV FFI_mitls_configure_cipher_suites(/* in */ mitls_state *state, const char *cs);
 extern int MITLS_CALLCONV FFI_mitls_configure_signature_algorithms(/* in */ mitls_state *state, const char *sa);
 extern int MITLS_CALLCONV FFI_mitls_configure_named_groups(/* in */ mitls_state *state, const char *ng);
-extern int MITLS_CALLCONV FFI_mitls_configure_alpn(/* in */ mitls_state *state, const char *apl);
+extern int MITLS_CALLCONV FFI_mitls_configure_alpn(/* in */ mitls_state *state, const mitls_alpn *alpn, size_t alpn_count);
 extern int MITLS_CALLCONV FFI_mitls_configure_early_data(/* in */ mitls_state *state, uint32_t max_early_data);
 extern int MITLS_CALLCONV FFI_mitls_configure_custom_extensions(/* in */ mitls_state *state, const mitls_extension *exts, size_t exts_count);
 extern int MITLS_CALLCONV FFI_mitls_configure_ticket_callback(mitls_state *state, void *cb_state, pfn_FFI_ticket_cb ticket_cb);
@@ -183,14 +194,15 @@ typedef mitls_ticket quic_ticket;
 typedef struct {
   int is_server;
 
-  const char *alpn; // Colon separated list of application-level protocols, or NULL
   const char *cipher_suites; // Colon separated list of ciphersuite or NULL
   const char *signature_algorithms; // Colon separated list of signature schemes or NULL
   const char *named_groups; // Colon separated list of Diffie-Hellman groups or NULL
   int enable_0rtt; // Probably true for QUIC
 
   // only used by the client
   const char *host_name; // Client only, sent in SNI. Can pass NULL for server
+  const mitls_alpn *alpn; // Array of ALPN protocols to offer
+  size_t alpn_count; // Size of above array
   const quic_ticket *server_ticket; // May be NULL
   const mitls_extension *exts; // Array of custom extensions to offer, may be NULL
   size_t exts_count;           // Size of custom extensions array

diff --git a/src/tls/AEADProvider.fst b/src/tls/AEADProvider.fst
@@ -248,7 +248,8 @@ let coerce (i:id) (r:rgn) (k:key i) (s:salt i)
     in
   dbg ((prov())^": COERCE(K="^(hex_of_bytes k)^")");
   w
-#reset-options
+
+//#reset-options
 
 type plainlen = n:nat{n <= max_TLSPlaintext_fragment_length}
 (* irreducible *)

diff --git a/src/tls/FFI.fst b/src/tls/FFI.fst
@@ -350,17 +350,19 @@ let ffiSetNamedGroups cfg x =
     offer_shares = ogl;
   }
 
-private
-let encodeALPN x =
-    if String.length x < 256 then utf8_encode x
-    else failwith ("ffiSetALPN: protocol <"^x^"> is too long")
+private let encodeALPN x =
+  if String.length x < 256 then utf8_encode x
+  else failwith ("ffiSetALPN: protocol <"^x^"> is too long")
 
-val ffiSetALPN: cfg:config -> x:string -> ML config
-let ffiSetALPN cfg x =
+val ffiSplitALPN: config -> string -> ML alpn
+let ffiSplitALPN cfg x =
   let apl = if x = "" then [] else split_string ':' x in
   if List.Tot.length apl > 255 then failwith "ffiSetALPN: too many entries";
-  let apl = map encodeALPN apl in
-  { cfg with alpn = if apl=[] then None else Some apl }
+  map encodeALPN apl
+
+val ffiSetALPN: config -> alpn -> ML config
+let ffiSetALPN cfg x =
+  { cfg with alpn = if x = [] then None else Some x }
 
 val ffiSetEarlyData: cfg:config -> x:UInt32.t -> ML config
 let ffiSetEarlyData cfg x =
@@ -383,6 +385,12 @@ let ffiSetTicketKey a k =
   | None -> false
   | Some a -> TLS.set_ticket_key a k)
 
+val ffiSetSealingKey: a:string -> k:bytes -> ML bool
+let ffiSetSealingKey a k =
+  (match findsetting a aeads with
+  | None -> false
+  | Some a -> TLS.set_sealing_key a k)
+
 let ffiSetTicket (cfg:config) (tid:bytes) (si:bytes) : ML config =
   {cfg with use_tickets = (tid,si) :: cfg.use_tickets}
 
@@ -426,28 +434,6 @@ let ffiSetCertCallbacks (cfg:config) (cb:cert_cb) =
   trace "Setting up certificate callbacks.";
   {cfg with cert_callbacks = cb}
 
-// ADL july 24: now returns both the ticket and the
-// entry in the PSK database to allow inter-process ticket reuse
-// Beware! this exports crypto materials!
-(*
-let ffiGetTicket c: ML (option (ticket:bytes * rms:bytes)) =
-  match (Connection.c_cfg c).peer_name with
-  | Some n ->
-    (match Ticket.lookup n with
-    | Some (t, true) ->
-      (match PSK.psk_lookup t with
-      | None -> None
-      | Some ctx ->
-        let ae = ctx.PSK.early_ae in
-        let h = ctx.PSK.early_hash in
-        let pskb = PSK.psk_value t in
-        let (| li, rmsid |) = Ticket.dummy_rmsid ae h in
-        let si = Ticket.serialize (Ticket.Ticket13 (CipherSuite13 ae h) li rmsid psk) in
-        Some (t, si))
-    | _ -> None)
-  | None -> None
-*)
-
 val ffiGetCert: Connection.connection -> ML cbytes
 let ffiGetCert c =
   let cert = getCert c in
@@ -479,7 +465,7 @@ let ffiTicketInfoBytes (info:ticketInfo) (key:bytes) =
     | TicketInfo_12 (pv, cs, ems) ->
       Ticket.Ticket12 pv cs ems (Ticket.dummy_msId pv cs ems) key
     in
-  Ticket.ticket_encrypt (Ticket.serialize si)
+  Ticket.create_ticket true si
 
 let ffiSplitChain (chain:bytes) : ML (list cert_repr) =
   match Cert.parseCertificateList chain with

diff --git a/src/tls/Handshake.fst b/src/tls/Handshake.fst
@@ -1111,7 +1111,7 @@ let server_ClientFinished hs cvd digestCCS digestClientFinished =
           let ticket = Ticket.Ticket12 pv cs (Nego.emsFlag mode) msId ms in
           let ticket = {
             sticket_lifetime = FStar.UInt32.(uint_to_t 3600);
-            sticket_ticket = Ticket.create_ticket ticket;
+            sticket_ticket = Ticket.create_ticket false ticket;
           } in
           HandshakeLog.send_tag #ha hs.log (NewSessionTicket ticket)
         else digestClientFinished in
@@ -1209,7 +1209,7 @@ let server_ClientFinished_13 hs f digestBeforeClientFinished digestClientFinishe
            let age_add = uint32_of_bytes age_add in
            let now = CoreCrypto.now () in
            let ticket = Ticket.Ticket13 cs li rmsid rms empty_bytes now age_add empty_bytes in
-           let tb = Ticket.create_ticket ticket in
+           let tb = Ticket.create_ticket false ticket in
 
            trace ("Sending ticket: "^(print_bytes tb));
            let ticket_ext =

diff --git a/src/tls/Makefile b/src/tls/Makefile
@@ -21,7 +21,7 @@ quic-%: clean-depend
 test: clean-depend model-test kremlin-test ocaml-test quic-test
 
 clean: ocaml-clean kremlin-clean quic-clean model-clean
-	rm -rf $(EXTRACT_DIR)/Kremlin $(EXTRACT_DIR)/OCaml $(EXTRACT_DIR)/copied
+	rm -rf extract/Kremlin extract/OCaml extract/copied
 
 %.fst-in %.fsti-in:
 	$(MAKE) -f Makefile.$(FLAVOR) $@

diff --git a/src/tls/Makefile.Kremlin b/src/tls/Makefile.Kremlin
@@ -100,7 +100,7 @@ ALL_EXTERNAL_FILES	= \
     Crypto_HKDF_Crypto_HMAC.c Crypto_HKDF_Crypto_HMAC.h) \
   $(addprefix curve/,Hacl_Curve25519.c Hacl_Curve25519.h) \
   $(addprefix kremlib/,kremstr.c kremdate.c) \
-  kreminc/kremlib.h \
+  $(addprefix kreminc/,kremlib.h) \
   $(addprefix kreminc/kremlin/,c.h c_endianness.h c_string.h fstar_bytes.h \
     fstar_char.h fstar_dyn.h fstar_ints.h fstar_uint128.h prims_int.h prims_string.h \
     testlib.h \
@@ -109,7 +109,7 @@ ALL_EXTERNAL_FILES	= \
     buffer_bytes.c RegionAllocator.c RegionAllocator.h) \
   $(addprefix include/,hacl_glue.h hacks.h regions.h) \
   $(addprefix vale/,sha256_main_i.c sha256_main_i.h sha256-$(MARCH)$(VARIANT).S \
-    Vale_Hash_SHA2_256.c vale_aes_glue.c aes-$(MARCH)$(VARIANT).S DafnyLib.h) \
+    Vale_Hash_SHA2_256.c vale_aes_glue.c aesgcm-$(MARCH)$(VARIANT).S aes-$(MARCH)$(VARIANT).S DafnyLib.h) \
   $(addprefix pki/,mipki.h) \
   $(addprefix ffi/,mitlsffi.h)
 

diff --git a/src/tls/Makefile.OCaml b/src/tls/Makefile.OCaml
@@ -10,7 +10,7 @@ FLAVOR=OCaml
 EXTENSION=ml
 #Don't extract modules from fstarlib (NOEXTRACT_MODULES)
 #And also some specific ones from mitls that are implemented in C
-EXTRACT='* -Prims -FStar +FStar.Test +FStar.Kremlin.Endianness -CoreCrypto -CryptoTypes -DHDB -LowCProvider -HaclProvider -FFICallbacks -Crypto.AEAD -Crypto.Symmetric -Crypto.Plain -Spec.Loops -Buffer.Utils -C +C.Loops -LowParse.SLow.Tac -BufferBytes'
+EXTRACT='* -Prims -FStar +FStar.Test +FStar.Kremlin.Endianness -CoreCrypto -CryptoTypes -EverCrypt.Bytes -EverCrypt -DHDB -LowCProvider -HaclProvider -FFICallbacks -Crypto.AEAD -Crypto.Symmetric -Crypto.Plain -Spec.Loops -Buffer.Utils -C +C.Loops -LowParse.SLow.Tac -BufferBytes'
 SPECINC=$(MITLS_HOME)/src/tls/concrete-flags  $(MITLS_HOME)/src/tls/concrete-flags/OCaml
 include Makefile.common
 VFLAGS+=--admit_smt_queries true
@@ -197,14 +197,19 @@ UNAME = $(shell uname)
 
 ifeq ($(OS),Windows_NT)
   ifeq ($(shell uname -o),Cygwin)
-    MITLS_HOME_RUN := $(shell cygpath -u ${MITLS_HOME})
-    EVERCRYPT_HOME_RUN := $(shell cygpath -u ${EVERCRYPT_HOME})
+    MITLS_HOME_RUN := $(shell cygpath -a -u ${MITLS_HOME})
+    EVERCRYPT_HOME_RUN := $(shell cygpath -a -u ${EVERCRYPT_HOME})
+    MLCRYPTO_HOME_RUN := $(shell cygpath -a -u ${MLCRYPTO_HOME})
+  else
+    MITLS_HOME_RUN := $(MITLS_HOME)
+    EVERCRYPT_HOME_RUN := $(EVERCRYPT_HOME)
+    MLCRYPTO_HOME_RUN := $(MLCRYPTO_HOME)
   endif
-  export PATH := $(EVERCRYPT_HOME_RUN)/out:$(MITLS_HOME_RUN)/src/pki:$(PATH)
+  export PATH := $(MLCRYPTO_HOME_RUN)/openssl:$(EVERCRYPT_HOME_RUN)/out:$(MITLS_HOME_RUN)/src/pki:$(PATH)
 else ifeq ($(UNAME),Darwin)
-  PREFIX = DYLD_LIBRARY_PATH=$(EVERCRYPT_HOME)/out:$(MITLS_HOME)/src/pki:$(DYLD_LIBRARY_PATH)
+  PREFIX = DYLD_LIBRARY_PATH=$(MLCRYPTO_HOME)/openssl:$(EVERCRYPT_HOME)/out:$(MITLS_HOME)/src/pki:$(DYLD_LIBRARY_PATH)
 else ifeq ($(UNAME),Linux)
-  export LD_LIBRARY_PATH := $(EVERCRYPT_HOME)/out:$(MITLS_HOME)/src/pki:$(LD_LIBRARY_PATH)
+  export LD_LIBRARY_PATH := $(MLCRYPTO_HOME)/openssl:$(EVERCRYPT_HOME)/out:$(MITLS_HOME)/src/pki:$(LD_LIBRARY_PATH)
 endif
 
 test: mitls.exe $(CERT_FILES)