Efficient Code Certification

ECC is a simple and efficient approach to the certification of compiled code downloaded from an untrusted source. It can ensure a basic but nontrivial level of code safety, including control flow safety, memory safety, and stack safety in a way that is simple, efficient, and (most importantly) relatively painless to incorporate into existing compilers. Although less expressive than the proof carrying code of Necula and Lee or typed assembly language of Morrisett et al., ECC certificates are by comparison relatively compact and easy to produce and to verify. Unlike JAVA byte code, ECC operates at the level of native code; it is not interpreted and no further compilation is necessary.

The ECC prototype consists of a Scheme to x86 certifying compiler and verifier. It is highly experimental and still under construction. A relatively stable preliminary version for Windows is available for downloading.

More Info

Dexter Kozen, "Efficient Code Certification," Tech. Report 98-1661, Cornell Univ., January 1998.
Dexter Kozen, "Language-Based Security," In M. Kutylowski, L. Pacholski, and T. Wierzbicki, editors, Proc. Conf. Mathematical Foundations of Computer Science (MFCS'99), Lecture Notes in Computer Science v. 1672, Springer-Verlag, September 1999, 284-298.

Software

Personnel

The following students have contributed to this project:

Jason Hartlinex86 emulator
Jim Ezickruntime support for native execution
Gaurav Agarwalx86 parser
Carson Bloomberg   compiler enhancements

Related Projects at Cornell

TAL
Security Automata
PolyJ
Inline Reference Monitors
Information Assurance Institute

Acknowledgment

This work is supported by the National Science Foundation under research grant CCR-9708915.

Send email to Dexter
Dexter's home page
Copyright (c) 2000 Cornell University
Last updated: 18 December 2000