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 Tcp

open Bytes
open Error

type NetworkStream
type TcpListener

(* Create a network stream from a given stream.
   Only used by the application interface TLSharp. *)

val create: System.IO.Stream -> NetworkStream

(* Server side *)

val listen: string -> int -> TcpListener
val acceptTimeout: int -> TcpListener -> NetworkStream
val accept: TcpListener -> NetworkStream
val stop: TcpListener -> unit

(* Client side *)

val connectTimeout: int -> string -> int -> NetworkStream
val connect: string -> int -> NetworkStream

(* Input/Output *)

// val dataAvailable: NetworkStream -> bool Result
val read: NetworkStream -> int -> bytes Result
val write: NetworkStream -> bytes -> unit Result
val close: NetworkStream -> unit

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

open System.Net
open System.Net.Sockets
open Bytes
open Error

type NetworkStream = N of System.IO.Stream
type TcpListener = T of System.Net.Sockets.TcpListener

let create s = N(s)

(* Server side *)

let listen addr port =
    let tcpList = new System.Net.Sockets.TcpListener(IPAddress.Parse(addr),port) in
    tcpList.Server.SetSocketOption(SocketOptionLevel.Socket, SocketOptionName.ReuseAddress, true);
    tcpList.Start();
    T tcpList

let acceptTimeout timeout (T tcpList) =
    let client = tcpList.AcceptTcpClient() in
    client.ReceiveTimeout <- timeout;
    client.SendTimeout <- timeout;
    N (client.GetStream())

let accept t =
    acceptTimeout 0 t

let stop (T tcpList) =
    tcpList.Stop()

(* Client side *)

let connectTimeout timeout addr port =
    let tcpCl = new TcpClient(addr,port) in
    tcpCl.ReceiveTimeout <- timeout;
    tcpCl.SendTimeout <- timeout;
    N (tcpCl.GetStream())

let connect addr port =
    connectTimeout 0 addr port

(* Input/Output *)

let rec read_acc (N ns) nbytes prev =
    if nbytes = 0 then
        Correct (prev)
    else
        try
            let buf = Array.zeroCreate nbytes in
            let read = ns.Read (buf, 0, nbytes) in
            if read = 0 then
                Error(AD_internal_error,"TCP connection closed")
            else
                let rem = nbytes - read in
                read_acc (N ns) rem (Array.append prev (Array.sub buf 0 read))
        with
            | _ -> Error(AD_internal_error, perror __SOURCE_FILE__ __LINE__ "TCP connection closed")

let read (N ns) nbytes =
    try
        read_acc (N ns) nbytes (Array.zeroCreate 0)
    with
        | _ -> Error (AD_internal_error, perror __SOURCE_FILE__ __LINE__ "TCP connection closed")

let write (N ns) content =
    try
        Correct (ns.Write (content, 0, content.Length))
    with
        | _ -> Error (AD_internal_error, perror __SOURCE_FILE__ __LINE__ "TCP connection closed")

let close (N ns) =
    ns.Close()

A verified reference TLS implementation

miTLS :: Tcp

F# Interface: Tcp.fsi

F# Implementation: Tcp.fs

F7 Interface: Tcp.fs7

Verification status

Module list

Trusted

Idealized

Verified