miTLS

(*
 * 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 DataStream
open TLSConstants
open TLSInfo
open Bytes
open Error
open Range

let min (a:nat) (b:nat) =
    if a <= b then a else b
let max (a:nat) (b:nat) =
    if a >= b then a else b

let splitRange ki r =
    let (l,h) = r in
    let si = epochSI(ki) in
    let cs = si.cipher_suite in
    let FS = TLSInfo.fragmentLength in
    let PS = maxPadSize si in
    if PS = 0 then
        if l<>h then
            unexpectedError "[splitRange] Incompatible range provided"
        else
            let len = min h FS in
            let r0 = (len,len) in
            let r1 = (l-len,h-len) in
            (r0,r1)
    else
        let encAlg = encAlg_of_ciphersuite cs si.protocol_version in
        match encAlg with
        | Stream_RC4_128 -> unexpectedError "[splitRange] Stream ciphers do not support pad"
        | CBC_Stale(alg) | CBC_Fresh(alg) ->
            let BS = blockSize alg in
            let t  = macSize (TLSConstants.macAlg_of_ciphersuite cs si.protocol_version) in
            if FS < PS || PS < BS then
                unexpectedError "[splitRange] Incompatible fragment size, padding size and block size"
            else
                if l >= FS then
                    let r0 = (FS,FS) in
                    let r1 = (l-FS,h-FS) in
                    (r0,r1)
                else
                    let z0 = PS - ((PS + t + 1) % BS) in
                    let zl = PS - ((l + PS + t + 1) % BS) in
                    if l = 0 then
                        let p = h-l in
                        let fh = min p z0 in
                        let r0 = (0,fh) in
                        let r1 = (0,h-fh) in
                        (r0,r1)
                    else
                        let p = (h-l) % z0 in
                        if (p <= zl) && (l+p <= FS) then
                            let r0 = (l,l+p) in
                            let r1 = (0,h-(l+p)) in
                            (r0,r1)
                        else
                            let r0 = (l,l) in
                            let r1 = (0,h-l) in
                            (r0,r1)

type stream = {sb: bytes list}
type delta = {contents: rbytes}

let createDelta (ki:epoch) (s:stream) (r:range) (b:bytes) = {contents = b}
let deltaBytes  (ki:epoch) (s:stream) (r:range) (d:delta) = d.contents
let deltaPlain  (ki:epoch) (s:stream) (r:range) (b:rbytes) = {contents = b}
let deltaRepr   (ki:epoch) (s:stream) (r:range) (d:delta) = d.contents

// ghost
type es = EmptyStream of epoch

let init (ki:epoch) = {sb = []}

let append (ki:epoch) (s:stream) (r:range) (d:delta) =
#if ideal
    {sb = d.contents :: s.sb}
#else
    s
#endif

let split (ki:epoch) (s:stream)  (r0:range) (r1:range) (d:delta) =
  let (_,h0) = r0 in
  let (l1,_) = r1 in
  let len = length d.contents in
  let n = if h0 < (len - l1) then h0 else len - l1
  let (sb0,sb1) = Bytes.split d.contents n in
  ({contents = sb0},{contents = sb1})

#if ideal
let widen (ki:epoch) (s:stream) (r0:range) (r1:range) (d:delta) = let b = d.contents in {contents = b}
#endif

(*
 * 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 DataStream

(* Application-level bytes streams exchanged over TLS;            *)
(* depending on the safety of their indexes,                      *)
(* these streams are treated abstractly by our TLS implementation *)

open TLSInfo
open Bytes
open Error
open Range

/// Auxiliary functions for ranges

private val min: a:nat -> b:nat -> c:nat{(a<=b /\ c=a) \/ (a>b /\ c=b)}
private val max: a:nat -> b:nat -> c:nat{(a>=b /\ c=a) \/ (a<b /\ c=b)}

val splitRange: ki:succEpoch -> r:range -> (r0:range * r1:range){r = Sum(r0,r1)}

/// Bytestreams

// we communicate deltas indexed by all preceding bytes on the stream.
// TLS guarantees abstraction for every delta with a safe index;
// this is the main basis for application-level integrity and secrecy

// used only as a ghost index:
// streams have no destructors, so they do not leak secrets
// they are used abstractly by TLS, except that
// their logical definition is needed for authentication in application code.
private type (;ki:epoch) stream = {sb:bytes list}

// the implementation of this type is application-specific
// but it must provide the following functions to TLS
private type (;ki:epoch, h:(;ki)stream, r:range) delta = {contents: (;r) rbytes}

function val Payload: e:epoch * s:(;e)stream * r:range * (;e,s,r)delta -> 'a // (;r)rbytes
private definition !e,s,r,d. Payload(e,s,r,d) = d.contents

function val EmptyStream: e:epoch -> (;e)stream
private definition !e. EmptyStream(e) = {sb = []}

function val ExtendStream: 'a * 'b * 'c * 'd -> 'e
private definition !ki,s,r,d. ExtendStream(ki,s,r,d) = {sb = d.contents :: s.sb }

function val StreamBytes: e:epoch * (;e)stream -> bytes
private definition !e,s,h,t.
 (s.sb = []   /\ StreamBytes(e,s) = [||]) \/
 (s.sb = h::t /\ StreamBytes(e,s) = (StreamBytes(e,{sb=t}) @| h))

ask !e. StreamBytes(e,EmptyStream(e)) = [||]
ask !e,s,r,d. StreamBytes(e,ExtendStream(e,s,r,d)) = ( StreamBytes(e,s) @| Payload(e,s,r,d) )

// The following two functions are
// used only by the application.
// They are never called from TLS.
val createDelta:
  ki:epoch -> s:(;ki) stream -> r:range ->
  b:(;r) rbytes -> c: (;ki,s,r) delta
val deltaBytes:
  ki:epoch -> s:(;ki) stream -> r:range ->
  c: (;ki,s,r) delta -> b:(;r) rbytes

// used by TLS
val init: e:epoch -> s:(;e)stream{s=EmptyStream(e)}
val append:
  ki:epoch -> s: (;ki) stream -> r:range ->
  d:(;ki,s,r) delta -> s':(;ki) stream{s' = ExtendStream(ki,s,r,d)}

val deltaPlain:
  ki:epoch{not Auth(ki)} -> s:(;ki) stream -> r:range ->
  b:(;r) rbytes -> d: (;ki,s,r) delta {b = Payload(ki,s,r,d)}
val deltaRepr:
  ki:epoch{not Safe(ki)} -> s:(;ki) stream -> r:range ->
  d: (;ki,s,r) delta -> b:(;r) rbytes{b = Payload(ki,s,r,d)}

val split: ki:epoch -> s:(;ki) stream ->
  r0:range -> r1:range -> d:(;ki,s,Sum(r0,r1)) delta ->
  (d0:(;ki,s,r0) delta * d1:(;ki,ExtendStream(ki,s,r0,d0),r1) delta){
	Payload(ki,s,Sum(r0,r1),d) =
		Payload(ki,s,r0,d0) @| Payload(ki,ExtendStream(ki,s,r0,d0),r1,d1)
  }

val widen: ki:epoch -> s:(;ki) stream ->
  r0:range -> r1:range{SubRange(r0,r1)} -> d0:(;ki,s,r0) delta ->
  d1:(;ki,s,r1) delta{Payload(ki,s,r0,d0) = Payload(ki,s,r1,d1)}

A verified reference TLS implementation

miTLS :: DataStream

F# Interface: DataStream.fsi

F# Implementation: DataStream.fs

F7 Interface: DataStream.fs7

Verification status

Module list

Trusted

Idealized

Verified