Language-Based Security for Extensible Systems

摘要

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 Microsoft's .NET framework.