Welcome to the HASK LAB

Systems software is notoriously difficult to reason about-either formally or informally-and this, in turn, greatly complicates the construction of high assurance systems. This difficulty stems from the conceptual "distance" between abstract models of systems and their concrete implementations. System models are formulated in terms of high-level abstractions while system implementations reflect the low-level and concrete details of hardware, machine languages and C. Typically, there is no apparent relationship between the system model and implementation to exploit in verifying critical system properties, and this disconnect discourages the construction of computer systems with verified security policies. The High Assurance Security Kernel (HASK) Laboratory at the University of Missouri is exploring a novel approach to bridging this conceptual gap by synthesizing implementations of system software from formal models of secure systems in a manner verified to preserve the system security property.