Dsls For Network Protocols

Domain Specific Languages for Network Protocols Saleem Bhatti, Edwin Brady, Kevin Hammond and James McKinna [email protected]

University of St Andrews NGNA 2009, June 22nd 2009

NGNA 2009, June 22nd 2009 – p.1/20

Introduction Next Generation Network Protocols will encompass a wide range of existing requirements, and certain applications may also require:  Rapid prototyping of application protocols  Strong verification of behaviour and properties

NGNA 2009, June 22nd 2009 – p.2/20

Our Methodology

Edwin + Saleem +

= Eureka!

NGNA 2009, June 22nd 2009 – p.3/20

Mantra

“Programs must be written for people to read, and only incidentally for machines to execute.” — H. Abelson and G.J. Sussman (Structure and Interpretation of Computer Programs)

NGNA 2009, June 22nd 2009 – p.4/20

Domain Specific Languages A Domain Specific Language (DSL) is a language designed for a particular problem domain.  Allows a user to focus on the high level of a problem

domain, rather than the low level details of a general purpose language.  Identify the general properties, requirements and

operations in the domain. We outline the construction of a DSL for a simple transport protocol.

NGNA 2009, June 22nd 2009 – p.5/20

Protocol Correctness Protocol correctness can be verified by model-checking a finite-state machine. However:  There may be a large number of states and

transitions.  The model is needed in addition to the implementation. Model-checking is therefore not self-contained. It can verify a protocol, but not its implementation.

NGNA 2009, June 22nd 2009 – p.6/20

Protocol Correctness In our approach we construct a self-contained domain-specific framework in a dependently-typed language.  We can express correctness properties in the

implementation itself.  We can express the precise form of data and ensure

it is validated.  We aim for Correctness By Construction.

NGNA 2009, June 22nd 2009 – p.7/20

ARQ Our simple transport protocol:  Automatic Repeat Request (ARQ)  Separate sender and receiver  State  Session state (status of connection)  Transmission state (status of transmitted data)

NGNA 2009, June 22nd 2009 – p.8/20

Session State

NGNA 2009, June 22nd 2009 – p.9/20

Transmission State

NGNA 2009, June 22nd 2009 – p.10/20

Session Management  START — initiate a session  START_RECV_ACK

— wait for the receiver to be ready

 END — close a session  END_RECV_ACK

— wait for the receiver to close  TIMEOUT — give up waiting

NGNA 2009, June 22nd 2009 – p.11/20

Session Management  START — initiate a session  START_RECV_ACK

— wait for the receiver to be ready

 END — close a session  END_RECV_ACK

— wait for the receiver to close  TIMEOUT — give up waiting

When are these operations valid? What is their effect on the state? How do we apply them correctly?

NGNA 2009, June 22nd 2009 – p.11/20

Session Management We would like to express contraints on these operations, describing when they are valid, e.g.: Command

Precondition

Postcondition

START

CLOSED

OPENING

START_RECV_ACK

OPENING

OPEN (if ACK received) OPENING (if nothing received)

END

OPEN

CLOSING

END_RECV_ACK

CLOSING

CLOSED (if ACK received) CLOSED (if nothing received)

TIMEOUT

Timeout

CLOSED

NGNA 2009, June 22nd 2009 – p.12/20

Dependent Types Allow types to be parameterised by values, giving a more precise description of data. e.g.: xs : List — A monomorphic list

NGNA 2009, June 22nd 2009 – p.13/20

Dependent Types Allow types to be parameterised by values, giving a more precise description of data. e.g.: xs : List — A monomorphic list ys : List Int — A list of integers

NGNA 2009, June 22nd 2009 – p.13/20

Dependent Types Allow types to be parameterised by values, giving a more precise description of data. e.g.: xs : List — A monomorphic list ys : List Int — A list of integers zs : List Int 5 — A list of integers, length 5

NGNA 2009, June 22nd 2009 – p.13/20

Dependent Types Allow types to be parameterised by values, giving a more precise description of data. e.g.: xs : List — A monomorphic list ys : List Int — A list of integers zs : List Int 5 — A list of integers, length 5

So the type of a function can also express a property of that function, e.g.: append : List a n -> List a m -> List a (n + m)

NGNA 2009, June 22nd 2009 – p.13/20

Sessions, Dependently Typed How do we express our session state machine?  Make each transition an operation in a DSL.  Defining the abstract syntax of the DSL language as

a dependent type.  Implement an interpreter for the abstract syntax.

NGNA 2009, June 22nd 2009 – p.14/20

Session State, Formally State carries the session state, i.e. states in the FSM, plus additional data: data State = | | |

CLOSED OPEN PState -- onne tion state CLOSING Nat -- timeout OPENING Nat -- timeout

Pstate carries the connection state. An open connection is either waiting for an ACK or ready to send the next packet. data PState = Waiting Seq Nat -- seq. no. and timeout | Ready Seq -- seq. no.

NGNA 2009, June 22nd 2009 – p.15/20

Sessions, Formally ARQLang is a data type defining the abstract syntax of our DSL, encoding state transitions in the type: data ARQLang : State -> State -> # -> # where START : (timeout:Nat) -> (ARQLang CLOSED (OPENING timeout) ()) | START_RECV_ACK : (if_ok: ARQLang (OPEN (Ready First)) B Ty) -> (if_fail: ARQLang (OPENING timeout) B Ty) -> (ARQLang (OPENING timeout) B Ty) ...

NGNA 2009, June 22nd 2009 – p.16/20

Session Management

Command

Precondition

Postcondition

START

CLOSED

OPENING

START_RECV_ACK

OPENING

OPEN (if ACK received) OPENING (if nothing received)

END

OPEN

CLOSING

END_RECV_ACK

CLOSING

CLOSED (if ACK received) CLOSED (if nothing received)

TIMEOUT

Timeout

CLOSED

NGNA 2009, June 22nd 2009 – p.17/20

Protocol Implementation Functions explain each state transition, or composition of transitions, in terms of allowed operations, e.g.:  open : (timeout : Nat) -> ARQLang CLOSED (OPENING timeout) ()

The types guarantee that the operations are executed in an order consistent with the state machine.

NGNA 2009, June 22nd 2009 – p.18/20

Protocol Implementation Functions explain each state transition, or composition of transitions, in terms of allowed operations, e.g.:  open : (timeout : Nat) -> ARQLang CLOSED (OPENING timeout) ()  lose : ARQLang (CLOSING y) CLOSED ()

The types guarantee that the operations are executed in an order consistent with the state machine.

NGNA 2009, June 22nd 2009 – p.18/20

Protocol Implementation Functions explain each state transition, or composition of transitions, in terms of allowed operations, e.g.:  open : (timeout : Nat) -> ARQLang CLOSED (OPENING timeout) ()  lose : ARQLang (CLOSING y) CLOSED ()  session : ARQLang CLOSED CLOSED ()

The types guarantee that the operations are executed in an order consistent with the state machine.

NGNA 2009, June 22nd 2009 – p.18/20

Protocol Implementation Functions explain each state transition, or composition of transitions, in terms of allowed operations, e.g.:  open : (timeout : Nat) -> ARQLang CLOSED (OPENING timeout) ()  lose : ARQLang (CLOSING y) CLOSED ()  session : ARQLang CLOSED CLOSED ()  session' : ARQLang (OPEN (Ready First)) (OPEN (Ready n)) -> ARQLang CLOSED CLOSED ()

The types guarantee that the operations are executed in an order consistent with the state machine.

NGNA 2009, June 22nd 2009 – p.18/20

Protocol Implementation Finally, we define an interpreter which executes these operations, parameterised by the host name and port number of the receiver.  interp : (host : String) -> (port : Int) ->

ARQLang x y t -> IO t

 The protocol designer defines everything in terms of

ARQLang.

 Only interp executes any low level operations (e.g.

physical layer).

NGNA 2009, June 22nd 2009 – p.19/20

Conclusions and Future Work  Built a simple transport protocol with ARQ as proof

of concept.  The model and proof of correctness together are the

implementation.  We have now begun a project to develop our ideas

further. We are particularly interested in  Adaptivity  Uncertainty  Immediate goals: larger scale implementation,

interoperability with C/Java implementations, efficiency.

NGNA 2009, June 22nd 2009 – p.20/20