miTLS :: Bytes

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

type nat = int
type bytes = byte[]
type lbytes = bytes

val createBytes: int -> int -> bytes

val bytes_of_int: int -> int -> bytes

val int_of_bytes: bytes -> int

val length: bytes -> int

val equalBytes: bytes -> bytes -> bool

(* append *)
val (@|): bytes -> bytes -> bytes
val split: bytes -> int -> (bytes * bytes)
val split2: bytes -> int -> int -> (bytes * bytes * bytes)
(* strings *)
val utf8: string -> bytes
val iutf8: bytes -> string

(* Time spans *)
type DateTime
type TimeSpan
val now: unit -> DateTime
val newTimeSpan: nat -> nat -> nat -> nat -> TimeSpan
val addTimeSpan: DateTime -> TimeSpan -> DateTime
val greaterDateTime: DateTime -> DateTime -> bool

(* List operations *)

val fold: (bytes -> bytes -> bytes) -> bytes -> bytes list -> bytes
val filter: ('a -> bool) -> 'a list -> 'a list // In HS, only used with 'a = HT_type, but it's not defined here.
val foldBack: (bytes -> bytes -> bytes) -> bytes list -> bytes -> bytes
val exists: ('a -> bool) -> 'a list -> bool
val memr: 'a list -> 'a -> bool when 'a : equality
val choose: ('a -> 'b option) -> 'a list -> 'b list // Not used parametrically in HS, but types are not defined here.
val tryFind: ('a -> bool) -> 'a list -> 'a option
#if ideal

val find: ('a -> bool) -> 'a list -> 'a
//val assoc: 'a -> ('a * 'b) list -> 'b option
//val assoc2_1: ('a*'b) -> ('a * 'b *'c) list -> 'b option
#endif
val listLength: ('a list) -> int
val listHead: ('a list) -> 'a

val random: nat -> bytes

F# Implementation: Bytes.fs

module Bytes

type nat = int
type bytes = byte[]

let length (d:bytes) = d.Length
type lbytes = bytes

let createBytes len (value:int) : bytes =
    try Array.create len (byte value)
    with :? System.OverflowException -> failwith "Default integer for createBytes was greater than max_value"

let bytes_of_int nb i =
  let rec put_bytes bb lb n =
    if lb = 0 then failwith "not enough bytes"
    else
      begin
        Array.set bb (lb-1) (byte (n%256));
        if n/256 > 0 then
          put_bytes bb (lb-1) (n/256)
        else bb
      end
  in
  let b = Array.zeroCreate nb in
    put_bytes b nb i

let int_of_bytes (b:bytes) : int =
    List.fold (fun x y -> 256 * x + y) 0 (List.map (int) (Array.toList b))

//@ Constant time comparison (to mitigate timing attacks)
//@ The number of byte comparisons depends only on the lengths of both arrays.
let equalBytes (b1:bytes) (b2:bytes) =
    length b1 = length b2 &&
    Array.fold2 (fun ok x y -> x = y && ok) true b1 b2

let (@|) (a:bytes) (b:bytes) = Array.append a b
let split (b:bytes) i : bytes * bytes =
  Array.sub b 0 i,
  Array.sub b i (b.Length-i)
let split2 (b:bytes) i j : bytes * bytes * bytes =
  Array.sub b 0 i,
  Array.sub b i j,
  Array.sub b (i+j) (b.Length-(i+j))

let utf8 (x:string) : bytes = System.Text.Encoding.UTF8.GetBytes x
let iutf8 (x:bytes) : string = System.Text.Encoding.UTF8.GetString x

(* Time spans *)
type DateTime = DT of System.DateTime
type TimeSpan = TS of System.TimeSpan
let now () = DT (System.DateTime.Now)
let newTimeSpan d h m s = TS (new System.TimeSpan(d,h,m,s))
let addTimeSpan (DT(a)) (TS(b)) = DT (a + b)
let greaterDateTime (DT(a)) (DT(b)) = a > b

(* List operation functions. Currently only used by the Handshake. *)
let fold (op: bytes-> bytes-> bytes) state data = List.fold op state data
let filter f l = List.filter f l
let foldBack (f:bytes -> bytes -> bytes) bl s = List.foldBack f bl s
let exists f l = List.exists f l
let memr l x = List.exists (fun y -> x = y) l
let choose f l = List.choose f l
let tryFind f l = List.tryFind f l
#if ideal
let find f l = List.find f l

let rec assoc f l =
    match l with
      | (f',l')::_ when f=f' -> Some (f)
      | _::l                   -> assoc f l
      | []                       -> None
let rec assoc2_1 (f1,f2) l =
    match l with
      | (f1',f2',v)::_ when f1=f1' && f2=f2' -> Some (v)
      | _::l                   -> assoc2_1 (f1,f2) l
      | []                       -> None

let mem x l = List.exists (fun y -> x = y) l
#endif
let listLength (l:'a list) = l.Length
let listHead (l:'a list) = l.Head

let isSome (l:'a option) =
  match l with
      Some(x) -> true
    | None -> false

let random (n:nat) = CoreRandom.random n

F7 Interface: Bytes.fs7

module Bytes

(* Binary representations, using variable-length byte arrays *)
(* This module implementation is trusted, not verified *)

type nat = n:int {0 <= n} // a convenient abbreviation
type bytes = byte array

(* Lengths for arrays and lists *)

function val Length: bytes -> int
val length: b:bytes -> l:nat {Length(b) = l}
// lengths distribute over concatenations
assume !x:bytes, y:bytes. Length(x @| y) = Length(x) + Length(y)

type (;l:nat) lbytes = b:bytes {Length(b) = l}

function val ListLength: 'a list -> nat
assume ListLength(op_Nil()) = 0
assume !x,y. ListLength(op_ColonColon(x,y)) = 1 + ListLength(y)
assume !l. Length(array_of_list(l)) = ListLength(l)

val createBytes: l:int -> v:int { 0 <= v /\ v < 256 } -> (;l) lbytes

val equalBytes: b0:bytes -> b1:bytes ->
  r:bool {(r = true /\ b0 = b1) \/ (r = false /\ b0 <> b1)}

(* Array concatenation (append) *)
(* we use the infix operator @| both concretely and in formulas *)

val op_AtBar: b1:bytes -> b2:bytes -> b:bytes{b = b1 @| b2}
//val append: b1:bytes -> b2:bytes -> b:bytes{b = b1 @| b2}

val split:
  b:bytes -> i:nat{Length(b) >= i} ->
  b1:bytes * b2:bytes { Length(b1) = i /\ b = b1 @| b2 }

val split2: b:bytes -> i:nat -> j:nat  {Length(b) >= i+j} ->
  b1:bytes * b2:bytes * b3:bytes { Length(b1)=i /\ Length(b2)=j /\ b = b1 @| b2 @| b3}

// empty array is an identity for append
// assume !x. [||] @| x = x
assume !x. x @| [||] = x

// append is injective when using fixed lengths.
assume !b1,b2,c1,c2.
  (b1 @| b2 = c1 @| c2 /\ Length(b1)=Length(c1)) => (b1=c1 /\ b2=c2)

assume !b1,b2,c1,c2.
  (b1 @| b2 = c1 @| c2 /\ Length(b2)=Length(c2)) => (b1=c1 /\ b2=c2)

// append is associative
assume !b1,b2,b3. (b1 @| b2) @| b3 = b1 @| (b2 @| b3)

(* integer multi-byte representations *)

function val IntBytes: int * int -> bytes

val bytes_of_int: l:int -> i:int -> b:bytes{b = IntBytes(l,i)}
val int_of_bytes: b:bytes {Length(b)<=8} -> i:nat
  {b = IntBytes(Length(b),i) /\ (Length(b) = 1 => (0 <= i /\ i < 256)) }

// the first argument is the length of the representation
assume !l:int, i:int. Length(IntBytes(l,i)) = l
// the representation is injective
assume !l:int, i0:int, i1:int. IntBytes(l,i0) = IntBytes(l,i1) => i0=i1

(* string representation, used in sample apps *)

function val Utf8: string -> bytes
val utf8:  s:string -> b:bytes { b = Utf8(s) }
val iutf8: b:bytes -> s:string { b = Utf8(s) }

// utf8 is injective
assume !x:string, y:string. ( Utf8(x)=Utf8(y) => x = y )

(* Time spans *)

type DateTime
type TimeSpan
val now: unit -> DateTime
val newTimeSpan: nat -> nat -> nat -> nat -> TimeSpan
val addTimeSpan: DateTime -> TimeSpan -> DateTime
val greaterDateTime: DateTime -> DateTime -> bool

(* List operations *)

function val Unfold: bytes * bytes list -> bytes
function val UnfoldBack: bytes list * bytes -> bytes
val fold:     (bytes -> bytes -> bytes) -> s:bytes -> bl:bytes list -> b:bytes{b=Unfold(s,bl)}
val foldBack: (bytes -> bytes -> bytes) -> bl:bytes list -> s:bytes -> b:bytes{b=UnfoldBack(bl,s)}
val filter: ('a -> bool) -> 'a list -> 'a list
val exists: ('a -> bool) -> 'a list -> bool
val memr: 'a list -> 'a -> bool
val choose: ('a -> 'b option) -> 'a list -> 'b list
val tryFind: ('a -> bool) -> 'a list -> 'a option
val listLength: l:('a list) -> len:nat{ListLength(l)=len}
val listHead: l:('a list){ListLength(l) > 0} -> 'a
val find: ('a -> bool) -> 'a list -> 'a

(* random bytes generation *)

val random: n:nat -> b:bytes {Length(b)=n}

Verification status

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

Verification does not depend on other F7 interfaces.

miTLS

A verified reference TLS implementation

miTLS :: Bytes

F# Interface: Bytes.fsi

F# Implementation: Bytes.fs

F7 Interface: Bytes.fs7

Verification status

Module list

Trusted

Idealized

Verified