The HASK Lab at MU
Our group explores the nexus between programming languages, computer security and formal methods.
Language Based Methods in Computer Security
Our research combines ideas from languages research in novel ways to construct high-assurance secure systems. Structures and techniques from programming language research provide
- a mathematical basis for formal verification,
- a flexible, modular organizing principle for system design and implementation, and
- tools for generating efficient, correct implementations from high-level specifications.
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.
Separation Kernels
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.