|
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
|
Automated Techniques for Provably Safe Mobile Code
