Scaling Proof-Carrying Code to Production Compilers and Security Policies
Abstract
We have developed high-assurance software protection mechanisms that can be used in component-software platforms (virtual machines such as Sun's Java or Microsoft's .Net). The idea is to leverage type-safe source languages to get fine-grained protection at the level of individual object fields and methods. The obstacle to be overcome was the inherent complexity of virtual machine implementations, particularly their just-in-time compiler, before installing that output for execution. We have successfully shown how to integrate this technology into the compiler, and how to conduct formal, automated verification of the protection mechanism. We have also developed a technology for distributed authentication and public key distribution, called "proof-carrying authentication." This allows many participants with different goals, different policies, and even different policy languages, to cooperate in authenticating each other (and third parties). Finally, we have started a seedling effort in policy-based network management.
Document Details
- Document Type
- Technical Report
- Publication Date
- Apr 01, 2005
- Accession Number
- ADA434335
Entities
People
- Andrew Appel
- David P. Walker
- Edward W. Felton
- Valery Trifonov
- Zhong Shao
Organizations
- Princeton University