Programming languages research has many techniques for generating efficient, correct implementations from high-level specifications. Recent research on language-based security formulates models of information security in terms of modular, algebraic structures from language semantics. This research combines these threads in novel ways to construct high-assurance secure systems in which techniques from programming language semantics provide both a mathematical basis for formal verification and a flexible, modular organizing principle for system design and implementation. This methodology is illustrated with a case study in which kernels (in particular, separation kernels) with a verified security policy are synthesized directly from formal models of security.
There is growing interest within defense and avionics circles in separation kernels as a means of coping with serious concerns for system security, safety and integrity arising from the use of high levels of integration. Multi-level security (MLS) systems can be implemented by physical separation: computations at different security levels are situated on different network nodes. However, for many defense and avionics scenarios, physical separation is infeasible due to tight resource constraints. Because sharing resources introduces potential vulnerabilities, mission- or safety-critical MLS systems require both highly integrated implementations and high-assurance security guarantees. This research will have a direct impact on how separation kernels are designed, implemented and verified. Can the rigorous techniques for constructing modular and robust secure systems be generalized to other systems? The long range goal is to facilitate the construction of systems with high assurance end-to-end guarantees, thereby making high assurance more widely available.
