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.
The following students have contributed to this project:
 | Jason Hartline | x86 emulator |
| Jim Ezick | runtime support for native execution |
| Gaurav Agarwal | x86 parser |
| Carson Bloomberg | compiler enhancements |
| TAL |
| Security Automata |
| PolyJ |
| Inline Reference Monitors |
| Information Assurance Institute |
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