Machine-Checked Metatheory for Security-Oriented Languages
Abstract
Security-oriented languages are a key ingredient to the design of secure software systems. The provide specific functionality, such as mechanisms for authorization, auditing, confidentiality, and the tracking of information-flow throughout the system. Programs written in these languages that take advantage of these features, can be automatically shown to possesses key properties, essential to the security of the entire system. However, these results critically rely on the metatheoretic properties of the languages themselves. This project has demonstrated both that it is feasible to mechanically check these properties, and that the overheads of the engineering process of producing mechanically verified languages are reasonable.
Document Details
- Document Type
- Technical Report
- Publication Date
- Aug 23, 2006
- Accession Number
- ADA536269
Entities
People
- Stephanie Weirich
- Steve Zdancewic
Organizations
- University of Pennsylvania