Language-Based Security for Extensible Systems
Final rept. Mar 2000-Nov 2003
CORNELL UNIV ITHACA NY
Pagination or Media Count:
Successful attacks on computing infrastructures often involve failures of type safety. A major contribution of this grant has been the creation of type systems and type-checking algorithms for low-level languages in use today. In addition, certifying compilation was developed to eliminate the need to trust correctness of highlevel language implementations. However, ensuring type safety is not sufficient for ruling-out misbehavior in code. A second contribution of this grant was to design and build program-rewriting tools employed for security policy enforcement and also to derive a theoretical characterization for what kinds of policies can be enforced by program rewriting. The theoretical work compares the expressive power of rewriting against traditional security enforcement mechanisms rewriting is proved to be strictly more powerful. The in-lined reference monitor toolkits handle x86 machine code, the Java virtual machine, and Microsofts .NET framework.
- Computer Programming and Software
- Computer Systems Management and Standards