The Fox project, really about proof-carrying code

[Paul Dufresne]

Recently, some facts have made me take a look to the Fox project.
Before reading "The Fox project: Advanced Language Technology for
Extensible Systems" (CMU-CS-98-107), I was believing that the Fox
project was about doing an OS around ML.

I was wrong, and discover that the Fox project have much to do with
security as seen by Tunes. The Fox project is a DARPA founded research
project that study how to achieve security in Active Network. An active
network is a network in which a router can be reprogrammed by an active
packet.

One way to achieves the security would be by making dynamic checks and/or
have the active packet to contain code that would execute on an abstract
machine, much like Java. But the Fox project choose to do static checks.

So they decided to use Edingburg Logical Framework (don't ask me what
it is, I don't know) to do PCC (Proof-carrying code). The idea is to
have the router publicly make known it's security policy expressed in
Logical Framework, and then a certifying compiler can use this policy
to generate binaries accompanied by a proof that the binary code comply
with the public security policy.

My understanding is that they have some working certifying compiler
for a subset of C (no structs yet), and that they want to make a
more complete safe C-like language certifying compiler that they would
propose to be included in the Flux OS toolkit. They are also working on
some kind of Kaffe JVM with proof-carrying code to be also eventually
be included in the Flux OS toolkit. These are long terms goals.

They are studying how to optimize the size of their proofs, that would
be ten times bigger than their binaries (for DEC Alpha) if I understood
correctly.

They are also working on a ML compiler that would have a more expressive
type system than ML. Well they don't speak of OCAML in this 1998 paper,
but they talk about including objects, classes, and subtype in their
TILT compiler (an extension of TIL compiler that was ML like but without
modules).

I hope this summarry will spark some interest for what seems to be a
very interesting project much more linked to Tunes that I would have
believed.

Paul