Secure Systems Development Using Security-Typed Languages

Open Access
Hicks, Boniface Patrick
Graduate Program:
Computer Science and Engineering
Doctor of Philosophy
Document Type:
Date of Defense:
August 03, 2007
Committee Members:
  • Patrick Drew Mcdaniel, Committee Chair
  • John Joseph Hannan, Committee Member
  • Sencun Zhu, Committee Member
  • Trent Ray Jaeger, Committee Member
  • Stephen George Simpson, Committee Member
  • Michael Johannes Hicks, Committee Member
  • language-based security
  • Jif
  • security-typed language
  • information flow
  • security
  • secure software engineering
<p>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.</p> <p> Security-typed languages are a new tool for building applications that verifiably implement information flow 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. </p> <p> 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. </p>