miTLS :: TLSExtensions

F# Interface: TLSExtensions.fsi

(*
 * Copyright (c) 2012--2013 MSR-INRIA Joint Center. All rights reserved.
 * 
 * This code is distributed under the terms for the CeCILL-B (version 1)
 * license.
 * 
 * You should have received a copy of the CeCILL-B (version 1) license
 * along with this program.  If not, see:
 * 
 *   http://www.cecill.info/licences/Licence_CeCILL-B_V1-en.txt
 *)

module TLSExtensions

open Bytes
open Error
open TLSConstants

type extensionType

val extensionsBytes: bool -> bytes -> bytes
val parseExtensions: bytes -> (extensionType * bytes) list Result
val inspect_ServerHello_extensions: (extensionType * bytes) list -> bytes -> unit Result
val checkClientRenegotiationInfoExtension: (extensionType * bytes) list -> TLSConstants.cipherSuites -> bytes -> bool

val sigHashAlgBytes: Sig.alg -> bytes
val parseSigHashAlg: bytes -> Sig.alg Result
val sigHashAlgListBytes: Sig.alg list -> bytes
val parseSigHashAlgList: bytes -> Sig.alg list Result
val default_sigHashAlg: ProtocolVersion -> cipherSuite -> Sig.alg list
val sigHashAlg_contains: Sig.alg list -> Sig.alg -> bool
val cert_type_list_to_SigHashAlg: certType list -> ProtocolVersion -> Sig.alg list
val cert_type_list_to_SigAlg: certType list -> sigAlg list
val sigHashAlg_bySigList: Sig.alg list -> sigAlg list -> Sig.alg list

F# Implementation: TLSExtensions.fs

module TLSExtensions

open Bytes
open Error
open TLSConstants

type extensionType =
    | HExt_renegotiation_info

let extensionTypeBytes hExt =
    match hExt with
    | HExt_renegotiation_info -> [|0xFFuy; 0x01uy|]

let parseExtensionType b =
    match b with
    | [|0xFFuy; 0x01uy|] -> correct(HExt_renegotiation_info)
    | _                  -> let reason = perror __SOURCE_FILE__ __LINE__ "" in Error(AD_decode_error, reason)

let isExtensionType et (ext:extensionType * bytes) =
    let et' = fst(ext) in
    et = et'

let extensionBytes extType data =
    let extTBytes = extensionTypeBytes extType in
    let payload = vlbytes 2 data in
    extTBytes @| payload

let consExt (e:extensionType * bytes) l = e :: l

let rec parseExtensionList data list =
    match length data with
    | 0 -> correct (list)
    | x when x < 4 ->
        (* This is a parsing error, or a malformed extension *)
        Error (AD_decode_error, perror __SOURCE_FILE__ __LINE__ "")
    | _ ->
        let (extTypeBytes,rem) = Bytes.split data 2 in
        match vlsplit 2 rem with
            | Error(x,y) -> Error (x,y) (* Parsing error *)
            | Correct (res) ->
                let (payload,rem) = res in
                match parseExtensionType extTypeBytes with
                | Error(x,y) ->
                    (* Unknown extension, skip it *)
                    parseExtensionList rem list
                | Correct(extType) ->
                    let thisExt = (extType,payload) in
                    let list = consExt thisExt list in
                    parseExtensionList rem list

(* Renegotiation Info extension -- RFC 5746 *)
let renegotiationInfoExtensionBytes verifyData =
    let payload = vlbytes 1 verifyData in
    extensionBytes HExt_renegotiation_info payload

let parseRenegotiationInfoExtension payload =
    if length payload > 0 then
        vlparse 1 payload
    else
        let reason = perror __SOURCE_FILE__ __LINE__ "" in
        Error(AD_decode_error,reason)

(* Top-level extension handling *)
let extensionsBytes safeRenegoEnabled verifyData =
    if safeRenegoEnabled then
        let renInfo = renegotiationInfoExtensionBytes verifyData in
        vlbytes 2 renInfo
    else
        (* We are sending no extensions at all *)
        [||]

let parseExtensions data =
    match length data with
    | 0 -> let el = [] in correct (el)
    | 1 -> Error(AD_decode_error, perror __SOURCE_FILE__ __LINE__ "")
    | _ ->
        match vlparse 2 data with
        | Error(x,y)    -> Error(x,y)
        | Correct(exts) ->
            match parseExtensionList exts [] with
            | Error(x,y) -> Error(x,y)
            | Correct(extList) ->
                (* Check there is at most one renegotiation_info extension *)

let ren_ext_list = Bytes.filter (isExtensionType HExt_renegotiation_info) extList in
                if listLength ren_ext_list > 1 then
                    Error(AD_handshake_failure, perror __SOURCE_FILE__ __LINE__ "Same extension received more than once")
                else
                    correct(ren_ext_list)

let check_reneg_info payload expected =
    // We also check there were no more data in this extension.
    match parseRenegotiationInfoExtension payload with
    | Error(x,y)     -> false
    | Correct (recv) -> equalBytes recv expected

let checkClientRenegotiationInfoExtension (ren_ext_list:(extensionType * bytes) list) ch_cipher_suites expected =
    let has_SCSV = contains_TLS_EMPTY_RENEGOTIATION_INFO_SCSV ch_cipher_suites in
    if equalBytes expected [||]
    then
        (* First handshake *)
        if listLength ren_ext_list = 0
        then has_SCSV
            (* either client gave SCSV and no extension; this is OK for first handshake *)
            (* or the client doesn't support this extension and we fail *)
        else
            let ren_ext = listHead ren_ext_list in
            let (extType,payload) = ren_ext in
            check_reneg_info payload expected
    else
        (* Not first handshake *)
        if has_SCSV || (listLength ren_ext_list = 0) then false
        else
            let ren_ext = listHead ren_ext_list in
            let (extType,payload) = ren_ext in
            check_reneg_info payload expected

let inspect_ServerHello_extensions (extList:(extensionType * bytes) list) expected =

(* We expect to find exactly one extension *)
    match listLength extList with
    | 0 -> Error(AD_handshake_failure, perror __SOURCE_FILE__ __LINE__ "Not enough extensions given")
    | x when x <> 1 -> Error(AD_handshake_failure, perror __SOURCE_FILE__ __LINE__ "Too many extensions given")
    | _ ->
        let (extType,payload) = listHead extList in
        match extType with
        | HExt_renegotiation_info ->
            (* Check its content *)
            if check_reneg_info payload expected then
                let unitVal = () in
                correct (unitVal)
            else
                (* RFC 5746, sec 3.4: send a handshake failure alert *)
                Error(AD_handshake_failure, perror __SOURCE_FILE__ __LINE__ "Wrong renegotiation information")

(* SignatureAndHashAlgorithm parsing functions *)
let sigHashAlgBytes alg =
    // pre: we're in TLS 1.2
    let (sign,hash) = alg in
    let signB = sigAlgBytes sign in
    let hashB = hashAlgBytes hash in
    hashB @| signB

let parseSigHashAlg b =
    let (hashB,signB) = Bytes.split b 1 in
    match parseSigAlg signB with
    | Error(x,y) -> Error(x,y)
    | Correct(sign) ->
        match parseHashAlg hashB with
        | Error(x,y) -> Error(x,y)
        | Correct(hash) -> correct(sign,hash)

let rec sigHashAlgListBytes algL =
    match algL with
    | [] -> [||]
    | h::t ->
        let oneItem = sigHashAlgBytes h in
        oneItem @| sigHashAlgListBytes t

let rec parseSigHashAlgList_int b : (Sig.alg list Result)=
    if length b = 0 then correct([])
    elif length b = 1 then Error(AD_decode_error, perror __SOURCE_FILE__ __LINE__ "")
    else
        let (thisB,remB) = Bytes.split b 2 in
        match parseSigHashAlg thisB with
        | Error(x,y) -> Error(x,y)
        | Correct(this) ->
            match parseSigHashAlgList_int remB with
            | Error(x,y) -> Error(x,y)
            | Correct(rem) -> correct(this :: rem)

let parseSigHashAlgList b =
    match vlparse 2 b with
    | Error(x,y) -> Error(x,y)
    | Correct(b) -> parseSigHashAlgList_int b

let default_sigHashAlg pv cs =
    default_sigHashAlg_fromSig pv (sigAlg_of_ciphersuite cs)

let sigHashAlg_contains (algList:Sig.alg list) (alg:Sig.alg) =
    Bytes.exists (fun a -> a = alg) algList

let sigHashAlg_bySigList (algList:Sig.alg list) (sigAlgList:sigAlg list):Sig.alg list =
    Bytes.choose (fun alg -> let (sigA,_) = alg in if (Bytes.exists (fun a -> a = sigA) sigAlgList) then Some(alg) else None) algList

let cert_type_to_SigHashAlg ct pv =
    match ct with
    | TLSConstants.DSA_fixed_dh | TLSConstants.DSA_sign -> default_sigHashAlg_fromSig pv SA_DSA
    | TLSConstants.RSA_fixed_dh | TLSConstants.RSA_sign -> default_sigHashAlg_fromSig pv SA_RSA

let rec cert_type_list_to_SigHashAlg ctl pv =

match ctl with
    | [] -> []
    | h::t -> (cert_type_to_SigHashAlg h pv) @ (cert_type_list_to_SigHashAlg t pv)

let cert_type_to_SigAlg ct =
    match ct with
    | TLSConstants.DSA_fixed_dh | TLSConstants.DSA_sign -> SA_DSA
    | TLSConstants.RSA_fixed_dh | TLSConstants.RSA_sign -> SA_RSA

let rec cert_type_list_to_SigAlg ctl =

match ctl with
    | [] -> []
    | h::t -> (cert_type_to_SigAlg h) :: (cert_type_list_to_SigAlg t)

F7 Interface: TLSExtensions.fs7

module TLSExtensions

open Bytes
open Error
open TLSConstants

private type extensionType =
    | HExt_renegotiation_info

function val ExtensionTypeBytes: extensionType -> bytes
private definition ExtensionTypeBytes(HExt_renegotiation_info) = [|0xFFuy; 0x01uy|]

val extensionTypeBytes: et:extensionType -> b:bytes{b=ExtensionTypeBytes(et)}
val parseExtensionType: b:bytes -> (et:extensionType{b=ExtensionTypeBytes(et)}) Result
val isExtensionType: et:extensionType -> ext:(extensionType * bytes) ->
	b:bool{b = true => (?et',d. ext=(et',d) /\ et = et')}

function val ExtensionBytes: extensionType * bytes -> bytes
private definition !et,b.
	ExtensionBytes(et,b) = ExtensionTypeBytes(et) @| VLBytes(2,b)
predicate ContainsExtensions of bytes * (extensionType * bytes) list

private definition !b,l. ContainsExtensions(b,l)

val extensionBytes: et:extensionType -> d:bytes -> b:bytes{b=ExtensionBytes(et,d)}
val consExt: extensionType * bytes -> (extensionType * bytes) list -> (extensionType * bytes) list
val parseExtensionList: b:bytes -> cur:(extensionType * bytes) list ->
	(res:(extensionType * bytes) list{ContainsExtensions(b,res)}) Result

val renegotiationInfoExtensionBytes: vd:bytes ->
	b:bytes{b=ExtensionBytes(HExt_renegotiation_info,VLBytes(1,vd))}
val parseRenegotiationInfoExtension: b:bytes ->
	(vd:bytes{b=VLBytes(1,vd)}) Result

function val ExtensionsBytes: bytes -> bytes
private definition !b. ExtensionsBytes(b) = VLBytes(2,b)
val extensionsBytes: en:bool -> vd:bytes ->
	b:bytes{(en = true /\ b = ExtensionsBytes(ExtensionBytes(HExt_renegotiation_info,VLBytes(1,vd))) ) \/
			(en = false /\ b = [||])}

val parseExtensions: b:bytes -> (res:(extensionType * bytes) list
	{(b = [||] /\ res = [] ) \/
	 (b <> [||] /\ ?ext. b = VLBytes(2,ext) /\ ContainsExtensions(ext,res) )
	}) Result

val check_reneg_info: got:bytes -> exp:bytes ->
	b:bool{b=true => (?d. got = VLBytes(1,d) /\ exp = d)}

val checkClientRenegotiationInfoExtension:
	(extensionType * bytes) list -> cipherSuites -> bytes -> bool

val inspect_ServerHello_extensions:
	(extensionType * bytes) list -> bytes ->
		unit Result

(* SignatureAndHashAlgorithm parsing functions *)
function val SigHashAlgBytes: 'a  -> bytes
private definition !s,h. SigHashAlgBytes((s,h)) = HashAlgBytes(s) @| SigAlgBytes(h)

val sigHashAlgBytes: a:Sig.alg -> b:bytes{b=SigHashAlgBytes(a)}
val parseSigHashAlg: b:bytes -> (a:Sig.alg{b=SigHashAlgBytes(a)}) Result

function val SigHashAlgsBytes: Sig.alg list -> bytes
val sigHashAlgListBytes: al:Sig.alg list -> b:bytes{b=SigHashAlgsBytes(al)}
val parseSigHashAlgList: b:bytes -> (al:Sig.alg list{b=SigHashAlgsBytes(al)}) Result
function val DefaultSigHashAlgs: ProtocolVersion * cipherSuite -> Sig.alg list
val default_sigHashAlg: pv:ProtocolVersion -> cs:cipherSuite -> al:Sig.alg list{al=DefaultSigHashAlgs(pv,cs)}
val sigHashAlg_contains: Sig.alg list -> Sig.alg -> bool
val cert_type_list_to_SigHashAlg: certType list -> ProtocolVersion -> Sig.alg list
val cert_type_list_to_SigAlg: certType list -> sigAlg list
val sigHashAlg_bySigList: Sig.alg list -> sigAlg list -> Sig.alg list

Verification status

This module is trusted: its F# code is assumed to meet its F7 interface.

Verification depends on the F7 interfaces of the following modules: Error Bytes TLSConstants HASH Sig

miTLS

A verified reference TLS implementation

miTLS :: TLSExtensions

F# Interface: TLSExtensions.fsi

F# Implementation: TLSExtensions.fs

F7 Interface: TLSExtensions.fs7

Verification status

Module list

Trusted

Idealized

Verified