Developing programming languages for Active Networks

Alan Jeffrey
 
 
 
 
 
 
 
 
COGS, University of Sussex, Brighton
Visiting CTI, DePaul University, Chicago

Overview

Active networks.

The SafetyNet project.

Related work.

Networked resource calculus.

Semantics.

Types.

Futher work.

Active Networks

In a traditional network topology, `smart' hosts are linked by `dumb' routers:
In reality, a router is often pretty smart.

An AN allows users to make use of the computing power in the routers:

Example Active Networks

Implement multicast on top of broadcast:
Active multicast networks can take advantage of processing power at the relays.

For example, an active relay can perform application-specific compression for low-bandwidth links.

Example Active Networks

`On the fly' firewalls:
Makes firewall deployment lightweight.

Example Active Networks

Intelligent agents.

Scaleable VR.

Application-specific protocols.

Application-specific proxies.

...

Problems with ANs

Switch managers are right to be worried about ANs. To be usable, ANs must not:
Add a notable performance overhead.

Compromise network integrity.

For example, if arbitrary C code were executed:
Security violations from dereferencing arbitrary memory.

Denial of Service attacks from flooding the network with packets or processes.

Why not Java?

Java solves some problems, eg banning pointer arithmetic, but at a run-time cost.

For example, each array assignment requires a bounds test and a run-time type test.

Can we achieve security and safety without requiring costly run-time checks?

SafetyNet

The goals of the SafetyNet project are to apply semantic techniques to networking problems.

To develop safety and security policies for ANs.

To design a typed language for programming ANs.

To show that any type-safe program will satisfy the safety and security policies.

To provide prototype implementations and simulation tools.

PIs: Alan Jeffrey (semantics gun for hire) and Ian Wakeman (networks expert), both University of Sussex.

Programming model

A network consists of a graph of locations.

At each location, there is a collection of resources and a collection of executing threads.

Threads may access existing resources, or register new resources.

Threads may spawn subthreads, and may migrate to neighbouring locations.

Threads can find out local information about the network, eg the next hop to a location, but not global information.

The language is statically typed, with a formal model of a `core' language.

Example: remote function access

A function which accesses a remote function:
serializable function remoteAccess (
  dest : location,
   packet : serializable type,
   port : at dest
      resource function (pdu : packet),
   pdu : packet
) {
   if (dest == localhost) {
      access port (pdu);
   } else {
      spawn at route dest
         remoteAccess (dest, packet, port, pdu);
   }
}

Related work

Language design work is based on:
Milner, Parrow and Walker's pi-calculus.

Boudol's blue-calculus.

Fournet, Gonthier, Lévy, Maranget and Rémy's join calculus.

Moggi's monadic meta-language.

Girard  / Reynolds' 2nd order lambda-calculus.

Hennessy and Riely's / Sewell's distributed pi-calculus.

Cardelli and Gordon's ambients.

Future work will be based on:
Benton, Bierman, Hyland, de Paiva's linear lambda-calculus.

Abadi and Gordon's spi-calculus.

Closest AN work is Gunter et al's PLAN.

Networked resource calculus

In this model, a network is a soup of located threads performing computations and located resources containing data.

For eample, one possible network is:

   l[register r = 0]
 | m[at l register s = access r + 1]
This reduces to (by migration):
   l[register r = 0]
 | l[register s = access r + 1]
then (by resource fetching):
   l[register r = 0]
 | l[register s = 1]

Syntax

The impredicative polymorphic lambda-calculus with tuples, recursive functions and let declarations.

Add a language of threads t including resource registration register r = v.

Add an expression for resource access access r.

Add declarations for new resources new r : T; and to spawn threads spawn t;.

The syntax of networks is:

 
N ::= 0 | N|N | l[t] | new r : T; N
 

Semantics: stuctural congruence

Generated by (with some side-conditions on variables):
 
(M | N) | O
 M | (N | O)
M | N N | M
M | 0 M
new x : T; N new y : T; N[y / x]
new x : T; (M | N) (new x : T; M) | N
new x : T; 0 0
l[let p = D e; t] l[D let p = e; t]  
 

Semantics: reduction precongruence

Generated by `usual functional stuff':
 
l[let p = v; t]
  l[t[v/p]]
l[let p = v w; t]
  l[let p = e[v/x,w/q]; t]
   (when v = function x q { e })
l[if (m == m) {D} else {E} t]
  l[D t]
l[if (m == n) {D} else {E} t]
  l[E t]   (when m  n)
 

Semantics: reduction precongruence

Additional rules for networking (where l  m means there is a link from l to m):
 
l[spawn t; u]
  l[t] | l[u]
l[register x = v] | l[let p = access x; t]
  l[register x = v] | l[let p = v; t]
l[new x : T; t]
  new x : T; l[t]
l[at m t]
  m[t]   (when l  m)
l[let p = localhost; t]
  l[let p = l; t]
l[let p = route m; t]
  l[let p = n; t]         (when l  n)
 

Example

A packet forwarder taking a few hops source  hop1  hop2  target:
s = remoteAccess (target, int, port, 0);

s' = if(target == localhost) {access port (0)}
       else {spawn at route target s}

s'' = spawn at route target s

t = register port (x : int) { ...x... }

This can reduce (writing  for (  )*) :
     source [s] | target [t]
source [s'] | target [t]
source [s''] | target [t]
hop1 [s] | target [t]
hop2 [s] | target [t]
target [s] | target [t]
target [s'] | target [t]
target [access port (0)] | target [t]
target [...0...] | target [t]

Types

We can typecheck the networked resource calculus with judgements:
  e : T
  t : thread
  N : network
We can then verify:
Type safety: any well-typed program satisfies the required safety and security conditions.

Subject reduction: any well-typed program stays well-typed.

Together, these properties mean that any well-typed program will always satisfy the safety and security conditions.

Types

For example, we can verify the safety properties:
Any resource of type at l resource T is only accessed at location l.

Any resource of type at l resource T is only ever registered with values of type T.

Any resource of type at l resource function (T) is only ever accessed with values of type T.

and the subject reduction property:
If N  M and  N : network then  M : network

Future work

There is still a lot of work to be done:
`Scale up' to a real programming language.

Develop and formalize `real world' safety and security policies.

Add linear types (for time-to-live counts or charging mechanisms).

Include security and digital signatures.

Include a `web of trust' model based on Hennessy and Riely.

Check principal typing.

Try out on real examples!

http://klee.cs.depaul.edu/an/