Secure systems development using security-typed languages
Boniface Hicks · 2007
To protect sensitive, electronic data against corruption and leakage by computer applications, business, military, medical, and other organizations establish high-level security policies. For these to be effective, however, the policies must be implemented in computer systems. This introduces a semantic gap between high-level, security policy semantics and the low-level, operational semantics of computer systems. Bridging this semantic gap by proving that high-level policy semantics are actually implemented in a computer system is a daunting problem. Security-typed languages are a new tool for building applications that verifiably implement information ow policies. By joining these language tools with systems principles, we find that it is possible to bridge the semantic gap in security policy. In particular, we focus on the systems principles of modularity, separation of security policy from mechanism, policy expressiveness and portability. When applying these systems principles to existing security-typed languages, additional policy and runtime infrastructure necessary is needed. In this dissertation, we develop designs and implementations of the runtime and policy infrastructure that is lacking. We also provide systems architectures, formal analyses and software engineering tools, along with multiple applications that use this infrastructure to verifiably implement high-level security policies in systems of applications. We find that, by applying some systems principles with the infrastructure they require, we can use STLs for building secure systems that verifiably enforce high-level security policies.