Security Kernel Verification Techniques: Algorithmic Representation.

摘要

A security kernel is a hardware and software mechanism that enforces access controls to information within a computer system. Given a formal specification for a kernel, this report shows how to construct an algorithmic or programming language representation of the kernel. A technique is suggested for proving that the algorithmic representation exhibits the specified user-visible behavior. A sequence of lower levels of specification, formalizing the levels of abstraction of Dijkstra, is essential to the construction and proof technique. (Author)