Security Kernel Verification
(I was sorting my document archive and thought some of you might find this interesting)
Attached is a zipped PDF document from the good people at Honeywell Systems & Research Center.
Quote:
The importance of this work is the experience that it reports on with using formal methods on a complete, sophisticated system that is being marketed and used for real-world applications. The statements we make about the effectiveness of the languages, techniques, and tools are not limited to verification of the multilevel security property, but are applicable to programming system properties in general. This evaluation is of interest, because we approached the specification and verification tasks as users of available tools, not as verification researchers.
Please keep in mind the point about these being real world systems. Some time back in the late 80's when the PC market began to explode the IT sector, security in particular was flooded with new users and older ideas of security were beyond most of their reach, so computer security was essentially reinvented anew. But not really anew, as in from some place else, but from ~15 years earlier. This coupled with the fact that systems needed to be easy to use (would PCs have taken off if users got lots of "access denied" warnings?) and cheap to develop, so cheap in fact that the two primary systems today comprise of a largely stole/purchased/borrowed compilation and a college student's caffeine induced project because he couldn't afford good enough hardware to run the system he had on hand.
The consequences of these forgotten lessons is still largely evident, anyhow, back to the document.
Concepts of security kernels, the importance of focusing on specification and verification, the principals of multi level security policies, and covert channels are all introduced at the layman level.
At a more advanced level policy exceptions, the differences between flow and policy violations, design specifications, and formal verification itself are discussed.
The system in question is the Kernelized Secure Operating System (KSOS6) and supplemental material regarding the specifics of KSOS6's proof of security verification are provided and structured by module/gate for intermediate level comprehension. It should be noted that both KSOS6 and KSOS11 have since been developed both direction and inspirationally into other systems including but not limited to STOP, LOCK, SMG, AITOS, and Gemini. These systems can be found extensively in both government and commercial applications where not only security but the highest level availability is required. Like the security, this level of availability is afforded by the assurances these systems feature.
Anyhow, enjoy the read.
catch
