End-to-end source-to-object verification of interface safety

Princeton University, Princeton NJ

Investigators

Abstract

ABSTRACT 0540914 Appel, Andrew Princeton University End-to-End Souce-to-Object Verification of Interface Safety The purpose of this research is to strengthen the internal protection barriers in software built from components and run in software virtual machines such as Sun's Java and Microsoft's .Net. In such software, programmers can design the interfaces between components--using standard techniques such as abstraction, object orientation, and information hiding--to limit the damage that rogue components can do. Rogue components are those that are designed maliciously or, more commonly, that have bugs making them vulnerable to attack and take-over. However, the protection barriers in Java and .Net (type systems that limit access by one component to data belonging to another component) are themselves vulnerable to attack if the type-checkers and compilers that implement them have bugs. In order to ensure that no compiler bugs can cause security vulnerabilies, the researchers will develop formal models to relate type systems at the source language--where programmers reason about them to design their protection interfaces--to the machine language that actually executes. The researchers will construct machine-checkable specifications and design ways to construct compilers with machine-checkable proofs of security.