Machine-Checked Metatheory for Security-Oriented Languages

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.