miTLS :: TLS

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

open Bytes
open Error
open Dispatch
open TLSInfo
open Tcp
open DataStream

type ioresult_o =
    | WriteError    of alertDescription option * string
    | WriteComplete of nextCn
    | WritePartial  of nextCn * msg_o
    | MustRead      of Connection

(* Event-driven interface *)

val read     : Connection -> ioresult_i
val write    : Connection -> msg_o -> ioresult_o
val full_shutdown : Connection -> Connection
val half_shutdown : Connection -> unit

val connect : NetworkStream -> config -> Connection
val resume  : NetworkStream -> sessionID -> config -> Connection

val rehandshake : Connection -> config -> bool * nextCn
val rekey       : Connection -> config -> bool * nextCn
val request     : Connection -> config -> bool * nextCn

val accept           : TcpListener   -> config -> Connection
val accept_connected : NetworkStream -> config -> Connection

val authorize: Connection -> query -> ioresult_i
val refuse:    Connection -> query -> unit

val getEpochIn:  Connection -> epoch
val getEpochOut: Connection -> epoch
val getSessionInfo: epoch -> SessionInfo
val getInStream:  Connection -> stream
val getOutStream: Connection -> stream

F# Implementation: TLS.fs

module TLS

open Bytes
open Error
open TLSInfo
open Tcp
open Dispatch

type ioresult_o =
    | WriteError    of alertDescription option * string
    | WriteComplete of nextCn
    | WritePartial  of nextCn * msg_o
    | MustRead      of Connection

let connect ns po = Dispatch.init ns Client po
let resume ns sid po = Dispatch.resume ns sid po

let rehandshake c po = Dispatch.rehandshake c po
let rekey c po = Dispatch.rekey c po

let accept list po =
    let ns = Tcp.accept list in
    Dispatch.init ns Server po
let accept_connected ns po = Dispatch.init ns Server po

let request c po = Dispatch.request c po

let read ca =
  let cb,outcome,m = Dispatch.read ca in
    match outcome,m with
      | WriteOutcome(WError(err)),_ -> ReadError(None,err)
      | RError(err),_ -> ReadError(None,err)
      | RAppDataDone,Some(b) -> Read(cb,b)
      | RQuery(q,adv),_ -> CertQuery(cb,q,adv)
      | RHSDone,_ -> Handshaken(cb)
      | RClose,_ -> Close (networkStream cb)
      | RFatal(ad),_ -> Fatal(ad)
      | RWarning(ad),_ -> Warning(cb,ad)
      | WriteOutcome(WMustRead),_ -> DontWrite(cb)
      | WriteOutcome(WHSDone),_ -> Handshaken (cb)
      | WriteOutcome(SentFatal(ad,s)),_ -> ReadError(Some(ad),s)
      | WriteOutcome(SentClose),_ -> Close (networkStream cb)
      | WriteOutcome(WriteAgain),_ -> unexpectedError "[read] Dispatch.read should never return WriteAgain"
      | _,_ -> ReadError(None, perror __SOURCE_FILE__ __LINE__ "Invalid dispatcher state. This is probably a bug, please report it")

let write c msg =
    let c,outcome,rdOpt = Dispatch.write c msg in
    match outcome with
      | WError(err) -> WriteError(None,err)
      | WAppDataDone ->
            match rdOpt with
              | None -> WriteComplete c
              | Some(rd) -> WritePartial (c,rd)
      | WHSDone ->
          (* A top-level write should never lead to HS completion.
             Currently, we report this as an internal error.
             Being more precise about the Dispatch state machine, we should be
             able to prove that this case should never happen, and so use the
             unexpectedError function. *)
          WriteError(None, perror __SOURCE_FILE__ __LINE__ "Invalid dispatcher state. This is probably a bug, please report it")
      | WMustRead ->
          MustRead(c)
      | SentClose ->
          (* A top-level write can never send a closure alert on its own.
             Either the user asks for half_shutdown, and the connection is consumed,
             or it asks for full_shutdown, and then it cannot write anymore *)
          WriteError(None, perror __SOURCE_FILE__ __LINE__ "Invalid dispatcher state. This is probably a bug, please report it")
      | SentFatal(ad,err) ->
          WriteError(Some(ad),err)
      | WriteAgain | WriteAgainFinishing ->
          unexpectedError "[write] writeAll should never ask to write again"

let full_shutdown c = Dispatch.full_shutdown c
let half_shutdown c = Dispatch.half_shutdown c

let authorize c q =
    let cb,outcome,m = Dispatch.authorize c q in
    match outcome with
      | WriteOutcome(WError(err)) -> ReadError(None,err)
      | RError(err) -> ReadError(None,err)
      | RHSDone -> Handshaken(cb)
      | RClose -> Close (networkStream cb)
      | RFatal(ad) -> Fatal(ad)
      | RWarning(ad) -> Warning(cb,ad)
      | WriteOutcome(WMustRead) -> DontWrite(cb)
      | WriteOutcome(WHSDone) -> Handshaken (cb)
      | WriteOutcome(SentFatal(ad,s)) -> ReadError(Some(ad),s)
      | WriteOutcome(SentClose) -> Close (networkStream cb)
      | WriteOutcome(WriteAgain) -> unexpectedError "[read] Dispatch.read should never return WriteAgain"
      | _ -> ReadError(None, perror __SOURCE_FILE__ __LINE__ "Invalid dispatcher state. This is probably a bug, please report it")

let refuse c q = Dispatch.refuse c q

let getEpochIn c = Dispatch.getEpochIn c
let getEpochOut c = Dispatch.getEpochOut c
let getSessionInfo ki = epochSI(ki)
let getInStream  c = Dispatch.getInStream c
let getOutStream c = Dispatch.getOutStream c

F7 Interface: TLS.fs7

module TLS

open Error
open Bytes
open TLSInfo
open DataStream (* application-specific module *)
open AppData
open Dispatch

type (;c:Connection) ioresult_i =
| ReadError of alertDescription option * string
  // We encountered an error while reading, so the connection dies.
  // we return the fatal alert we may have sent, if any,
  // or None in case of an internal error.

| Close of Tcp.NetworkStream {
	Auth(ConnectionEpochIn(c)) => EvClose(CnInfo(c).id_in, Bytes_i(c))
  }
  // We received an alert notifying the normal closure of the connection;
  // we learn that we have read everything sent by our peer,
  // and we get back the underlying TCP connection.

| Fatal of a:alertDescription {
	Auth(ConnectionEpochIn(c)) => EvFatal(CnInfo(c).id_in, a, Bytes_i(c))
  }
  // We received an alert notifying the abnornal closure of the connection by our peer
  // We learn that we have read everything sent by our peer.

| Warning of c':(;c) nextCn * a:alertDescription {
	Extend(c,c') /\ Auth(ConnectionEpochIn(c)) => EvWarning(CnInfo(c).id_in, a, Bytes_i(c))
  }
  // We received a warning (at this point in the input stream)

| CertQuery of c':(;c) nextCn * query * advice:bool {Extend(c, c')}
  // We received the peer certificates for the next epoch, to be authorized before proceeding.
  // "advice" is what the Windows certificate store said about this certificate.

| Handshaken of c':Connection {
       Role(c') = Role(c)
	/\ Rnd(c') = Rnd(c)
	/\ Config(c') = Config(c)
	/\ ConnectionEpochIn(c) = Pred(ConnectionEpochIn(c'))
	/\ Bytes_i(c') = [||]
	/\ EvClose(CnInfo(c).id_in, Bytes_i(c))
	/\ Handshake.Complete(CnInfo(c'),Config(c'))
	/\ (
		(Handshake.EvSentFinishedFirst(CnInfo(c'),true) /\
			  Bytes_o(c') = Bytes_o(c)
		   /\ ConnectionEpochOut(c') = ConnectionEpochOut(c)
		)
		\/
		(Handshake.EvSentFinishedFirst(CnInfo(c'),false) /\
			  Bytes_o(c') = [||]
		   /\ ConnectionEpochOut(c) = Pred(ConnectionEpochOut(c'))
		)
	   )
	}

| Read of c':(;c) nextCn * d:(;ConnectionEpochIn(c),CnStream_i(c)) msg_i {
	Extend_i(c,c',d) /\ (Auth(ConnectionEpochIn(c)) => EvWrite(CnInfo(c).id_in, Bytes_i(c')))
  }
  // We received a data fragment, appended to the input stream)

| DontWrite of c':Connection {
	   Role(c') = Role(c)
	/\ Rnd(c') = Rnd(c)
	/\ Config(c') = Config(c)
	/\ ConnectionEpochIn(c') = ConnectionEpochIn(c)
	/\ Bytes_i(c') = Bytes_i(c)
	/\ Bytes_o(c') = [||]
	/\ ConnectionEpochOut(c) = Pred(ConnectionEpochOut(c'))
    }

type (;c:Connection,d:(;ConnectionEpochOut(c),CnStream_o(c)) msg_o) ioresult_o =
| WriteError of alertDescription option * string
  // We encountered an error while writing;
  // we return the fatal alert we may have sent, if any,
  // or None in case of an internal error.

| WriteComplete of c':(;c) nextCn {Extend_o(c,c',d)}
  // We wrote the message in full. appended to the output stream

| WritePartial  of c':(;c) nextCn * d':(;ConnectionEpochOut(c'),CnStream_o(c')) msg_o {
	?d0. Extend_o(c,c',d0) /\ Split_o(c, d, d0, c', d')
  }
  // We wrote a fragment of the message, appended to the output stream, and return the rest

| MustRead of c':Connection {
		Role(c') = Role(c)
	 /\ Rnd(c') = Rnd(c)
     /\ Config(c') = Config(c)
	 /\ ConnectionEpochIn(c') = ConnectionEpochIn(c)
     /\ Bytes_i(c') = Bytes_i(c)
	 /\ Bytes_o(c') = [||]
	 /\ ConnectionEpochOut(c) = Pred(ConnectionEpochOut(c'))
	}

(* Event-driven interface *)

val read: c:Connection -> (;c) ioresult_i

val write: c:Connection{CanWrite(CnInfo(c))} -> d:(;ConnectionEpochOut(c),CnStream_o(c)) msg_o -> (;c,d) ioresult_o
// On the write side, the following events may be generated:
// - Write(ki,Bytes_o(c'))
// - Close(ki,Bytes_o(c))
// WriteError reports a local error
// WriteComplete reports write completion
// WritePartial reports partial write completion, and returns the rest
// MustRead signals that the connection cannot be used anymore for writing until a new handshake completes.
// (it may be a bit too restrictive)

val full_shutdown: c:Connection ->
	c':Connection{ Config(c') = Config(c) /\ Role(c') = Role(c) /\
		Rnd(c') = Rnd(c) /\
		ConnectionEpochIn(c') = ConnectionEpochIn(c) /\ Extend(c,c')
		// Note: we cannot write anymore
		}
val half_shutdown: c:Connection -> unit

val connect : Tcp.NetworkStream -> c:config -> (;Client,c) nullCn
val resume  : Tcp.NetworkStream -> sid:sessionID ->  c:config -> (;Client,c) nullCn
// even if the server declines, we authenticate the client's intent to resume from this sid.

val rekey: c:Connection {Role(c) = Client} -> conf:config ->
	(b:bool * c':Connection) {
		   Extend(c,c')
		/\ CnInfo(c') = CnInfo(c)
		/\ (   (b = false  /\ Config(c') = Config(c))
			\/ (b = true   /\ Config(c') = conf    ))
	}

val rehandshake: c:Connection {Role(c) = Client} -> conf:config ->
	(b:bool * c':Connection) {
		   Extend(c,c')
		/\ CnInfo(c') = CnInfo(c)
		/\ (   (b = false /\ Config(c') = Config(c))
			\/ (b = true  /\ Config(c') = conf    ))
	}

val request: c:Connection {Role(c) = Server} -> conf:config ->
	(b:bool * c':Connection) {
		   Extend(c,c')
		/\ CnInfo(c') = CnInfo(c)
		/\ (   (b = false /\ Config(c') = Config(c))
			\/ (b = true  /\ Config(c') = conf    ))
	}

val accept: Tcp.TcpListener -> c:config -> (;Server,c) nullCn
val accept_connected: Tcp.NetworkStream -> c:config -> (;Server,c) nullCn

// we echo the query so that we have an explicit user decision to blame.
val authorize : c:Connection -> q:query-> (;c)ioresult_i
val refuse    : c:Connection -> q:query -> unit

val getSessionInfo: k:succEpoch -> s:SessionInfo{s = EpochSI(k)}

val getEpochIn : c:Connection -> k:epoch{k = ConnectionEpochIn (c)}
val getEpochOut: c:Connection -> k:epoch{k = ConnectionEpochOut(c)}

val getInStream : c:Connection -> s:(;ConnectionEpochIn (c)) stream{s = CnStream_i(c)}
val getOutStream: c:Connection -> s:(;ConnectionEpochOut(c)) stream{s = CnStream_o(c)}

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 Nonce Tcp TLSConstants RSAKey DHGroup HASH HMAC TLSPRF Sig Cert TLSInfo Range DataStream AppFragment HSFragment TLSFragment StatefulPlain LHAEPlain MAC_SHA256 MAC_SHA1 MAC Encode ENC LHAE StatefulLHAE Record Alert PRF CRE DH RSA SessionDB TLSExtensions Handshake AppData Dispatch

miTLS

A verified reference TLS implementation

miTLS :: TLS

F# Interface: TLS.fsi

F# Implementation: TLS.fs

F7 Interface: TLS.fs7

Verification status

Module list

Trusted

Idealized

Verified