Lambda the Ultimate

inactiveTopic Automated Techniques for Provably Safe Mobile Code
started 1/3/2003; 1:19:30 PM - last post 1/3/2003; 1:19:30 PM
Ehud Lamm - Automated Techniques for Provably Safe Mobile Code  blueArrow
1/3/2003; 1:19:30 PM (reads: 1230, responses: 0)
Automated Techniques for Provably Safe Mobile Code
Christopher Colby, Karl Crary, Robert Harper, Peter Lee, and Frank Pfenning. Automated Techniques for Provably Safe Mobile Code. Theoretical Computer Science special issue on Dependable Computing. 2003.

We present a general framework for provably safe mobile code. It relies on a formal definition of a safety policy and explicit evidence for compliance with this policy which is attached to a binary. Concrete realizations of this framework are proof-carrying code (PCC), where the evidence for safety is a formal proof generated by a certifying compiler, and typed assembly language (TAL), where the evidence for safety is given via type annotations propagated throughout the compilation process in typed intermediate languages. Validity of the evidence is established via a small trusted type checker, either directly on the binary or indirectly on proof representations in a logical framework (LF).

Related to several topics mentioned here recently (auditors, Cecil etc.). The paper gives a nice survey of the issues and techniques involved.

The line of research presented in this paper gives yet another reason why types should be propagated from the source program via the compiler right into the object code. It is interesting to note that this is related to one approach for implementing generic code (e.g., using VM support).

Some LtU readers may enjoy noting that in some sense this brings us back to the classic implementation of dynamic typing (e.g., types being a property of values not variables). But I think this analogy goes only so far.


Posted to general by Ehud Lamm on 1/3/03; 1:30:47 PM