Developing a programming language for Active Networks

Alan Jeffrey

CTI, DePaul University, Chicago

Joint work with Ian Wakeman, Tim Owen and Rory Graves (University of Sussex)

Overview

Active networks.

The SafetyNet project.

Programming model.

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?

Example of run-time speedup

Every method call or field access in Java has to check for null pointer exceptions.

This is because Java allows all classes to have a null value.

In SafetyNet, we have a special class:

  class Maybe[Data] { ... }

We can distinguish in the type system between Int (guaranteed to contain an int) and Maybe[Int] (might be empty).

We also insist all fields are initialized before an object can be used.

Result: no more null pointer exceptions!

SafetyNet project

The SafetyNet project is current work-in-progress.

The plan is to design and implement a network programming language with:

Key ideas:

Design philosophy

Remove run-time checks wherever possible.

Use the type system to avoid compromising safety.

Use generic libraries rather than add language features.

Use language features from recent research in semantics of distributed / OO languages.

Fast prototyping, driven by examples.

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

A class which accesses a remote method:
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] {
   method send (p : packet) {
      if (at dest) {
         port.send (p);
      } else {
         spawn at route dest {
            new RemoteStream [Packet]
               (dest, port).send (p);
         }
     }
}

Example: remote method 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 acknowlegement.

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
These can be presented graphically (work in progress).

Semantics: stuctural 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.

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. Done some.

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

Include security and digital signatures.  Still to do

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

Check principal typing.  Still to do

Implement a prototype compiler.  Done some.

Try out on real examples!  Done some.

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