diff --git a/hax-driver.py b/hax-driver.py index 40df8f1..50ce48d 100755 --- a/hax-driver.py +++ b/hax-driver.py @@ -97,7 +97,7 @@ def shell(command, expect=0, cwd=None, env={}): "-**::non_hax::** -bertie::stream::**", "fstar", "--interfaces", - "+** +!bertie::tls13crypto::** +!bertie::tls13utils::**" + "+** +!bertie::tls13crypto::** +!bertie::tls13utils::** +!bertie::tls13cert::**" ], cwd=".", env=hax_env, diff --git a/proofs/fstar/extraction/Bertie.Tls13cert.fst b/proofs/fstar/extraction/Bertie.Tls13cert.fst deleted file mode 100644 index b35fd8f..0000000 --- a/proofs/fstar/extraction/Bertie.Tls13cert.fst +++ /dev/null @@ -1,993 +0,0 @@ -module Bertie.Tls13cert -#set-options "--fuel 0 --ifuel 1 --z3rlimit 15 --admit_smt_queries true" -open Core -open FStar.Mul - -let _ = - (* This module has implicit dependencies, here we make them explicit. *) - (* The implicit dependencies arise from typeclasses instances. *) - let open Bertie.Tls13utils in - () - -let asn1_error (#v_T: Type0) (err: u8) = Core.Result.Result_Err err <: Core.Result.t_Result v_T u8 - -let check_success (v_val: bool) = - if v_val - then Core.Result.Result_Ok (() <: Prims.unit) <: Core.Result.t_Result Prims.unit u8 - else asn1_error #Prims.unit v_ASN1_ERROR - -let check_tag (b: Bertie.Tls13utils.t_Bytes) (offset: usize) (value: u8) = - if (Bertie.Tls13utils.impl__Bytes__len b <: usize) >. offset - then - if - (Bertie.Tls13utils.f_declassify #u8 #u8 #FStar.Tactics.Typeclasses.solve (b.[ offset ] <: u8) - <: - u8) =. - value - then Core.Result.Result_Ok (() <: Prims.unit) <: Core.Result.t_Result Prims.unit u8 - else asn1_error #Prims.unit v_ASN1_INVALID_TAG - else asn1_error #Prims.unit v_ASN1_INVALID_TAG - -let length_length (b: Bertie.Tls13utils.t_Bytes) (offset: usize) = - if (Bertie.Tls13utils.impl__Bytes__len b <: usize) >. offset - then - if - ((Bertie.Tls13utils.f_declassify #u8 #u8 #FStar.Tactics.Typeclasses.solve (b.[ offset ] <: u8) - <: - u8) >>! - 7l - <: - u8) =. - 1uy - then - Core.Result.Result_Ok - (cast ((Bertie.Tls13utils.f_declassify #u8 - #u8 - #FStar.Tactics.Typeclasses.solve - (b.[ offset ] <: u8) - <: - u8) &. - 127uy - <: - u8) - <: - usize) - <: - Core.Result.t_Result usize u8 - else Core.Result.Result_Ok (sz 0) <: Core.Result.t_Result usize u8 - else asn1_error #usize v_ASN1_ERROR - -let short_length (b: Bertie.Tls13utils.t_Bytes) (offset: usize) = - if (Bertie.Tls13utils.impl__Bytes__len b <: usize) >. offset - then - if - ((Bertie.Tls13utils.f_declassify #u8 #u8 #FStar.Tactics.Typeclasses.solve (b.[ offset ] <: u8) - <: - u8) &. - 128uy - <: - u8) =. - 0uy - then - Core.Result.Result_Ok - (cast ((Bertie.Tls13utils.f_declassify #u8 - #u8 - #FStar.Tactics.Typeclasses.solve - (b.[ offset ] <: u8) - <: - u8) &. - 127uy - <: - u8) - <: - usize) - <: - Core.Result.t_Result usize u8 - else asn1_error #usize v_ASN1_ERROR - else asn1_error #usize v_ASN1_ERROR - -[@@ FStar.Tactics.Typeclasses.tcinstance] -assume -val impl': Core.Clone.t_Clone t_CertificateKey - -let impl = impl' - -[@@ FStar.Tactics.Typeclasses.tcinstance] -assume -val impl_1': Core.Marker.t_Copy t_CertificateKey - -let impl_1 = impl_1' - -let ecdsa_public_key (cert: Bertie.Tls13utils.t_Bytes) (indices: t_CertificateKey) = - let CertificateKey offset len:t_CertificateKey = indices in - match check_tag cert offset 4uy <: Core.Result.t_Result Prims.unit u8 with - | Core.Result.Result_Ok _ -> - Core.Result.Result_Ok - (Bertie.Tls13utils.impl__Bytes__slice cert (offset +! sz 1 <: usize) (len -! sz 1 <: usize)) - <: - Core.Result.t_Result Bertie.Tls13utils.t_Bytes u8 - | Core.Result.Result_Err err -> - Core.Result.Result_Err err <: Core.Result.t_Result Bertie.Tls13utils.t_Bytes u8 - -let read_octet_header (b: Bertie.Tls13utils.t_Bytes) (offset: usize) = - match check_tag b offset 4uy <: Core.Result.t_Result Prims.unit u8 with - | Core.Result.Result_Ok _ -> - let offset:usize = offset +! sz 1 in - (match length_length b offset <: Core.Result.t_Result usize u8 with - | Core.Result.Result_Ok length_length -> - let offset:usize = (offset +! length_length <: usize) +! sz 1 in - Core.Result.Result_Ok offset <: Core.Result.t_Result usize u8 - | Core.Result.Result_Err err -> Core.Result.Result_Err err <: Core.Result.t_Result usize u8) - | Core.Result.Result_Err err -> Core.Result.Result_Err err <: Core.Result.t_Result usize u8 - -let read_sequence_header (b: Bertie.Tls13utils.t_Bytes) (offset: usize) = - match check_tag b offset 48uy <: Core.Result.t_Result Prims.unit u8 with - | Core.Result.Result_Ok _ -> - let offset:usize = offset +! sz 1 in - (match length_length b offset <: Core.Result.t_Result usize u8 with - | Core.Result.Result_Ok length_length -> - let offset:usize = (offset +! length_length <: usize) +! sz 1 in - Core.Result.Result_Ok offset <: Core.Result.t_Result usize u8 - | Core.Result.Result_Err err -> Core.Result.Result_Err err <: Core.Result.t_Result usize u8) - | Core.Result.Result_Err err -> Core.Result.Result_Err err <: Core.Result.t_Result usize u8 - -let read_version_number (b: Bertie.Tls13utils.t_Bytes) (offset: usize) = - match check_tag b offset 160uy <: Core.Result.t_Result Prims.unit u8 with - | Core.Result.Result_Ok _ -> - let offset:usize = offset +! sz 1 in - (match short_length b offset <: Core.Result.t_Result usize u8 with - | Core.Result.Result_Ok length -> - Core.Result.Result_Ok ((offset +! sz 1 <: usize) +! length) <: Core.Result.t_Result usize u8 - | Core.Result.Result_Err err -> Core.Result.Result_Err err <: Core.Result.t_Result usize u8) - | Core.Result.Result_Err _ -> Core.Result.Result_Ok offset <: Core.Result.t_Result usize u8 - -let long_length (b: Bertie.Tls13utils.t_Bytes) (offset len: usize) = - if len >. sz 4 - then asn1_error #usize v_ASN1_SEQUENCE_TOO_LONG - else - if (Bertie.Tls13utils.impl__Bytes__len b <: usize) >=. (offset +! len <: usize) - then - let u32word:t_Array u8 (sz 4) = - Rust_primitives.Hax.repeat (Bertie.Tls13utils.v_U8 0uy <: u8) (sz 4) - in - let u32word:t_Array u8 (sz 4) = - Rust_primitives.Hax.Monomorphized_update_at.update_at_range u32word - ({ Core.Ops.Range.f_start = sz 0; Core.Ops.Range.f_end = len } - <: - Core.Ops.Range.t_Range usize) - (Core.Slice.impl__copy_from_slice #u8 - (u32word.[ { Core.Ops.Range.f_start = sz 0; Core.Ops.Range.f_end = len } - <: - Core.Ops.Range.t_Range usize ] - <: - t_Slice u8) - (b.[ { - Core.Ops.Range.f_start = offset; - Core.Ops.Range.f_end = offset +! len <: usize - } - <: - Core.Ops.Range.t_Range usize ] - <: - t_Slice u8) - <: - t_Slice u8) - in - Core.Result.Result_Ok - ((cast (Bertie.Tls13utils.f_declassify #u32 - #u32 - #FStar.Tactics.Typeclasses.solve - (Bertie.Tls13utils.u32_from_be_bytes u32word <: u32) - <: - u32) - <: - usize) >>! - ((sz 4 -! len <: usize) *! sz 8 <: usize)) - <: - Core.Result.t_Result usize u8 - else asn1_error #usize v_ASN1_ERROR - -let length (b: Bertie.Tls13utils.t_Bytes) (offset: usize) = - if (Bertie.Tls13utils.impl__Bytes__len b <: usize) >. offset - then - if - ((Bertie.Tls13utils.f_declassify #u8 #u8 #FStar.Tactics.Typeclasses.solve (b.[ offset ] <: u8) - <: - u8) &. - 128uy - <: - u8) =. - 0uy - then - match short_length b offset <: Core.Result.t_Result usize u8 with - | Core.Result.Result_Ok len -> - Core.Result.Result_Ok (offset +! sz 1, len <: (usize & usize)) - <: - Core.Result.t_Result (usize & usize) u8 - | Core.Result.Result_Err err -> - Core.Result.Result_Err err <: Core.Result.t_Result (usize & usize) u8 - else - match length_length b offset <: Core.Result.t_Result usize u8 with - | Core.Result.Result_Ok len -> - let offset:usize = offset +! sz 1 in - (match long_length b offset len <: Core.Result.t_Result usize u8 with - | Core.Result.Result_Ok v_end -> - Core.Result.Result_Ok (offset +! len, v_end <: (usize & usize)) - <: - Core.Result.t_Result (usize & usize) u8 - | Core.Result.Result_Err err -> - Core.Result.Result_Err err <: Core.Result.t_Result (usize & usize) u8) - | Core.Result.Result_Err err -> - Core.Result.Result_Err err <: Core.Result.t_Result (usize & usize) u8 - else asn1_error #(usize & usize) v_ASN1_ERROR - -let read_integer (b: Bertie.Tls13utils.t_Bytes) (offset: usize) = - match check_tag b offset 2uy <: Core.Result.t_Result Prims.unit u8 with - | Core.Result.Result_Ok _ -> - let offset:usize = offset +! sz 1 in - (match length b offset <: Core.Result.t_Result (usize & usize) u8 with - | Core.Result.Result_Ok (offset, length) -> - Core.Result.Result_Ok (Bertie.Tls13utils.impl__Bytes__slice b offset length) - <: - Core.Result.t_Result Bertie.Tls13utils.t_Bytes u8 - | Core.Result.Result_Err err -> - Core.Result.Result_Err err <: Core.Result.t_Result Bertie.Tls13utils.t_Bytes u8) - | Core.Result.Result_Err err -> - Core.Result.Result_Err err <: Core.Result.t_Result Bertie.Tls13utils.t_Bytes u8 - -let rsa_public_key (cert: Bertie.Tls13utils.t_Bytes) (indices: t_CertificateKey) = - let CertificateKey offset v__len:t_CertificateKey = indices in - match check_tag cert offset 48uy <: Core.Result.t_Result Prims.unit u8 with - | Core.Result.Result_Ok _ -> - let offset:usize = offset +! sz 1 in - (match length cert offset <: Core.Result.t_Result (usize & usize) u8 with - | Core.Result.Result_Ok (offset, v__seq_len) -> - (match check_tag cert offset 2uy <: Core.Result.t_Result Prims.unit u8 with - | Core.Result.Result_Ok _ -> - let offset:usize = offset +! sz 1 in - (match length cert offset <: Core.Result.t_Result (usize & usize) u8 with - | Core.Result.Result_Ok (offset, int_len) -> - let n:Bertie.Tls13utils.t_Bytes = - Bertie.Tls13utils.impl__Bytes__slice cert offset int_len - in - let offset:usize = offset +! int_len in - (match check_tag cert offset 2uy <: Core.Result.t_Result Prims.unit u8 with - | Core.Result.Result_Ok _ -> - let offset:usize = offset +! sz 1 in - (match length cert offset <: Core.Result.t_Result (usize & usize) u8 with - | Core.Result.Result_Ok (offset, int_len) -> - let e:Bertie.Tls13utils.t_Bytes = - Bertie.Tls13utils.impl__Bytes__slice cert offset int_len - in - Core.Result.Result_Ok - ({ Bertie.Tls13crypto.f_modulus = n; Bertie.Tls13crypto.f_exponent = e } - <: - Bertie.Tls13crypto.t_RsaVerificationKey) - <: - Core.Result.t_Result Bertie.Tls13crypto.t_RsaVerificationKey u8 - | Core.Result.Result_Err err -> - Core.Result.Result_Err err - <: - Core.Result.t_Result Bertie.Tls13crypto.t_RsaVerificationKey u8) - | Core.Result.Result_Err err -> - Core.Result.Result_Err err - <: - Core.Result.t_Result Bertie.Tls13crypto.t_RsaVerificationKey u8) - | Core.Result.Result_Err err -> - Core.Result.Result_Err err - <: - Core.Result.t_Result Bertie.Tls13crypto.t_RsaVerificationKey u8) - | Core.Result.Result_Err err -> - Core.Result.Result_Err err - <: - Core.Result.t_Result Bertie.Tls13crypto.t_RsaVerificationKey u8) - | Core.Result.Result_Err err -> - Core.Result.Result_Err err - <: - Core.Result.t_Result Bertie.Tls13crypto.t_RsaVerificationKey u8) - | Core.Result.Result_Err err -> - Core.Result.Result_Err err <: Core.Result.t_Result Bertie.Tls13crypto.t_RsaVerificationKey u8 - -let cert_public_key - (certificate: Bertie.Tls13utils.t_Bytes) - (spki: (Bertie.Tls13crypto.t_SignatureScheme & t_CertificateKey)) - = - match spki._1 <: Bertie.Tls13crypto.t_SignatureScheme with - | Bertie.Tls13crypto.SignatureScheme_ED25519 -> - asn1_error #Bertie.Tls13crypto.t_PublicVerificationKey v_ASN1_UNSUPPORTED_ALGORITHM - | Bertie.Tls13crypto.SignatureScheme_EcdsaSecp256r1Sha256 -> - (match - ecdsa_public_key certificate spki._2 <: Core.Result.t_Result Bertie.Tls13utils.t_Bytes u8 - with - | Core.Result.Result_Ok pk -> - Core.Result.Result_Ok - (Bertie.Tls13crypto.PublicVerificationKey_EcDsa pk - <: - Bertie.Tls13crypto.t_PublicVerificationKey) - <: - Core.Result.t_Result Bertie.Tls13crypto.t_PublicVerificationKey u8 - | Core.Result.Result_Err err -> - Core.Result.Result_Err err - <: - Core.Result.t_Result Bertie.Tls13crypto.t_PublicVerificationKey u8) - | Bertie.Tls13crypto.SignatureScheme_RsaPssRsaSha256 -> - match - rsa_public_key certificate spki._2 - <: - Core.Result.t_Result Bertie.Tls13crypto.t_RsaVerificationKey u8 - with - | Core.Result.Result_Ok pk -> - Core.Result.Result_Ok - (Bertie.Tls13crypto.PublicVerificationKey_Rsa pk <: Bertie.Tls13crypto.t_PublicVerificationKey - ) - <: - Core.Result.t_Result Bertie.Tls13crypto.t_PublicVerificationKey u8 - | Core.Result.Result_Err err -> - Core.Result.Result_Err err - <: - Core.Result.t_Result Bertie.Tls13crypto.t_PublicVerificationKey u8 - -let skip_integer (b: Bertie.Tls13utils.t_Bytes) (offset: usize) = - match check_tag b offset 2uy <: Core.Result.t_Result Prims.unit u8 with - | Core.Result.Result_Ok _ -> - let offset:usize = offset +! sz 1 in - (match length b offset <: Core.Result.t_Result (usize & usize) u8 with - | Core.Result.Result_Ok (offset, length) -> - Core.Result.Result_Ok (offset +! length) <: Core.Result.t_Result usize u8 - | Core.Result.Result_Err err -> Core.Result.Result_Err err <: Core.Result.t_Result usize u8) - | Core.Result.Result_Err err -> Core.Result.Result_Err err <: Core.Result.t_Result usize u8 - -let skip_sequence (b: Bertie.Tls13utils.t_Bytes) (offset: usize) = - match check_tag b offset 48uy <: Core.Result.t_Result Prims.unit u8 with - | Core.Result.Result_Ok _ -> - let offset:usize = offset +! sz 1 in - (match length b offset <: Core.Result.t_Result (usize & usize) u8 with - | Core.Result.Result_Ok (offset, length) -> - Core.Result.Result_Ok (offset +! length) <: Core.Result.t_Result usize u8 - | Core.Result.Result_Err err -> Core.Result.Result_Err err <: Core.Result.t_Result usize u8) - | Core.Result.Result_Err err -> Core.Result.Result_Err err <: Core.Result.t_Result usize u8 - -let rsa_private_key (key: Bertie.Tls13utils.t_Bytes) = - match read_sequence_header key (sz 0) <: Core.Result.t_Result usize u8 with - | Core.Result.Result_Ok offset -> - (match skip_integer key offset <: Core.Result.t_Result usize u8 with - | Core.Result.Result_Ok hoist50 -> - let offset:usize = hoist50 in - (match skip_sequence key offset <: Core.Result.t_Result usize u8 with - | Core.Result.Result_Ok hoist51 -> - let offset:usize = hoist51 in - (match read_octet_header key offset <: Core.Result.t_Result usize u8 with - | Core.Result.Result_Ok hoist52 -> - let offset:usize = hoist52 in - (match read_sequence_header key offset <: Core.Result.t_Result usize u8 with - | Core.Result.Result_Ok hoist53 -> - let offset:usize = hoist53 in - (match skip_integer key offset <: Core.Result.t_Result usize u8 with - | Core.Result.Result_Ok hoist54 -> - let offset:usize = hoist54 in - (match skip_integer key offset <: Core.Result.t_Result usize u8 with - | Core.Result.Result_Ok hoist55 -> - let offset:usize = hoist55 in - (match skip_integer key offset <: Core.Result.t_Result usize u8 with - | Core.Result.Result_Ok hoist56 -> - let offset:usize = hoist56 in - read_integer key offset - | Core.Result.Result_Err err -> - Core.Result.Result_Err err - <: - Core.Result.t_Result Bertie.Tls13utils.t_Bytes u8) - | Core.Result.Result_Err err -> - Core.Result.Result_Err err - <: - Core.Result.t_Result Bertie.Tls13utils.t_Bytes u8) - | Core.Result.Result_Err err -> - Core.Result.Result_Err err - <: - Core.Result.t_Result Bertie.Tls13utils.t_Bytes u8) - | Core.Result.Result_Err err -> - Core.Result.Result_Err err <: Core.Result.t_Result Bertie.Tls13utils.t_Bytes u8) - | Core.Result.Result_Err err -> - Core.Result.Result_Err err <: Core.Result.t_Result Bertie.Tls13utils.t_Bytes u8) - | Core.Result.Result_Err err -> - Core.Result.Result_Err err <: Core.Result.t_Result Bertie.Tls13utils.t_Bytes u8) - | Core.Result.Result_Err err -> - Core.Result.Result_Err err <: Core.Result.t_Result Bertie.Tls13utils.t_Bytes u8) - | Core.Result.Result_Err err -> - Core.Result.Result_Err err <: Core.Result.t_Result Bertie.Tls13utils.t_Bytes u8 - -let ecdsa_secp256r1_sha256_oid (_: Prims.unit) = - Core.Convert.f_into #(t_Array u8 (sz 8)) - #Bertie.Tls13utils.t_Bytes - #FStar.Tactics.Typeclasses.solve - (let list = [42uy; 134uy; 72uy; 206uy; 61uy; 3uy; 1uy; 7uy] in - FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 8); - Rust_primitives.Hax.array_of_list 8 list) - -let rsa_pkcs1_encryption_oid (_: Prims.unit) = - Core.Convert.f_into #(t_Array u8 (sz 9)) - #Bertie.Tls13utils.t_Bytes - #FStar.Tactics.Typeclasses.solve - (let list = [42uy; 134uy; 72uy; 134uy; 247uy; 13uy; 1uy; 1uy; 1uy] in - FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 9); - Rust_primitives.Hax.array_of_list 9 list) - -let x962_ec_public_key_oid (_: Prims.unit) = - Core.Convert.f_into #(t_Array u8 (sz 7)) - #Bertie.Tls13utils.t_Bytes - #FStar.Tactics.Typeclasses.solve - (let list = [42uy; 134uy; 72uy; 206uy; 61uy; 2uy; 1uy] in - FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 7); - Rust_primitives.Hax.array_of_list 7 list) - -let read_spki (cert: Bertie.Tls13utils.t_Bytes) (offset: usize) = - match check_tag cert offset 48uy <: Core.Result.t_Result Prims.unit u8 with - | Core.Result.Result_Ok _ -> - let offset:usize = offset +! sz 1 in - (match length cert offset <: Core.Result.t_Result (usize & usize) u8 with - | Core.Result.Result_Ok (offset, v__seq_len) -> - (match check_tag cert offset 48uy <: Core.Result.t_Result Prims.unit u8 with - | Core.Result.Result_Ok _ -> - let offset:usize = offset +! sz 1 in - (match length cert offset <: Core.Result.t_Result (usize & usize) u8 with - | Core.Result.Result_Ok (offset, seq_len) -> - (match check_tag cert offset 6uy <: Core.Result.t_Result Prims.unit u8 with - | Core.Result.Result_Ok _ -> - (match - length cert (offset +! sz 1 <: usize) - <: - Core.Result.t_Result (usize & usize) u8 - with - | Core.Result.Result_Ok (oid_offset, oid_len) -> - let ec_pk_oid, ecdsa_p256, rsa_pk_oid:(bool & bool & bool) = - false, false, false <: (bool & bool & bool) - in - let ec_oid:Bertie.Tls13utils.t_Bytes = x962_ec_public_key_oid () in - let rsa_oid:Bertie.Tls13utils.t_Bytes = rsa_pkcs1_encryption_oid () in - if (Bertie.Tls13utils.impl__Bytes__len ec_oid <: usize) =. oid_len - then - let ec_pk_oid:bool = true in - let ec_pk_oid:bool = - Rust_primitives.Hax.Folds.fold_range (sz 0) - (Bertie.Tls13utils.impl__Bytes__len ec_oid <: usize) - (fun ec_pk_oid temp_1_ -> - let ec_pk_oid:bool = ec_pk_oid in - let _:usize = temp_1_ in - true) - ec_pk_oid - (fun ec_pk_oid i -> - let ec_pk_oid:bool = ec_pk_oid in - let i:usize = i in - let oid_byte_equal:bool = - (Bertie.Tls13utils.f_declassify #u8 - #u8 - #FStar.Tactics.Typeclasses.solve - (cert.[ oid_offset +! i <: usize ] <: u8) - <: - u8) =. - (Bertie.Tls13utils.f_declassify #u8 - #u8 - #FStar.Tactics.Typeclasses.solve - (ec_oid.[ i ] <: u8) - <: - u8) - in - let ec_pk_oid:bool = ec_pk_oid && oid_byte_equal in - ec_pk_oid) - in - if ec_pk_oid - then - let oid_offset:usize = oid_offset +! oid_len in - match - check_tag cert oid_offset 6uy <: Core.Result.t_Result Prims.unit u8 - with - | Core.Result.Result_Ok _ -> - let oid_offset:usize = oid_offset +! sz 1 in - (match - length cert oid_offset <: Core.Result.t_Result (usize & usize) u8 - with - | Core.Result.Result_Ok (oid_offset, v__oid_len) -> - let ecdsa_p256:bool = true in - let ec_oid:Bertie.Tls13utils.t_Bytes = - ecdsa_secp256r1_sha256_oid () - in - let ecdsa_p256:bool = - Rust_primitives.Hax.Folds.fold_range (sz 0) - (Bertie.Tls13utils.impl__Bytes__len ec_oid <: usize) - (fun ecdsa_p256 temp_1_ -> - let ecdsa_p256:bool = ecdsa_p256 in - let _:usize = temp_1_ in - true) - ecdsa_p256 - (fun ecdsa_p256 i -> - let ecdsa_p256:bool = ecdsa_p256 in - let i:usize = i in - let oid_byte_equal:bool = - (Bertie.Tls13utils.f_declassify #u8 - #u8 - #FStar.Tactics.Typeclasses.solve - (cert.[ oid_offset +! i <: usize ] <: u8) - <: - u8) =. - (Bertie.Tls13utils.f_declassify #u8 - #u8 - #FStar.Tactics.Typeclasses.solve - (ec_oid.[ i ] <: u8) - <: - u8) - in - let ecdsa_p256:bool = ecdsa_p256 && oid_byte_equal in - ecdsa_p256) - in - (match - check_success ecdsa_p256 <: Core.Result.t_Result Prims.unit u8 - with - | Core.Result.Result_Ok _ -> - let ec_pk_oid, ecdsa_p256, oid_offset:(bool & bool & usize) = - ec_pk_oid, ecdsa_p256, oid_offset <: (bool & bool & usize) - in - let rsa_pk_oid:bool = - if - (Bertie.Tls13utils.impl__Bytes__len rsa_oid <: usize) =. - oid_len - then - let rsa_pk_oid:bool = true in - Rust_primitives.Hax.Folds.fold_range (sz 0) - (Bertie.Tls13utils.impl__Bytes__len rsa_oid <: usize) - (fun rsa_pk_oid temp_1_ -> - let rsa_pk_oid:bool = rsa_pk_oid in - let _:usize = temp_1_ in - true) - rsa_pk_oid - (fun rsa_pk_oid i -> - let rsa_pk_oid:bool = rsa_pk_oid in - let i:usize = i in - let oid_byte_equal:bool = - (Bertie.Tls13utils.f_declassify #u8 - #u8 - #FStar.Tactics.Typeclasses.solve - (cert.[ oid_offset +! i <: usize ] <: u8) - <: - u8) =. - (Bertie.Tls13utils.f_declassify #u8 - #u8 - #FStar.Tactics.Typeclasses.solve - (rsa_oid.[ i ] <: u8) - <: - u8) - in - let rsa_pk_oid:bool = - rsa_pk_oid && oid_byte_equal - in - rsa_pk_oid) - else rsa_pk_oid - in - (match - check_success (ec_pk_oid && ecdsa_p256 || rsa_pk_oid) - <: - Core.Result.t_Result Prims.unit u8 - with - | Core.Result.Result_Ok _ -> - let offset:usize = offset +! seq_len in - (match - check_tag cert offset 3uy - <: - Core.Result.t_Result Prims.unit u8 - with - | Core.Result.Result_Ok _ -> - let offset:usize = offset +! sz 1 in - (match - length cert offset - <: - Core.Result.t_Result (usize & usize) u8 - with - | Core.Result.Result_Ok (offset, bit_string_len) -> - let offset:usize = - if - (Bertie.Tls13utils.f_declassify #u8 - #u8 - #FStar.Tactics.Typeclasses.solve - (cert.[ offset ] <: u8) - <: - u8) =. - 0uy - then - let offset:usize = offset +! sz 1 in - offset - else offset - in - if ec_pk_oid && ecdsa_p256 - then - Core.Result.Result_Ok - ((Bertie.Tls13crypto.SignatureScheme_EcdsaSecp256r1Sha256 - <: - Bertie.Tls13crypto.t_SignatureScheme), - (CertificateKey offset - (bit_string_len -! sz 1) - <: - t_CertificateKey) - <: - (Bertie.Tls13crypto.t_SignatureScheme & - t_CertificateKey)) - <: - Core.Result.t_Result - (Bertie.Tls13crypto.t_SignatureScheme & - t_CertificateKey) u8 - else - if rsa_pk_oid - then - Core.Result.Result_Ok - ((Bertie.Tls13crypto.SignatureScheme_RsaPssRsaSha256 - <: - Bertie.Tls13crypto.t_SignatureScheme), - (CertificateKey offset - (bit_string_len -! sz 1) - <: - t_CertificateKey) - <: - (Bertie.Tls13crypto.t_SignatureScheme & - t_CertificateKey)) - <: - Core.Result.t_Result - (Bertie.Tls13crypto.t_SignatureScheme & - t_CertificateKey) u8 - else - asn1_error #(Bertie.Tls13crypto.t_SignatureScheme & - t_CertificateKey) - v_ASN1_INVALID_CERTIFICATE - | Core.Result.Result_Err err -> - Core.Result.Result_Err err - <: - Core.Result.t_Result - (Bertie.Tls13crypto.t_SignatureScheme & - t_CertificateKey) u8) - | Core.Result.Result_Err err -> - Core.Result.Result_Err err - <: - Core.Result.t_Result - (Bertie.Tls13crypto.t_SignatureScheme & - t_CertificateKey) u8) - | Core.Result.Result_Err err -> - Core.Result.Result_Err err - <: - Core.Result.t_Result - (Bertie.Tls13crypto.t_SignatureScheme & t_CertificateKey - ) u8) - | Core.Result.Result_Err err -> - Core.Result.Result_Err err - <: - Core.Result.t_Result - (Bertie.Tls13crypto.t_SignatureScheme & t_CertificateKey) u8 - ) - | Core.Result.Result_Err err -> - Core.Result.Result_Err err - <: - Core.Result.t_Result - (Bertie.Tls13crypto.t_SignatureScheme & t_CertificateKey) u8) - | Core.Result.Result_Err err -> - Core.Result.Result_Err err - <: - Core.Result.t_Result - (Bertie.Tls13crypto.t_SignatureScheme & t_CertificateKey) u8 - else - let ec_pk_oid, ecdsa_p256, oid_offset:(bool & bool & usize) = - ec_pk_oid, ecdsa_p256, oid_offset <: (bool & bool & usize) - in - let rsa_pk_oid:bool = - if (Bertie.Tls13utils.impl__Bytes__len rsa_oid <: usize) =. oid_len - then - let rsa_pk_oid:bool = true in - Rust_primitives.Hax.Folds.fold_range (sz 0) - (Bertie.Tls13utils.impl__Bytes__len rsa_oid <: usize) - (fun rsa_pk_oid temp_1_ -> - let rsa_pk_oid:bool = rsa_pk_oid in - let _:usize = temp_1_ in - true) - rsa_pk_oid - (fun rsa_pk_oid i -> - let rsa_pk_oid:bool = rsa_pk_oid in - let i:usize = i in - let oid_byte_equal:bool = - (Bertie.Tls13utils.f_declassify #u8 - #u8 - #FStar.Tactics.Typeclasses.solve - (cert.[ oid_offset +! i <: usize ] <: u8) - <: - u8) =. - (Bertie.Tls13utils.f_declassify #u8 - #u8 - #FStar.Tactics.Typeclasses.solve - (rsa_oid.[ i ] <: u8) - <: - u8) - in - let rsa_pk_oid:bool = rsa_pk_oid && oid_byte_equal in - rsa_pk_oid) - else rsa_pk_oid - in - match - check_success (ec_pk_oid && ecdsa_p256 || rsa_pk_oid) - <: - Core.Result.t_Result Prims.unit u8 - with - | Core.Result.Result_Ok _ -> - let offset:usize = offset +! seq_len in - (match - check_tag cert offset 3uy <: Core.Result.t_Result Prims.unit u8 - with - | Core.Result.Result_Ok _ -> - let offset:usize = offset +! sz 1 in - (match - length cert offset <: Core.Result.t_Result (usize & usize) u8 - with - | Core.Result.Result_Ok (offset, bit_string_len) -> - let offset:usize = - if - (Bertie.Tls13utils.f_declassify #u8 - #u8 - #FStar.Tactics.Typeclasses.solve - (cert.[ offset ] <: u8) - <: - u8) =. - 0uy - then - let offset:usize = offset +! sz 1 in - offset - else offset - in - if ec_pk_oid && ecdsa_p256 - then - Core.Result.Result_Ok - ((Bertie.Tls13crypto.SignatureScheme_EcdsaSecp256r1Sha256 - <: - Bertie.Tls13crypto.t_SignatureScheme), - (CertificateKey offset (bit_string_len -! sz 1) - <: - t_CertificateKey) - <: - (Bertie.Tls13crypto.t_SignatureScheme & t_CertificateKey)) - <: - Core.Result.t_Result - (Bertie.Tls13crypto.t_SignatureScheme & t_CertificateKey) - u8 - else - if rsa_pk_oid - then - Core.Result.Result_Ok - ((Bertie.Tls13crypto.SignatureScheme_RsaPssRsaSha256 - <: - Bertie.Tls13crypto.t_SignatureScheme), - (CertificateKey offset (bit_string_len -! sz 1) - <: - t_CertificateKey) - <: - (Bertie.Tls13crypto.t_SignatureScheme & t_CertificateKey - )) - <: - Core.Result.t_Result - (Bertie.Tls13crypto.t_SignatureScheme & t_CertificateKey - ) u8 - else - asn1_error #(Bertie.Tls13crypto.t_SignatureScheme & - t_CertificateKey) - v_ASN1_INVALID_CERTIFICATE - | Core.Result.Result_Err err -> - Core.Result.Result_Err err - <: - Core.Result.t_Result - (Bertie.Tls13crypto.t_SignatureScheme & t_CertificateKey) u8 - ) - | Core.Result.Result_Err err -> - Core.Result.Result_Err err - <: - Core.Result.t_Result - (Bertie.Tls13crypto.t_SignatureScheme & t_CertificateKey) u8) - | Core.Result.Result_Err err -> - Core.Result.Result_Err err - <: - Core.Result.t_Result - (Bertie.Tls13crypto.t_SignatureScheme & t_CertificateKey) u8 - else - let ec_pk_oid, ecdsa_p256, oid_offset:(bool & bool & usize) = - ec_pk_oid, ecdsa_p256, oid_offset <: (bool & bool & usize) - in - let rsa_pk_oid:bool = - if (Bertie.Tls13utils.impl__Bytes__len rsa_oid <: usize) =. oid_len - then - let rsa_pk_oid:bool = true in - Rust_primitives.Hax.Folds.fold_range (sz 0) - (Bertie.Tls13utils.impl__Bytes__len rsa_oid <: usize) - (fun rsa_pk_oid temp_1_ -> - let rsa_pk_oid:bool = rsa_pk_oid in - let _:usize = temp_1_ in - true) - rsa_pk_oid - (fun rsa_pk_oid i -> - let rsa_pk_oid:bool = rsa_pk_oid in - let i:usize = i in - let oid_byte_equal:bool = - (Bertie.Tls13utils.f_declassify #u8 - #u8 - #FStar.Tactics.Typeclasses.solve - (cert.[ oid_offset +! i <: usize ] <: u8) - <: - u8) =. - (Bertie.Tls13utils.f_declassify #u8 - #u8 - #FStar.Tactics.Typeclasses.solve - (rsa_oid.[ i ] <: u8) - <: - u8) - in - let rsa_pk_oid:bool = rsa_pk_oid && oid_byte_equal in - rsa_pk_oid) - else rsa_pk_oid - in - (match - check_success (ec_pk_oid && ecdsa_p256 || rsa_pk_oid) - <: - Core.Result.t_Result Prims.unit u8 - with - | Core.Result.Result_Ok _ -> - let offset:usize = offset +! seq_len in - (match - check_tag cert offset 3uy <: Core.Result.t_Result Prims.unit u8 - with - | Core.Result.Result_Ok _ -> - let offset:usize = offset +! sz 1 in - (match - length cert offset <: Core.Result.t_Result (usize & usize) u8 - with - | Core.Result.Result_Ok (offset, bit_string_len) -> - let offset:usize = - if - (Bertie.Tls13utils.f_declassify #u8 - #u8 - #FStar.Tactics.Typeclasses.solve - (cert.[ offset ] <: u8) - <: - u8) =. - 0uy - then - let offset:usize = offset +! sz 1 in - offset - else offset - in - if ec_pk_oid && ecdsa_p256 - then - Core.Result.Result_Ok - ((Bertie.Tls13crypto.SignatureScheme_EcdsaSecp256r1Sha256 - <: - Bertie.Tls13crypto.t_SignatureScheme), - (CertificateKey offset (bit_string_len -! sz 1) - <: - t_CertificateKey) - <: - (Bertie.Tls13crypto.t_SignatureScheme & t_CertificateKey)) - <: - Core.Result.t_Result - (Bertie.Tls13crypto.t_SignatureScheme & t_CertificateKey) - u8 - else - if rsa_pk_oid - then - Core.Result.Result_Ok - ((Bertie.Tls13crypto.SignatureScheme_RsaPssRsaSha256 - <: - Bertie.Tls13crypto.t_SignatureScheme), - (CertificateKey offset (bit_string_len -! sz 1) - <: - t_CertificateKey) - <: - (Bertie.Tls13crypto.t_SignatureScheme & t_CertificateKey - )) - <: - Core.Result.t_Result - (Bertie.Tls13crypto.t_SignatureScheme & t_CertificateKey - ) u8 - else - asn1_error #(Bertie.Tls13crypto.t_SignatureScheme & - t_CertificateKey) - v_ASN1_INVALID_CERTIFICATE - | Core.Result.Result_Err err -> - Core.Result.Result_Err err - <: - Core.Result.t_Result - (Bertie.Tls13crypto.t_SignatureScheme & t_CertificateKey) u8 - ) - | Core.Result.Result_Err err -> - Core.Result.Result_Err err - <: - Core.Result.t_Result - (Bertie.Tls13crypto.t_SignatureScheme & t_CertificateKey) u8) - | Core.Result.Result_Err err -> - Core.Result.Result_Err err - <: - Core.Result.t_Result - (Bertie.Tls13crypto.t_SignatureScheme & t_CertificateKey) u8) - | Core.Result.Result_Err err -> - Core.Result.Result_Err err - <: - Core.Result.t_Result - (Bertie.Tls13crypto.t_SignatureScheme & t_CertificateKey) u8) - | Core.Result.Result_Err err -> - Core.Result.Result_Err err - <: - Core.Result.t_Result (Bertie.Tls13crypto.t_SignatureScheme & t_CertificateKey) - u8) - | Core.Result.Result_Err err -> - Core.Result.Result_Err err - <: - Core.Result.t_Result (Bertie.Tls13crypto.t_SignatureScheme & t_CertificateKey) u8) - | Core.Result.Result_Err err -> - Core.Result.Result_Err err - <: - Core.Result.t_Result (Bertie.Tls13crypto.t_SignatureScheme & t_CertificateKey) u8) - | Core.Result.Result_Err err -> - Core.Result.Result_Err err - <: - Core.Result.t_Result (Bertie.Tls13crypto.t_SignatureScheme & t_CertificateKey) u8) - | Core.Result.Result_Err err -> - Core.Result.Result_Err err - <: - Core.Result.t_Result (Bertie.Tls13crypto.t_SignatureScheme & t_CertificateKey) u8 - -let verification_key_from_cert (cert: Bertie.Tls13utils.t_Bytes) = - match read_sequence_header cert (sz 0) <: Core.Result.t_Result usize u8 with - | Core.Result.Result_Ok offset -> - (match read_sequence_header cert offset <: Core.Result.t_Result usize u8 with - | Core.Result.Result_Ok hoist77 -> - let offset:usize = hoist77 in - (match read_version_number cert offset <: Core.Result.t_Result usize u8 with - | Core.Result.Result_Ok hoist78 -> - let offset:usize = hoist78 in - (match skip_integer cert offset <: Core.Result.t_Result usize u8 with - | Core.Result.Result_Ok hoist79 -> - let offset:usize = hoist79 in - (match skip_sequence cert offset <: Core.Result.t_Result usize u8 with - | Core.Result.Result_Ok hoist80 -> - let offset:usize = hoist80 in - (match skip_sequence cert offset <: Core.Result.t_Result usize u8 with - | Core.Result.Result_Ok hoist81 -> - let offset:usize = hoist81 in - (match skip_sequence cert offset <: Core.Result.t_Result usize u8 with - | Core.Result.Result_Ok hoist82 -> - let offset:usize = hoist82 in - (match skip_sequence cert offset <: Core.Result.t_Result usize u8 with - | Core.Result.Result_Ok hoist83 -> - let offset:usize = hoist83 in - read_spki cert offset - | Core.Result.Result_Err err -> - Core.Result.Result_Err err - <: - Core.Result.t_Result - (Bertie.Tls13crypto.t_SignatureScheme & t_CertificateKey) u8) - | Core.Result.Result_Err err -> - Core.Result.Result_Err err - <: - Core.Result.t_Result - (Bertie.Tls13crypto.t_SignatureScheme & t_CertificateKey) u8) - | Core.Result.Result_Err err -> - Core.Result.Result_Err err - <: - Core.Result.t_Result - (Bertie.Tls13crypto.t_SignatureScheme & t_CertificateKey) u8) - | Core.Result.Result_Err err -> - Core.Result.Result_Err err - <: - Core.Result.t_Result (Bertie.Tls13crypto.t_SignatureScheme & t_CertificateKey) - u8) - | Core.Result.Result_Err err -> - Core.Result.Result_Err err - <: - Core.Result.t_Result (Bertie.Tls13crypto.t_SignatureScheme & t_CertificateKey) u8) - | Core.Result.Result_Err err -> - Core.Result.Result_Err err - <: - Core.Result.t_Result (Bertie.Tls13crypto.t_SignatureScheme & t_CertificateKey) u8) - | Core.Result.Result_Err err -> - Core.Result.Result_Err err - <: - Core.Result.t_Result (Bertie.Tls13crypto.t_SignatureScheme & t_CertificateKey) u8) - | Core.Result.Result_Err err -> - Core.Result.Result_Err err - <: - Core.Result.t_Result (Bertie.Tls13crypto.t_SignatureScheme & t_CertificateKey) u8 diff --git a/proofs/fstar/extraction/Bertie.Tls13formats.Handshake_data.fst b/proofs/fstar/extraction/Bertie.Tls13formats.Handshake_data.fst index c0015cb..7e4d262 100644 --- a/proofs/fstar/extraction/Bertie.Tls13formats.Handshake_data.fst +++ b/proofs/fstar/extraction/Bertie.Tls13formats.Handshake_data.fst @@ -322,3 +322,35 @@ let impl__HandshakeData__from_bytes Core.Result.t_Result t_HandshakeData u8 | Core.Result.Result_Err err -> Core.Result.Result_Err err <: Core.Result.t_Result t_HandshakeData u8 + +let rec impl__HandshakeData__find_handshake_message + (self: t_HandshakeData) + (handshake_type: t_HandshakeType) + (start: usize) + = + if ((impl__HandshakeData__len self <: usize) -! start <: usize) <. sz 4 + then false + else + match + Bertie.Tls13utils.length_u24_encoded (Bertie.Tls13utils.impl__Bytes__raw_slice self._0 + ({ + Core.Ops.Range.f_start = start +! sz 1 <: usize; + Core.Ops.Range.f_end = Bertie.Tls13utils.impl__Bytes__len self._0 <: usize + } + <: + Core.Ops.Range.t_Range usize) + <: + t_Slice u8) + <: + Core.Result.t_Result usize u8 + with + | Core.Result.Result_Err _ -> false + | Core.Result.Result_Ok len -> + if + Bertie.Tls13utils.eq1 (self._0.[ start ] <: u8) + (Bertie.Tls13utils.v_U8 (t_HandshakeType_cast_to_repr handshake_type <: u8) <: u8) + then true + else + impl__HandshakeData__find_handshake_message self + handshake_type + ((start +! sz 4 <: usize) +! len <: usize) diff --git a/proofs/fstar/extraction/Bertie.Tls13formats.fst b/proofs/fstar/extraction/Bertie.Tls13formats.fst index 931a97d..4f308a7 100644 --- a/proofs/fstar/extraction/Bertie.Tls13formats.fst +++ b/proofs/fstar/extraction/Bertie.Tls13formats.fst @@ -378,6 +378,57 @@ let set_client_hello_binder Bertie.Tls13utils.tlserr #Bertie.Tls13formats.Handshake_data.t_HandshakeData (Bertie.Tls13utils.parse_failed () <: u8) +let check_server_name (extension: t_Slice u8) = + match + Bertie.Tls13utils.check_length_encoding_u16_slice extension + <: + Core.Result.t_Result Prims.unit u8 + with + | Core.Result.Result_Ok _ -> + if (Core.Slice.impl__len #u8 extension <: usize) >. sz 3 + then + match + Bertie.Tls13utils.check_eq1 (Bertie.Tls13utils.v_U8 0uy <: u8) (extension.[ sz 2 ] <: u8) + <: + Core.Result.t_Result Prims.unit u8 + with + | Core.Result.Result_Ok _ -> + (match + Bertie.Tls13utils.check_length_encoding_u16_slice (extension.[ { + Core.Ops.Range.f_start = sz 3; + Core.Ops.Range.f_end = Core.Slice.impl__len #u8 extension <: usize + } + <: + Core.Ops.Range.t_Range usize ] + <: + t_Slice u8) + <: + Core.Result.t_Result Prims.unit u8 + with + | Core.Result.Result_Ok _ -> + Core.Result.Result_Ok + (Core.Convert.f_into #(t_Slice u8) + #Bertie.Tls13utils.t_Bytes + #FStar.Tactics.Typeclasses.solve + (extension.[ { + Core.Ops.Range.f_start = sz 5; + Core.Ops.Range.f_end = Core.Slice.impl__len #u8 extension <: usize + } + <: + Core.Ops.Range.t_Range usize ] + <: + t_Slice u8)) + <: + Core.Result.t_Result Bertie.Tls13utils.t_Bytes u8 + | Core.Result.Result_Err err -> + Core.Result.Result_Err err <: Core.Result.t_Result Bertie.Tls13utils.t_Bytes u8) + | Core.Result.Result_Err err -> + Core.Result.Result_Err err <: Core.Result.t_Result Bertie.Tls13utils.t_Bytes u8 + else + Bertie.Tls13utils.tlserr #Bertie.Tls13utils.t_Bytes (Bertie.Tls13utils.parse_failed () <: u8) + | Core.Result.Result_Err err -> + Core.Result.Result_Err err <: Core.Result.t_Result Bertie.Tls13utils.t_Bytes u8 + let parse_server_certificate (certificate: Bertie.Tls13formats.Handshake_data.t_HandshakeData) = match Bertie.Tls13formats.Handshake_data.impl__HandshakeData__as_handshake_message certificate @@ -586,60 +637,6 @@ let check_psk_key_exchange_modes (client_hello: t_Slice u8) = (sz 2) | Core.Result.Result_Err err -> Core.Result.Result_Err err <: Core.Result.t_Result Prims.unit u8 -let check_server_name (extension: t_Slice u8) = - match - Bertie.Tls13utils.check_length_encoding_u16_slice extension - <: - Core.Result.t_Result Prims.unit u8 - with - | Core.Result.Result_Ok _ -> - (match - Bertie.Tls13utils.check_eq_with_slice ((let list = [Bertie.Tls13utils.v_U8 0uy] in - FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1); - Rust_primitives.Hax.array_of_list 1 list) - <: - t_Slice u8) - extension - (sz 2) - (sz 3) - <: - Core.Result.t_Result Prims.unit u8 - with - | Core.Result.Result_Ok _ -> - (match - Bertie.Tls13utils.check_length_encoding_u16_slice (extension.[ { - Core.Ops.Range.f_start = sz 3; - Core.Ops.Range.f_end = Core.Slice.impl__len #u8 extension <: usize - } - <: - Core.Ops.Range.t_Range usize ] - <: - t_Slice u8) - <: - Core.Result.t_Result Prims.unit u8 - with - | Core.Result.Result_Ok _ -> - Core.Result.Result_Ok - (Core.Convert.f_into #(t_Slice u8) - #Bertie.Tls13utils.t_Bytes - #FStar.Tactics.Typeclasses.solve - (extension.[ { - Core.Ops.Range.f_start = sz 5; - Core.Ops.Range.f_end = Core.Slice.impl__len #u8 extension <: usize - } - <: - Core.Ops.Range.t_Range usize ] - <: - t_Slice u8)) - <: - Core.Result.t_Result Bertie.Tls13utils.t_Bytes u8 - | Core.Result.Result_Err err -> - Core.Result.Result_Err err <: Core.Result.t_Result Bertie.Tls13utils.t_Bytes u8) - | Core.Result.Result_Err err -> - Core.Result.Result_Err err <: Core.Result.t_Result Bertie.Tls13utils.t_Bytes u8) - | Core.Result.Result_Err err -> - Core.Result.Result_Err err <: Core.Result.t_Result Bertie.Tls13utils.t_Bytes u8 - let check_server_psk_shared_key (v__algs: Bertie.Tls13crypto.t_Algorithms) (b: t_Slice u8) = Bertie.Tls13utils.check_eq_slice ((let list = [Bertie.Tls13utils.v_U8 0uy; Bertie.Tls13utils.v_U8 0uy] @@ -772,56 +769,61 @@ let server_certificate (v__algs: Bertie.Tls13crypto.t_Algorithms) (cert: Bertie. Core.Result.t_Result Bertie.Tls13formats.Handshake_data.t_HandshakeData u8 let check_server_key_share (algs: Bertie.Tls13crypto.t_Algorithms) (b: t_Slice u8) = - match - Bertie.Tls13crypto.impl__Algorithms__supported_group algs - <: - Core.Result.t_Result Bertie.Tls13utils.t_Bytes u8 - with - | Core.Result.Result_Ok hoist87 -> - (match - Bertie.Tls13utils.check_eq_with_slice (Bertie.Tls13utils.impl__Bytes__as_raw hoist87 - <: - t_Slice u8) - b - (sz 0) - (sz 2) - <: - Core.Result.t_Result Prims.unit u8 - with - | Core.Result.Result_Ok _ -> - (match - Bertie.Tls13utils.check_length_encoding_u16_slice (b.[ { - Core.Ops.Range.f_start = sz 2; - Core.Ops.Range.f_end = Core.Slice.impl__len #u8 b <: usize - } - <: - Core.Ops.Range.t_Range usize ] - <: - t_Slice u8) - <: - Core.Result.t_Result Prims.unit u8 - with - | Core.Result.Result_Ok _ -> - Core.Result.Result_Ok - (Core.Convert.f_from #Bertie.Tls13utils.t_Bytes - #(t_Slice u8) - #FStar.Tactics.Typeclasses.solve - (b.[ { - Core.Ops.Range.f_start = sz 4; + if (Core.Slice.impl__len #u8 b <: usize) >=. sz 2 + then + match + Bertie.Tls13crypto.impl__Algorithms__supported_group algs + <: + Core.Result.t_Result Bertie.Tls13utils.t_Bytes u8 + with + | Core.Result.Result_Ok hoist87 -> + (match + Bertie.Tls13utils.check_eq_with_slice (Bertie.Tls13utils.impl__Bytes__as_raw hoist87 + <: + t_Slice u8) + b + (sz 0) + (sz 2) + <: + Core.Result.t_Result Prims.unit u8 + with + | Core.Result.Result_Ok _ -> + (match + Bertie.Tls13utils.check_length_encoding_u16_slice (b.[ { + Core.Ops.Range.f_start = sz 2; Core.Ops.Range.f_end = Core.Slice.impl__len #u8 b <: usize } <: Core.Ops.Range.t_Range usize ] <: - t_Slice u8)) - <: - Core.Result.t_Result Bertie.Tls13utils.t_Bytes u8 - | Core.Result.Result_Err err -> - Core.Result.Result_Err err <: Core.Result.t_Result Bertie.Tls13utils.t_Bytes u8) - | Core.Result.Result_Err err -> - Core.Result.Result_Err err <: Core.Result.t_Result Bertie.Tls13utils.t_Bytes u8) - | Core.Result.Result_Err err -> - Core.Result.Result_Err err <: Core.Result.t_Result Bertie.Tls13utils.t_Bytes u8 + t_Slice u8) + <: + Core.Result.t_Result Prims.unit u8 + with + | Core.Result.Result_Ok _ -> + Core.Result.Result_Ok + (Core.Convert.f_from #Bertie.Tls13utils.t_Bytes + #(t_Slice u8) + #FStar.Tactics.Typeclasses.solve + (b.[ { + Core.Ops.Range.f_start = sz 4; + Core.Ops.Range.f_end = Core.Slice.impl__len #u8 b <: usize + } + <: + Core.Ops.Range.t_Range usize ] + <: + t_Slice u8)) + <: + Core.Result.t_Result Bertie.Tls13utils.t_Bytes u8 + | Core.Result.Result_Err err -> + Core.Result.Result_Err err <: Core.Result.t_Result Bertie.Tls13utils.t_Bytes u8) + | Core.Result.Result_Err err -> + Core.Result.Result_Err err <: Core.Result.t_Result Bertie.Tls13utils.t_Bytes u8) + | Core.Result.Result_Err err -> + Core.Result.Result_Err err <: Core.Result.t_Result Bertie.Tls13utils.t_Bytes u8 + else Bertie.Tls13utils.tlserr #Bertie.Tls13utils.t_Bytes (Bertie.Tls13utils.parse_failed () <: u8) + +#push-options "--admit_smt_queries true" let check_server_extension (algs: Bertie.Tls13crypto.t_Algorithms) (b: t_Slice u8) = if (Core.Slice.impl__len #u8 b <: usize) <. sz 4 @@ -940,6 +942,8 @@ let check_server_extension (algs: Bertie.Tls13crypto.t_Algorithms) (b: t_Slice u <: Core.Result.t_Result (usize & Core.Option.t_Option Bertie.Tls13utils.t_Bytes) u8 +#pop-options + let check_signature_algorithms (algs: Bertie.Tls13crypto.t_Algorithms) (ch: t_Slice u8) = match Bertie.Tls13utils.check_length_encoding_u16_slice ch <: Core.Result.t_Result Prims.unit u8 @@ -1414,6 +1418,8 @@ let parse_ecdsa_signature (sig: Bertie.Tls13utils.t_Bytes) = | Core.Result.Result_Err err -> Core.Result.Result_Err err <: Core.Result.t_Result Bertie.Tls13utils.t_Bytes u8 +#push-options "--admit_smt_queries true" + let parse_certificate_verify (algs: Bertie.Tls13crypto.t_Algorithms) (certificate_verify: Bertie.Tls13formats.Handshake_data.t_HandshakeData) @@ -1510,6 +1516,10 @@ let parse_certificate_verify | Core.Result.Result_Err err -> Core.Result.Result_Err err <: Core.Result.t_Result Bertie.Tls13utils.t_Bytes u8 +#pop-options + +#push-options "--admit_smt_queries true" + let parse_encrypted_extensions (v__algs: Bertie.Tls13crypto.t_Algorithms) (encrypted_extensions: Bertie.Tls13formats.Handshake_data.t_HandshakeData) @@ -1551,6 +1561,8 @@ let parse_encrypted_extensions t_Slice u8) | Core.Result.Result_Err err -> Core.Result.Result_Err err <: Core.Result.t_Result Prims.unit u8 +#pop-options + let check_handshake_record (p: Bertie.Tls13utils.t_Bytes) = if (Bertie.Tls13utils.impl__Bytes__len p <: usize) <. sz 5 then @@ -1982,6 +1994,8 @@ let server_supported_version (v__algorithms: Bertie.Tls13crypto.t_Algorithms) = | Core.Result.Result_Err err -> Core.Result.Result_Err err <: Core.Result.t_Result Bertie.Tls13utils.t_Bytes u8 +#push-options "--admit_smt_queries true" + let server_hello (algs: Bertie.Tls13crypto.t_Algorithms) (sr sid gy: Bertie.Tls13utils.t_Bytes) = let ver:Bertie.Tls13utils.t_Bytes = Bertie.Tls13utils.bytes2 3uy 3uy in match @@ -2160,6 +2174,8 @@ let server_hello (algs: Bertie.Tls13crypto.t_Algorithms) (sr sid gy: Bertie.Tls1 <: Core.Result.t_Result Bertie.Tls13formats.Handshake_data.t_HandshakeData u8 +#pop-options + let signature_algorithms (algs: Bertie.Tls13crypto.t_Algorithms) = match Bertie.Tls13crypto.impl__Algorithms__signature_algorithm algs @@ -2193,6 +2209,8 @@ let signature_algorithms (algs: Bertie.Tls13crypto.t_Algorithms) = | Core.Result.Result_Err err -> Core.Result.Result_Err err <: Core.Result.t_Result Bertie.Tls13utils.t_Bytes u8 +#push-options "--admit_smt_queries true" + let client_hello (algorithms: Bertie.Tls13crypto.t_Algorithms) (client_random kem_pk server_name: Bertie.Tls13utils.t_Bytes) @@ -2444,6 +2462,8 @@ let client_hello <: Core.Result.t_Result (Bertie.Tls13formats.Handshake_data.t_HandshakeData & usize) u8 +#pop-options + let rec check_server_extensions (algs: Bertie.Tls13crypto.t_Algorithms) (b: t_Slice u8) = match check_server_extension algs b @@ -2480,7 +2500,9 @@ let rec check_server_extensions (algs: Bertie.Tls13crypto.t_Algorithms) (b: t_Sl <: Core.Result.t_Result (Core.Option.t_Option Bertie.Tls13utils.t_Bytes) u8 -let rec find_key_share (g: Bertie.Tls13utils.t_Bytes) (ch: t_Slice u8) = +#push-options "--admit_smt_queries true" + +let find_key_share (g: Bertie.Tls13utils.t_Bytes) (ch: t_Slice u8) = if (Core.Slice.impl__len #u8 ch <: usize) <. sz 4 then Bertie.Tls13utils.tlserr #Bertie.Tls13utils.t_Bytes (Bertie.Tls13utils.parse_failed () <: u8) else @@ -2544,6 +2566,8 @@ let rec find_key_share (g: Bertie.Tls13utils.t_Bytes) (ch: t_Slice u8) = | Core.Result.Result_Err err -> Core.Result.Result_Err err <: Core.Result.t_Result Bertie.Tls13utils.t_Bytes u8 +#pop-options + let check_key_shares (algs: Bertie.Tls13crypto.t_Algorithms) (ch: t_Slice u8) = match Bertie.Tls13utils.check_length_encoding_u16_slice ch <: Core.Result.t_Result Prims.unit u8 diff --git a/proofs/fstar/extraction/Bertie.Tls13formats.fsti b/proofs/fstar/extraction/Bertie.Tls13formats.fsti index 431692a..c863fd2 100644 --- a/proofs/fstar/extraction/Bertie.Tls13formats.fsti +++ b/proofs/fstar/extraction/Bertie.Tls13formats.fsti @@ -427,6 +427,14 @@ val set_client_hello_binder | _ -> true)) (fun _ -> Prims.l_True) +/// Check the server name for the sni extension. +/// Returns the value for the server name indicator when successful, and a `[TLSError`] +/// otherwise. +val check_server_name (extension: t_Slice u8) + : Prims.Pure (Core.Result.t_Result Bertie.Tls13utils.t_Bytes u8) + Prims.l_True + (fun _ -> Prims.l_True) + val parse_server_certificate (certificate: Bertie.Tls13formats.Handshake_data.t_HandshakeData) : Prims.Pure (Core.Result.t_Result Bertie.Tls13utils.t_Bytes u8) Prims.l_True @@ -444,14 +452,6 @@ val build_server_name (name: Bertie.Tls13utils.t_Bytes) val check_psk_key_exchange_modes (client_hello: t_Slice u8) : Prims.Pure (Core.Result.t_Result Prims.unit u8) Prims.l_True (fun _ -> Prims.l_True) -/// Check the server name for the sni extension. -/// Returns the value for the server name indicator when successful, and a `[TLSError`] -/// otherwise. -val check_server_name (extension: t_Slice u8) - : Prims.Pure (Core.Result.t_Result Bertie.Tls13utils.t_Bytes u8) - Prims.l_True - (fun _ -> Prims.l_True) - val check_server_psk_shared_key (v__algs: Bertie.Tls13crypto.t_Algorithms) (b: t_Slice u8) : Prims.Pure (Core.Result.t_Result Prims.unit u8) Prims.l_True (fun _ -> Prims.l_True) @@ -482,10 +482,23 @@ val check_server_key_share (algs: Bertie.Tls13crypto.t_Algorithms) (b: t_Slice u Prims.l_True (fun _ -> Prims.l_True) +/// For termination, needs: (decreases Seq.length b) val check_server_extension (algs: Bertie.Tls13crypto.t_Algorithms) (b: t_Slice u8) : Prims.Pure (Core.Result.t_Result (usize & Core.Option.t_Option Bertie.Tls13utils.t_Bytes) u8) Prims.l_True - (fun _ -> Prims.l_True) + (ensures + fun result -> + let result:Core.Result.t_Result (usize & Core.Option.t_Option Bertie.Tls13utils.t_Bytes) + u8 = + result + in + match + result + <: + Core.Result.t_Result (usize & Core.Option.t_Option Bertie.Tls13utils.t_Bytes) u8 + with + | Core.Result.Result_Ok (len, out) -> len >=. sz 4 + | _ -> true) val check_signature_algorithms (algs: Bertie.Tls13crypto.t_Algorithms) (ch: t_Slice u8) : Prims.Pure (Core.Result.t_Result Prims.unit u8) Prims.l_True (fun _ -> Prims.l_True) @@ -563,7 +576,7 @@ val handshake_record (p: Bertie.Tls13formats.Handshake_data.t_HandshakeData) (Bertie.Tls13utils.impl__Bytes__len p.Bertie.Tls13formats.Handshake_data._0 <: usize) <. sz 65536 && (Bertie.Tls13utils.impl__Bytes__len d <: usize) =. - (sz 3 +! + (sz 5 +! (Bertie.Tls13utils.impl__Bytes__len p.Bertie.Tls13formats.Handshake_data._0 <: usize) <: usize) @@ -766,6 +779,7 @@ val check_server_extensions (algs: Bertie.Tls13crypto.t_Algorithms) (b: t_Slice Prims.l_True (fun _ -> Prims.l_True) +/// Needs decreases clause val find_key_share (g: Bertie.Tls13utils.t_Bytes) (ch: t_Slice u8) : Prims.Pure (Core.Result.t_Result Bertie.Tls13utils.t_Bytes u8) Prims.l_True diff --git a/proofs/fstar/extraction/Bertie.Tls13utils.fsti b/proofs/fstar/extraction/Bertie.Tls13utils.fsti index f259d57..04b3025 100644 --- a/proofs/fstar/extraction/Bertie.Tls13utils.fsti +++ b/proofs/fstar/extraction/Bertie.Tls13utils.fsti @@ -157,13 +157,6 @@ val check (b: bool) val check_eq1 (b1 b2: u8) : Prims.Pure (Core.Result.t_Result Prims.unit u8) Prims.l_True (fun _ -> Prims.l_True) -/// Attempt to TLS encode the `bytes` with [`u8`] length. -/// On success, return a new [Bytes] slice such that its first byte encodes the -/// length of `bytes` and the remainder equals `bytes`. Return a [TLSError] if -/// the length of `bytes` exceeds what can be encoded in one byte. -val encode_length_u8 (bytes: t_Slice u8) - : Prims.Pure (Core.Result.t_Result t_Bytes u8) Prims.l_True (fun _ -> Prims.l_True) - /// Check if `bytes[2..]` is at least as long as the length encoded by `bytes[0..2]` /// in big-endian order. /// On success, return the encoded length. Return a [TLSError] if `bytes` is less than 2 @@ -351,14 +344,52 @@ val bytes (x: t_Slice u8) /// big-endian length of `bytes` and the remainder equals `bytes`. Return a [TLSError] if /// the length of `bytes` exceeds what can be encoded in two bytes. val encode_length_u16 (bytes: t_Bytes) - : Prims.Pure (Core.Result.t_Result t_Bytes u8) Prims.l_True (fun _ -> Prims.l_True) + : Prims.Pure (Core.Result.t_Result t_Bytes u8) + Prims.l_True + (ensures + fun result -> + let result:Core.Result.t_Result t_Bytes u8 = result in + match result <: Core.Result.t_Result t_Bytes u8 with + | Core.Result.Result_Ok lenb -> + (impl__Bytes__len bytes <: usize) <. sz 65536 && + (impl__Bytes__len lenb <: usize) >=. sz 2 && + ((impl__Bytes__len lenb <: usize) -! sz 2 <: usize) =. (impl__Bytes__len bytes <: usize) + | _ -> true) /// Attempt to TLS encode the `bytes` with [`u24`] length. /// On success, return a new [Bytes] slice such that its first three bytes encode the /// big-endian length of `bytes` and the remainder equals `bytes`. Return a [TLSError] if /// the length of `bytes` exceeds what can be encoded in three bytes. val encode_length_u24 (bytes: t_Bytes) - : Prims.Pure (Core.Result.t_Result t_Bytes u8) Prims.l_True (fun _ -> Prims.l_True) + : Prims.Pure (Core.Result.t_Result t_Bytes u8) + Prims.l_True + (ensures + fun result -> + let result:Core.Result.t_Result t_Bytes u8 = result in + match result <: Core.Result.t_Result t_Bytes u8 with + | Core.Result.Result_Ok lenb -> + (impl__Bytes__len bytes <: usize) <. sz 16777216 && + (impl__Bytes__len lenb <: usize) >=. sz 3 && + ((impl__Bytes__len lenb <: usize) -! sz 3 <: usize) =. (impl__Bytes__len bytes <: usize) + | _ -> true) + +/// Attempt to TLS encode the `bytes` with [`u8`] length. +/// On success, return a new [Bytes] slice such that its first byte encodes the +/// length of `bytes` and the remainder equals `bytes`. Return a [TLSError] if +/// the length of `bytes` exceeds what can be encoded in one byte. +val encode_length_u8 (bytes: t_Slice u8) + : Prims.Pure (Core.Result.t_Result t_Bytes u8) + Prims.l_True + (ensures + fun result -> + let result:Core.Result.t_Result t_Bytes u8 = result in + match result <: Core.Result.t_Result t_Bytes u8 with + | Core.Result.Result_Ok lenb -> + (Core.Slice.impl__len #u8 bytes <: usize) <. sz 256 && + (impl__Bytes__len lenb <: usize) >=. sz 1 && + ((impl__Bytes__len lenb <: usize) -! sz 1 <: usize) =. + (Core.Slice.impl__len #u8 bytes <: usize) + | _ -> true) val tlserr (#v_T: Type0) (err: u8) : Prims.Pure (Core.Result.t_Result v_T u8) @@ -416,30 +447,75 @@ val impl__Bytes__update_slice (self: t_Bytes) (start: usize) (other: t_Bytes) (b : Prims.Pure t_Bytes Prims.l_True (fun _ -> Prims.l_True) val check_length_encoding_u16_slice (bytes: t_Slice u8) - : Prims.Pure (Core.Result.t_Result Prims.unit u8) Prims.l_True (fun _ -> Prims.l_True) + : Prims.Pure (Core.Result.t_Result Prims.unit u8) + Prims.l_True + (ensures + fun result -> + let result:Core.Result.t_Result Prims.unit u8 = result in + match result <: Core.Result.t_Result Prims.unit u8 with + | Core.Result.Result_Ok _ -> + (Core.Slice.impl__len #u8 bytes <: usize) >=. sz 2 && + (Core.Slice.impl__len #u8 bytes <: usize) <=. sz 65537 + | _ -> true) /// Check if `bytes` contains exactly as many bytes of content as encoded by its /// first two bytes. /// Returns `Ok(())` if there are no bytes left, and a [`TLSError`] if there are /// more bytes in the `bytes`. val check_length_encoding_u16 (bytes: t_Bytes) - : Prims.Pure (Core.Result.t_Result Prims.unit u8) Prims.l_True (fun _ -> Prims.l_True) + : Prims.Pure (Core.Result.t_Result Prims.unit u8) + Prims.l_True + (ensures + fun result -> + let result:Core.Result.t_Result Prims.unit u8 = result in + match result <: Core.Result.t_Result Prims.unit u8 with + | Core.Result.Result_Ok _ -> + (impl__Bytes__len bytes <: usize) >=. sz 2 && + (impl__Bytes__len bytes <: usize) <=. sz 65537 + | _ -> true) /// Check if `bytes` contains exactly as many bytes of content as encoded by its /// first three bytes. /// Returns `Ok(())` if there are no bytes left, and a [`TLSError`] if there are /// more bytes in the `bytes`. val check_length_encoding_u24 (bytes: t_Slice u8) - : Prims.Pure (Core.Result.t_Result Prims.unit u8) Prims.l_True (fun _ -> Prims.l_True) + : Prims.Pure (Core.Result.t_Result Prims.unit u8) + Prims.l_True + (ensures + fun result -> + let result:Core.Result.t_Result Prims.unit u8 = result in + match result <: Core.Result.t_Result Prims.unit u8 with + | Core.Result.Result_Ok _ -> + (Core.Slice.impl__len #u8 bytes <: usize) >=. sz 3 && + (Core.Slice.impl__len #u8 bytes <: usize) <=. sz 16777218 + | _ -> true) val check_length_encoding_u8_slice (bytes: t_Slice u8) - : Prims.Pure (Core.Result.t_Result Prims.unit u8) Prims.l_True (fun _ -> Prims.l_True) + : Prims.Pure (Core.Result.t_Result Prims.unit u8) + Prims.l_True + (ensures + fun result -> + let result:Core.Result.t_Result Prims.unit u8 = result in + match result <: Core.Result.t_Result Prims.unit u8 with + | Core.Result.Result_Ok _ -> + (Core.Slice.impl__len #u8 bytes <: usize) >=. sz 1 && + (Core.Slice.impl__len #u8 bytes <: usize) <=. sz 256 + | _ -> true) /// Check if `bytes` contains exactly the TLS `u8` length encoded content. /// Returns `Ok(())` if there are no bytes left, and a [`TLSError`] if there are /// more bytes in the `bytes`. val check_length_encoding_u8 (bytes: t_Bytes) - : Prims.Pure (Core.Result.t_Result Prims.unit u8) Prims.l_True (fun _ -> Prims.l_True) + : Prims.Pure (Core.Result.t_Result Prims.unit u8) + Prims.l_True + (ensures + fun result -> + let result:Core.Result.t_Result Prims.unit u8 = result in + match result <: Core.Result.t_Result Prims.unit u8 with + | Core.Result.Result_Ok _ -> + (impl__Bytes__len bytes <: usize) >=. sz 1 && + (impl__Bytes__len bytes <: usize) <=. sz 256 + | _ -> true) /// Check if [U8] slices `b1` and `b2` are of the same /// length and agree on all positions. diff --git a/src/tls13formats.rs b/src/tls13formats.rs index eaa751e..5035fb5 100644 --- a/src/tls13formats.rs +++ b/src/tls13formats.rs @@ -8,7 +8,7 @@ use crate::{ zero_key, Algorithms, Digest, HashAlgorithm, Hmac, KemPk, Random, SignatureScheme, }, tls13utils::{ - bytes1, bytes2, bytes_concat, check, check_eq, check_eq_slice, check_eq_with_slice, + bytes1, bytes2, bytes_concat, check, check_eq, check_eq1, check_eq_slice, check_eq_with_slice, check_length_encoding_u16, check_length_encoding_u16_slice, check_length_encoding_u24, check_length_encoding_u8, check_length_encoding_u8_slice, check_mem, encode_length_u16, encode_length_u24, encode_length_u8, eq_slice, length_u16_encoded, @@ -74,9 +74,13 @@ fn build_server_name(name: &Bytes) -> Result { /// otherwise. fn check_server_name(extension: &[U8]) -> Result { check_length_encoding_u16_slice(extension)?; - check_eq_with_slice(&[U8(0)], extension, 2, 3)?; - check_length_encoding_u16_slice(&extension[3..extension.len()])?; - Ok(extension[5..extension.len()].into()) + if extension.len() > 3 { + check_eq1(U8(0), extension[2])?; + check_length_encoding_u16_slice(&extension[3..extension.len()])?; + Ok(extension[5..extension.len()].into()) + } else { + tlserr(parse_failed()) + } } /// Build the supported versions bytes for the client hello. @@ -139,6 +143,8 @@ fn key_shares(algs: &Algorithms, gx: KemPk) -> Result { Ok(encode_length_u16(encode_length_u16(ks)?)?.prefix(PREFIX)) } +/// Needs decreases clause +#[hax_lib::fstar::verification_status(lax)] fn find_key_share(g: &Bytes, ch: &[U8]) -> Result { if ch.len() < 4 { tlserr(parse_failed()) @@ -162,10 +168,14 @@ fn server_key_shares(algs: &Algorithms, gx: KemPk) -> Result { } fn check_server_key_share(algs: &Algorithms, b: &[U8]) -> Result { - check_eq_with_slice(algs.supported_group()?.as_raw(), b, 0, 2)?; - check_length_encoding_u16_slice(&b[2..b.len()])?; - // XXX Performance: These conversions aren't necessary. A slice would suffice. - Ok(Bytes::from(&b[4..b.len()])) + if b.len() >= 2 { + check_eq_with_slice(algs.supported_group()?.as_raw(), b, 0, 2)?; + check_length_encoding_u16_slice(&b[2..b.len()])?; + // XXX Performance: These conversions aren't necessary. A slice would suffice. + Ok(Bytes::from(&b[4..b.len()])) + } else { + tlserr(parse_failed()) + } } fn pre_shared_key(algs: &Algorithms, session_ticket: &Bytes) -> Result<(Bytes, usize), TLSError> { @@ -295,6 +305,11 @@ fn check_extension(algs: &Algorithms, bytes: &[U8]) -> Result<(usize, Extensions } } +/// For termination, needs: (decreases Seq.length b) +#[hax_lib::fstar::verification_status(lax)] +#[hax_lib::ensures(|result| match result { + Result::Ok((len,out)) => len >= 4, + _ => true})] fn check_server_extension(algs: &Algorithms, b: &[U8]) -> Result<(usize, Option), TLSError> { if b.len() < 4 { Err(parse_failed()) @@ -512,6 +527,7 @@ fn get_psk_extensions( /// Build a ClientHello message. #[hax_lib::pv_constructor] +#[hax_lib::fstar::verification_status(lax)] pub(crate) fn client_hello( algorithms: &Algorithms, client_random: Random, @@ -708,6 +724,7 @@ pub(super) fn parse_client_hello( /// Build the server hello message. #[hax_lib::pv_constructor] +#[hax_lib::fstar::verification_status(lax)] pub(crate) fn server_hello( algs: &Algorithms, sr: Random, @@ -798,6 +815,7 @@ pub(crate) fn encrypted_extensions(_algs: &Algorithms) -> Result Result (p.0.len() < 65536 && d.len() == 3 + p.0.len()), + Result::Ok(d) => (p.0.len() < 65536 && d.len() == 5 + p.0.len()), _ => true})] pub(crate) fn handshake_record(p: HandshakeData) -> Result { let ty = bytes1(ContentType::Handshake as u8); diff --git a/src/tls13formats/handshake_data.rs b/src/tls13formats/handshake_data.rs index e0b2ace..226aec1 100644 --- a/src/tls13formats/handshake_data.rs +++ b/src/tls13formats/handshake_data.rs @@ -172,7 +172,9 @@ impl HandshakeData { /// /// Returns `true`` if `payload` contains a message of the given type, `false` otherwise. /// - /// For termination proof in F*: (decreases (Seq.length self._0._0 - v start)) + /// For termination proof in F*: we need to hand-edit and add: + /// (decreases (Seq.length self._0._0 - v start)) + /// https://github.com/cryspen/hax/issues/1233 #[hax_lib::requires(fstar!(r#"Seq.length self._0._0 >= v start"#))] pub(crate) fn find_handshake_message( &self, diff --git a/src/tls13utils.rs b/src/tls13utils.rs index 164262a..ba45862 100644 --- a/src/tls13utils.rs +++ b/src/tls13utils.rs @@ -622,6 +622,9 @@ pub(crate) fn check_mem(b1: &[U8], b2: &[U8]) -> Result<(), TLSError> { /// length of `bytes` and the remainder equals `bytes`. Return a [TLSError] if /// the length of `bytes` exceeds what can be encoded in one byte. #[hax_lib::pv_constructor] +#[hax_lib::ensures(|result| match result { + Result::Ok(lenb) => bytes.len() < 256 && lenb.len() >= 1 && lenb.len() - 1 == bytes.len(), + _ => true})] pub(crate) fn encode_length_u8(bytes: &[U8]) -> Result { let len = bytes.len(); if len >= 256 { @@ -639,6 +642,9 @@ pub(crate) fn encode_length_u8(bytes: &[U8]) -> Result { /// On success, return a new [Bytes] slice such that its first two bytes encode the /// big-endian length of `bytes` and the remainder equals `bytes`. Return a [TLSError] if /// the length of `bytes` exceeds what can be encoded in two bytes. +#[hax_lib::ensures(|result| match result { + Result::Ok(lenb) => bytes.len() < 65536 && lenb.len() >= 2 && lenb.len() - 2 == bytes.len(), + _ => true})] pub(crate) fn encode_length_u16(mut bytes: Bytes) -> Result { let len = bytes.len(); if len >= 65536 { @@ -658,6 +664,9 @@ pub(crate) fn encode_length_u16(mut bytes: Bytes) -> Result { /// On success, return a new [Bytes] slice such that its first three bytes encode the /// big-endian length of `bytes` and the remainder equals `bytes`. Return a [TLSError] if /// the length of `bytes` exceeds what can be encoded in three bytes. +#[hax_lib::ensures(|result| match result { + Result::Ok(lenb) => bytes.len() < 16777216 && lenb.len() >= 3 && lenb.len() - 3 == bytes.len(), + _ => true})] pub(crate) fn encode_length_u24(bytes: &Bytes) -> Result { let len = bytes.len(); if len >= 16777216 { @@ -764,6 +773,9 @@ pub(crate) fn length_u24_encoded(bytes: &[U8]) -> Result { } } +#[hax_lib::ensures(|result| match result { + Result::Ok(_) => bytes.len() >= 1 && bytes.len() <= 256, + _ => true})] pub(crate) fn check_length_encoding_u8_slice(bytes: &[U8]) -> Result<(), TLSError> { if length_u8_encoded(bytes)? + 1 != bytes.len() { Err(parse_failed()) @@ -776,11 +788,17 @@ pub(crate) fn check_length_encoding_u8_slice(bytes: &[U8]) -> Result<(), TLSErro /// /// Returns `Ok(())` if there are no bytes left, and a [`TLSError`] if there are /// more bytes in the `bytes`. +#[hax_lib::ensures(|result| match result { + Result::Ok(_) => bytes.len() >= 1 && bytes.len() <= 256, + _ => true})] pub(crate) fn check_length_encoding_u8(bytes: &Bytes) -> Result<(), TLSError> { check_length_encoding_u8_slice(bytes.as_raw()) } #[inline(always)] +#[hax_lib::ensures(|result| match result { + Result::Ok(_) => bytes.len() >= 2 && bytes.len() <= 65537, + _ => true})] pub(crate) fn check_length_encoding_u16_slice(bytes: &[U8]) -> Result<(), TLSError> { if length_u16_encoded(bytes)? + 2 != bytes.len() { Err(parse_failed()) @@ -794,6 +812,9 @@ pub(crate) fn check_length_encoding_u16_slice(bytes: &[U8]) -> Result<(), TLSErr /// /// Returns `Ok(())` if there are no bytes left, and a [`TLSError`] if there are /// more bytes in the `bytes`. +#[hax_lib::ensures(|result| match result { + Result::Ok(_) => bytes.len() >= 2 && bytes.len() <= 65537, + _ => true})] pub(crate) fn check_length_encoding_u16(bytes: &Bytes) -> Result<(), TLSError> { check_length_encoding_u16_slice(bytes.as_raw()) } @@ -803,6 +824,9 @@ pub(crate) fn check_length_encoding_u16(bytes: &Bytes) -> Result<(), TLSError> { /// /// Returns `Ok(())` if there are no bytes left, and a [`TLSError`] if there are /// more bytes in the `bytes`. +#[hax_lib::ensures(|result| match result { + Result::Ok(_) => bytes.len() >= 3 && bytes.len() <= 16777218, + _ => true})] pub(crate) fn check_length_encoding_u24(bytes: &[U8]) -> Result<(), TLSError> { if length_u24_encoded(bytes)? + 3 != bytes.len() { Err(parse_failed())