Trust in Security-Policy Enforcement Mechanisms

摘要

This project investigated language-based approaches for enforcing security policies and proactive approaches for implementing trustworthy distributed services. One avenue of language-based work produced Cyclone, a type-safe variant of C. The Cyclone language retains the familiar syntax and semantics of C code. but provides the strong security guarantees of modern languages such as Java. A second avenue of language-based work explored a general class of policy enforcement mechanism based on in-line reference monitors (IRM), which insert checks and actions in an application to ensure the resulting code will respect the policy when executed. The class of policies enforceable through IRMs was shown not to correspond to any class of the Kleene hierarchy. In addition. a certified IRM rewriter framework was developed for Microsoft NET code. It produces explicit evidence so an independent proof checker can determine that rewritten code respects a desired security policy. Finally, proactive obfuscation was investigated as a basis for achieving independence of server replicas comprising a service. This resulted in new agreement protocols to handle servers that periodically have their storage purged and reloaded (to eliminate undetectably compromised code and data). It also produced a semantic characterization of how obfuscation compares with strong typing, finding that the two are comparable, a surprising result.