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

appel， AndrewPrinceton大学端到端接口安全的源到对象验证本研究的目的是加强由组件构建的软件的内部保护屏障，并在软件虚拟机（如Sun的Java和Microsoft的。net）中运行。在这样的软件中，程序员可以使用抽象、面向对象和信息隐藏等标准技术来设计组件之间的接口，以限制恶意组件可能造成的损害。流氓组件是那些被恶意设计的组件，或者更常见的是那些有漏洞的组件，使它们容易受到攻击和接管。但是，Java和。Net（限制一个组件访问属于另一个组件的数据的类型系统）本身很容易受到攻击，如果实现它们的类型检查器和编译器有错误。为了确保没有编译器错误会导致安全漏洞，研究人员将开发正式的模型，将源语言的类型系统（程序员在其中推断它们以设计其保护接口）与实际执行的机器语言联系起来。研究人员将构建机器可检查的规范，并设计方法来构建具有机器可检查安全性证明的编译器。

ABSTRACT0540914Appel, AndrewPrinceton UniversityEnd-to-End Souce-to-Object Verification of Interface SafetyThe 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.