miTLS :: AppData

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

open TLSInfo
open Bytes
open Error
open DataStream
open Range

type app_state

val inStream:  ConnectionInfo -> app_state -> stream
val outStream: ConnectionInfo -> app_state -> stream

val init: ConnectionInfo -> app_state

val writeAppData: ConnectionInfo -> app_state -> range -> AppFragment.fragment -> stream -> app_state

val next_fragment: ConnectionInfo -> app_state -> (range * AppFragment.fragment * app_state) option

val clearOutBuf: ConnectionInfo -> app_state -> app_state

val recv_fragment: ConnectionInfo ->  app_state -> range -> AppFragment.fragment -> app_state

val readAppData: ConnectionInfo -> app_state -> ((range * delta) option * app_state)

val reset_incoming:  ConnectionInfo -> app_state -> ConnectionInfo -> app_state

val reset_outgoing:  ConnectionInfo -> app_state -> ConnectionInfo -> app_state

F# Implementation: AppData.fs

module AppData

open Error
open Bytes
open TLSInfo
open DataStream
open Range

type input_buffer =  stream * (range * AppFragment.plain) option
type output_buffer =
    | NoneBuf of stream
    | SomeBuf of stream * range * AppFragment.plain * stream

type app_state = {
  app_incoming: input_buffer;
  app_outgoing: output_buffer;
}

let inStream  (c:ConnectionInfo) state =
    let (s,_) = state.app_incoming in s
let outStream (c:ConnectionInfo) state =
    match state.app_outgoing with
    | NoneBuf(s) -> s
    | SomeBuf(s,_,_,_) -> s

let init ci =
  let in_s = DataStream.init ci.id_in in
  let out_s = DataStream.init ci.id_out in
    {app_outgoing = (NoneBuf(out_s));
     app_incoming = (in_s,None)
    }

// Stores appdata in the output buffer, so that it will possibly sent on the network
let writeAppData (c:ConnectionInfo) (a:app_state) (r:range) (f:AppFragment.plain) (s':stream) =
    let s = outStream c a in
    {a with app_outgoing = SomeBuf(s,r,f,s')}

let noneBuf ki s = NoneBuf(s)
let some x = Some x
// When polled, gives Dispatch the next fragment to be delivered,
// and commits to it (adds it to the output stream)
let next_fragment (c:ConnectionInfo) (a:app_state) =
    let out = a.app_outgoing in
    match out with
    | NoneBuf(_) -> None
    | SomeBuf (s,r,f,s') ->
        let b' = noneBuf c.id_out s' in
        some (r,f,{a with app_outgoing = b'})

// Clear contents from the output buffer
let clearOutBuf (c:ConnectionInfo) (a:app_state) =
    let s = outStream c a in
    {a with app_outgoing = NoneBuf(s)}

// Gets a fragment from Dispatch, adds it to the incoming buffer, but not yet to
// the stream of data delivered to the user
let recv_fragment (ci:ConnectionInfo)  (a:app_state)  (r:range) (f:AppFragment.fragment) =
    // pre: snd a.app_incoming = None
    let (s,_) = a.app_incoming in
    let rf = (r,f) in
    {a with app_incoming = (s,Some(rf))}

// Returns the buffered data to the user, and stores them in the stream
let readAppData (c:ConnectionInfo) (a:app_state) =
  let (s,data) = a.app_incoming in
    match data with
      | None -> None,a
      | Some(rf) ->
          let (r,f) = rf in
          let (d,ns) = AppFragment.delta c.id_in s r f in
          let rd = (r,d) in
          Some(rd),{a with app_incoming = (ns,None)}

let reset_outgoing (ci:ConnectionInfo) (a:app_state) (nci:ConnectionInfo) =
  let out_s = DataStream.init nci.id_out in
    {a with
       app_outgoing = NoneBuf(out_s)
    }

let reset_incoming (ci:ConnectionInfo) (a:app_state) (nci:ConnectionInfo) =
  let in_s = DataStream.init nci.id_in in
    {a with
       app_incoming =  (in_s,None)
    }

F7 Interface: AppData.fs7

module AppData

open TLSInfo
open Bytes
open Error
open DataStream
open Range

private type (;ki:epoch) input_buffer =
	h:(;ki) stream * (r:range * f:(;ki,r)AppFragment.fragment
	{Auth(ki) => AppFragment.Sent(ki,h,r,f)}) option
private type (;ki:epoch) output_buffer =
	| NoneBuf of (;ki)stream
	| SomeBuf of s:(;ki) stream * r:range * f:(;ki,r)AppFragment.fragment *
				 s':(;ki)stream{s' = AppFragment.Extend(ki,s,r,f) /\
				 (Auth(ki) => AppFragment.Sent(ki,s,r,f))}

private type (;ci:ConnectionInfo) app_state = {
    app_incoming: (;ci.id_in) input_buffer;
    app_outgoing: (;ci.id_out) output_buffer;
}

private function val AppInStream_int: e:epoch * (;e)input_buffer -> 'a
private definition !e,st,d. AppInStream_int(e,(st,d)) = st
private function val AppOutStream_int: e:epoch * (;e)output_buffer -> 'a
private definition !e,s. AppOutStream_int(e,NoneBuf(s)) = s
private definition !e,s,r,f,s'.	AppOutStream_int(e,SomeBuf(s,r,f,s')) = s

function val AppInStream:  ci:ConnectionInfo * (;ci)app_state -> 'a //(;ci.id_in) stream
function val AppOutStream: ci:ConnectionInfo * (;ci)app_state -> 'a //(;ci.id_out)stream
private definition !ci,s. AppInStream(ci,s) = AppInStream_int(ci.id_in,s.app_incoming)
private definition !ci,s. AppOutStream(ci,s) = AppOutStream_int(ci.id_out,s.app_outgoing)

private function val AppInBuf_int: e:epoch * (;e)input_buffer -> 'a
private definition !e,st,d. AppInBuf_int(e,(st,d)) = d
private function val AppOutBuf_int: e:epoch * (;e)output_buffer -> 'a
private definition !e,s. AppOutBuf_int(e,NoneBuf(s)) = None
private definition !e,s,r,f,s'.	AppOutBuf_int(e,SomeBuf(s,r,f,s')) = Some((r,f,s'))

function val AppInBuf:  ci:ConnectionInfo * (;ci)app_state -> 'a //(range * AppFragment.plain) option
function val AppOutBuf: ci:ConnectionInfo * (;ci)app_state -> 'a //(range * AppFragment.plain * stream) option
private definition !ci,s. AppInBuf(ci,s) = AppInBuf_int(ci.id_in,s.app_incoming)
private definition !ci,s. AppOutBuf(ci,s) = AppOutBuf_int(ci.id_out,s.app_outgoing)

val inStream:  ci:ConnectionInfo -> s:(;ci)app_state -> st:(;ci.id_in) stream{st = AppInStream(ci,s) }
val outStream: ci:ConnectionInfo -> s:(;ci)app_state -> st:(;ci.id_out)stream{st = AppOutStream(ci,s)}

val init: ci:ConnectionInfo ->
	s:(;ci)app_state{AppInBuf(ci,s) = None /\ AppOutBuf(ci,s) = None /\
		AppInStream(ci,s) = EmptyStream(ci.id_in) /\ AppOutStream(ci,s) = EmptyStream(ci.id_out)}

val writeAppData: ci:ConnectionInfo -> s:(;ci)app_state ->
	r:range -> f:(;ci.id_out,r)AppFragment.fragment{Auth(ci.id_out) => AppFragment.Sent(ci.id_out,AppOutStream(ci,s),r,f)} ->
	st:(;ci.id_out)stream{st = AppFragment.Extend(ci.id_out,AppOutStream(ci,s),r,f)} ->
	s':(;ci)app_state{AppOutBuf(ci,s') = Some((r,f,st)) /\
		AppInBuf(ci,s') = AppInBuf(ci,s) /\
		AppOutStream(ci,s') = AppOutStream(ci,s) /\
		AppInStream (ci,s') = AppInStream (ci,s)}

private val noneBuf: e:epoch -> s:(;e) stream -> o:(;e) output_buffer{o = NoneBuf(s)}
private val some: x:'a -> o:'a option{o = Some(x)}

val next_fragment: ci:ConnectionInfo{IsSuccEpoch(ci.id_out)} ->
  s:(;ci)app_state ->
  ro:((r:range * f:(;ci.id_out,r)AppFragment.fragment * s':(;ci)app_state)
	{(Auth(ci.id_out) => AppFragment.Sent(ci.id_out,AppOutStream(ci,s),r,f) ) /\
	  AppOutStream(ci,s') = AppFragment.Extend(ci.id_out,AppOutStream(ci,s),r,f) /\
	  AppOutBuf(ci,s) = Some((r,f,AppFragment.Extend(ci.id_out,AppOutStream(ci,s),r,f))) /\
	  AppOutBuf(ci,s') = None /\
	  AppInBuf(ci,s') = AppInBuf(ci,s) /\
	  AppInStream (ci,s') = AppInStream (ci,s)}) option{
    ro = None => AppOutBuf(ci,s) = None}

val clearOutBuf: ci:ConnectionInfo -> s:(;ci)app_state ->
	s':(;ci)app_state{
		AppOutStream(ci,s') = AppOutStream(ci,s) /\
		AppOutBuf(ci,s') = None /\
		AppInStream(ci,s') = AppInStream(ci,s) /\
		AppInBuf(ci,s') = AppInBuf(ci,s)
		}

val recv_fragment: ci:ConnectionInfo -> s:(;ci)app_state -> r:range ->
	f:(;ci.id_in,r)AppFragment.fragment{Auth(ci.id_in) =>
		AppFragment.Sent(ci.id_in,AppInStream(ci,s),r,f)} ->
	s':(;ci)app_state{AppInBuf(ci,s') = Some((r,f)) /\
		AppOutStream(ci,s') = AppOutStream(ci,s) /\
		AppInStream (ci,s') = AppInStream (ci,s)}

val readAppData: ci:ConnectionInfo -> s:(;ci)app_state ->
	((r:range * (;ci.id_in,AppInStream(ci,s),r)delta) option * s':(;ci)app_state){AppInBuf(ci,s') = None /\
		AppOutStream(ci,s') = AppOutStream(ci,s) /\
		( (AppInBuf(ci,s) = None /\ AppInStream(ci,s') = AppInStream(ci,s)) \/
		  (?r,f. AppInBuf(ci,s) = Some((r,f)) /\ AppInStream(ci,s') = AppFragment.Extend(ci.id_in,AppInStream(ci,s),r,f))
		)}

val reset_outgoing: ci:ConnectionInfo -> s:(;ci)app_state ->
	ci':ConnectionInfo{ci'.role = ci.role /\ ci'.id_in = ci.id_in} ->
	s':(;ci')app_state{AppOutBuf(ci',s') = None /\
            AppOutStream(ci',s') = EmptyStream(ci'.id_out) /\
            AppInStream(ci',s') = AppInStream(ci,s)}
val reset_incoming: ci:ConnectionInfo -> s:(;ci)app_state ->
	ci':ConnectionInfo{ci'.role = ci.role /\ ci'.id_out = ci.id_out} ->
	s':(;ci')app_state{AppInBuf(ci',s') = None /\
            AppInStream(ci',s') = EmptyStream(ci'.id_in) /\
            AppOutStream(ci',s') = AppOutStream(ci,s)}

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 DataStream AppFragment

miTLS

A verified reference TLS implementation

miTLS :: AppData

F# Interface: AppData.fsi

F# Implementation: AppData.fs

F7 Interface: AppData.fs7

Verification status

Module list

Trusted

Idealized

Verified