Developing a programming language for Active Networks

Alan Jeffrey
 
 
 
 
 
 
 

CTI, DePaul University, Chicago
COGS, University of Sussex, Brighton

Joint work with Ian Wakeman, Tim Owen and Rory Graves, Sussex

Overview

Active networks.

The SafetyNet project.

Programming model.

Semantics.

Types.

Further 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.

Scalable 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.

All objects are heap allocated.

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.

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 stream access

class OutStream
<serializable class Packet> {
   abstract method send (p : packet);
}

class RemoteStream
<serializable class Packet> (
   dest : location,
   port : OutStream <Packet> at dest
) extends OutStream <Packet> {
   field dest : ... = dest;
   field port : ... = port;
   method send (p : packet) {
      if (at dest) {
         port.send (p);
      } else {
         spawn at route dest {
           new RemoteStream <Packet>
             (dest, port).send (p);
         }
     }
}

Example: remote stream access

Or without creating a new object each time:
class Forwarder {
   static method forward
   <serializable class Packet> (
      dest : location,
      port : OutStream <Packet> at dest,
      p : packet
   ) {
      if (at dest) {
         port.send (p);
      } else {
         spawn at route dest {
            Forwarder.forward <Packet>
             (dest, port, p);
         }
      }
   }
}

Object-oriented model

Class-based polymorphic OO language.

Objects are either local (no remote references) or global (can be referred to by other locations).

Local objects have type Foo, global objects have type Foo at Loc.

Only serializable data can be migrated between locations.

Objects can be stack-based (eg foo) or heap-based (eg Foo).  Stack-based objects may be serialized, heap-based objects are not.

Classes are cached, shared resources.  The first time a class is used at a location, it is loaded, after that the cached copy is used.

Network model

Remote thread spawning is best-effort with no acknowledgement.

RPC is derived, not primitive!

Primitive is spawn at route Location { Thread }.

Network topology is dynamic.

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.

Abadi and Cardelli's object calculus

Gordon's concurrent object calculus

Odersky, Wadler et al's Generic Java

Closest AN work is Gunter et al's PLAN.

Formal model

A network consists of a collection of located resources and threads.  Subnetworks may have shared secrets.
Network ::=
   Loc [Thread] |
   Loc <Id = Resource> |
   Network | Network |
   0 |
   secret Id; Network
Resources are classes, objects or unknown:
Resource ::=
   class extends Class { ClassBody }
   object Class { Fields }
   unknown

Formal model graphically

Semantics: structural congruence

Generated by (with some side-conditions on variables):
 
(M | N) | O
 M | (N | O)
M | N N | M
M | 0 M
secret x; N secret y; N[y / x]
secret x; (M | N) (secret x; M) | N
secret x; 0 0
secret x; N secret x; L<x = unknown>  
Last rule requires L<x = ...> not in N.

Semantics: reduction precongruence

Reduction is given by approx. 30 rules, such as:
 
L[let P = O.F; T] |
L<O = object C {...field F = V;...}>
L[let P = V; T] |
L<O = object C {...field F = V;...}>
The rules include a formal treatment of an object-oriented class-based language, including class loading.

Example reduction

Types

We can typecheck the SafetyNet language with judgements:
Exp : Type
Network : 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.

Future work

There is still a lot of work to be done:
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.

Provide a versioning model.

Check principal typing.

Try out on real examples!

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