miTLS :: Alert

F# Interface: Alert.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 Alert

open Error
open TLSInfo
open Range

type pre_al_state
type state = pre_al_state

type ALFragReply =
    | EmptyALFrag
    | ALFrag of range * HSFragment.fragment
    | LastALFrag of range * HSFragment.fragment * alertDescription
    | LastALCloseFrag of range * HSFragment.fragment

type alert_reply =
    | ALAck of state
    | ALFatal of alertDescription * state
    | ALWarning of alertDescription * state
    | ALClose_notify of state

val alertBytes: alertDescription -> Bytes.bytes

val init: ConnectionInfo -> state

val send_alert: ConnectionInfo -> state -> alertDescription -> state

val next_fragment: ConnectionInfo -> state -> (ALFragReply * state)

val recv_fragment: ConnectionInfo -> state -> range -> HSFragment.fragment -> alert_reply Result

val is_incoming_empty: ConnectionInfo -> state -> bool
val reset_incoming: ConnectionInfo -> state -> ConnectionInfo -> state
val reset_outgoing: ConnectionInfo -> state -> ConnectionInfo -> state

F# Implementation: Alert.fs

module Alert

open Bytes
open Error
open TLSConstants
open TLSInfo
open Range

type pre_al_state = {
  al_incoming: bytes (* incomplete incoming message *)
  al_outgoing: bytes (* emptybstr if nothing to be sent *)
}

type state = pre_al_state

let init (ci:ConnectionInfo) = {al_incoming = [||]; al_outgoing = [||]}

type ALFragReply =
    | EmptyALFrag
    | ALFrag of range * HSFragment.plain
    | LastALFrag of range * HSFragment.plain * alertDescription
    | LastALCloseFrag of range * HSFragment.plain

type alert_reply =
    | ALAck of state
    | ALFatal of alertDescription * state
    | ALWarning of alertDescription * state
    | ALClose_notify of state

(* Conversions *)

let send_alert (ci:ConnectionInfo) state alertDesc =

(* Note: we only support sending one alert in the whole protocol execution
       (because we'll tell dispatch an alert has been sent when the buffer gets empty)
       So we only add an alert on an empty buffer (we don't enqueue more alerts) *)
    if equalBytes state.al_outgoing [||] then
        {state with al_outgoing = alertBytes alertDesc}
    else
        state (* Just ignore the request *)

// We implement locally fragmentation, not hiding any length
let makeFragment ki b =
    let (b0,rem) = if length b < fragmentLength then (b,[||])
                   else Bytes.split b fragmentLength
    let r0 = (length b0, length b0) in
    let f = HSFragment.fragmentPlain ki r0 b0 in
    ((r0,f),rem)

let next_fragment ci state =
    match state.al_outgoing with
    | [||] ->
        (EmptyALFrag, state)
    | d ->
        let ((r0,df),rem) = makeFragment ci.id_out d in
        let state = {state with al_outgoing = rem} in
        match rem with
        | [||] ->

match parseAlert d with
            | Error(x,y) -> unexpectedError ("[next_fragment] This invocation of parseAlertDescription should never fail")
            | Correct(ad) ->
                match ad with
                | AD_close_notify -> (LastALCloseFrag(r0,df),state)
                | _ -> (LastALFrag(r0,df,ad),state)
        | _ -> (ALFrag(r0,df),state)

let handle_alert ci state alDesc =
    match alDesc with
    | AD_close_notify ->
        (* we possibly send a close_notify back *)
        let state = send_alert ci state AD_close_notify in
        ALClose_notify (state)
    | _ ->
        if isFatal alDesc then
            ALFatal (alDesc,state)
        else
            ALWarning (alDesc,state)

let recv_fragment (ci:ConnectionInfo) state (r:range) (f:HSFragment.fragment) =

let fragment = HSFragment.fragmentRepr ci.id_in r f in
    match state.al_incoming with
    | [||] ->
        (* Empty buffer *)
        match length fragment with
        | 0 -> Error(AD_decode_error, perror __SOURCE_FILE__ __LINE__ "Empty alert fragments are invalid")
        | 1 -> Correct (ALAck ({state with al_incoming = fragment})) (* Buffer this partial alert *)
        | _ -> (* Full alert received *)
            let (al,rem) = Bytes.split fragment 2 in
            if length rem <> 0 then (* Check there are no more data *)
                Error(AD_decode_error, perror __SOURCE_FILE__ __LINE__ "No more data are expected after an alert")
            else
                match parseAlert al with
                | Error(x,y) -> Error(x,y)
                | Correct(alert) -> let res = handle_alert ci state alert in correct(res)
    | inc ->
        match length fragment with
        | 0 -> Error(AD_decode_error, perror __SOURCE_FILE__ __LINE__ "Empty alert fragments are invalid")
        | _ ->
            let (part2,rem) = Bytes.split fragment 1 in
            if length rem <> 0 then (* Check there are no more data *)
                Error(AD_decode_error, perror __SOURCE_FILE__ __LINE__ "No more data are expected after an alert")
            else
                let bmsg = inc @| part2 in
                match parseAlert bmsg with
                | Error(x,y) -> Error(x,y)
                | Correct(alert) ->
                    let state = {state with al_incoming = [||] } in
                    let res = handle_alert ci state alert in
                    correct(res)

let is_incoming_empty (c:ConnectionInfo) s = equalBytes s.al_incoming [||]

let reset_incoming (c:ConnectionInfo) s (nc:ConnectionInfo) =
    {s with al_incoming = [||]}

let reset_outgoing (c:ConnectionInfo) s (nc:ConnectionInfo) =
    {s with al_outgoing = [||]}

F7 Interface: Alert.fs7

module Alert

open Bytes
open Error
open TLSInfo
open Range

private type (;ci:ConnectionInfo)pre_al_state = {
  al_incoming: bytes; (* incomplete incoming message *)
  al_outgoing: bytes (* emptybstr if nothing to be sent *)
}
type (;ci:ConnectionInfo)state = (;ci)pre_al_state

type (;ki:epoch)ALFragReply =
    | EmptyALFrag
    | ALFrag of          (rg:range * (;ki,HSFragment.EmptyStream(ki),rg)HSFragment.plain)
    | LastALFrag of      (rg:range * (;ki,HSFragment.EmptyStream(ki),rg)HSFragment.plain * alertDescription)
    | LastALCloseFrag of (rg:range * (;ki,HSFragment.EmptyStream(ki),rg)HSFragment.plain)

type (;ci:ConnectionInfo)alert_reply =
    | ALAck of          (;ci)state
    | ALFatal of        alertDescription * (;ci)state
    | ALWarning of alertDescription * (;ci)state
    | ALClose_notify of (;ci)state

val alertBytes: ad:alertDescription -> b:bytes{b=AlertBytes(ad)}
val parseAlert: b:bytes -> (ad:alertDescription{b=AlertBytes(ad)}) Result

predicate IsFatal of alertDescription
private assume
	IsFatal(AD_unexpected_message   		) /\
	IsFatal(AD_bad_record_mac       		) /\
	IsFatal(AD_decryption_failed    		) /\
	IsFatal(AD_record_overflow      		) /\
	IsFatal(AD_decompression_failure		) /\
	IsFatal(AD_handshake_failure    		) /\
	IsFatal(AD_bad_certificate_fatal		) /\
	IsFatal(AD_unsupported_certificate_fatal) /\
	IsFatal(AD_certificate_revoked_fatal    ) /\
	IsFatal(AD_certificate_expired_fatal    ) /\
	IsFatal(AD_certificate_unknown_fatal    ) /\
	IsFatal(AD_illegal_parameter			) /\
	IsFatal(AD_unknown_ca       			) /\
	IsFatal(AD_access_denied    			) /\
	IsFatal(AD_decode_error     			) /\
	IsFatal(AD_export_restriction   		) /\
	IsFatal(AD_protocol_version     		) /\
	IsFatal(AD_insufficient_security		) /\
	IsFatal(AD_internal_error   			) /\
	IsFatal(AD_user_cancelled_fatal 		) /\
	IsFatal(AD_unsupported_extension		)

val isFatal: ad:alertDescription -> b:bool{b = true => IsFatal(ad)}

val init: ci:ConnectionInfo ->
	s:(;ci)state

val send_alert: ci:ConnectionInfo -> s:(;ci)state -> alertDescription ->
	s':(;ci)state

val makeFragment: e:epoch -> b:bytes -> (rg:range * (;e,HSFragment.EmptyStream(e),rg)HSFragment.plain) * bytes

val next_fragment: ci:ConnectionInfo -> s:(;ci)state ->
	(res:(;ci.id_out)ALFragReply * s':(;ci)state)

val handle_alert: ci:ConnectionInfo -> (;ci)state -> alertDescription -> (;ci)alert_reply

val recv_fragment: ci:ConnectionInfo -> s:(;ci)state ->
	rg:range -> f:(;ci.id_in,rg)HSFragment.fragment
    // {Auth(ci.id_in) => HSFragment.Sent(ci.id_in,AlInStream(ci,s),rg,f)}
	->
	(s':(;ci)alert_reply

) Result

val is_incoming_empty: ci:ConnectionInfo -> s:(;ci)state -> bool

val reset_incoming: ci:ConnectionInfo -> s:(;ci)state ->
	ci':ConnectionInfo{ci'.role = ci.role /\ ci'.id_out = ci.id_out} ->
	s':(;ci')state

val reset_outgoing: ci:ConnectionInfo -> s:(;ci)state ->
	ci':ConnectionInfo{ci'.role = ci.role /\ ci'.id_in = ci.id_in} ->
		s':(;ci')state

Verification status

The F# code of this module has been verified to meet its F7 interface.

Verification depends on the F7 interfaces of the following modules: Error Bytes TLSConstants RSAKey DHGroup HASH Sig Cert TLSInfo Range HSFragment

miTLS

A verified reference TLS implementation

miTLS :: Alert

F# Interface: Alert.fsi

F# Implementation: Alert.fs

F7 Interface: Alert.fs7

Verification status

Module list

Trusted

Idealized

Verified