Portal de Periódicos da CAPES

Structured specification of a Security Kernel

1975; Association for Computing Machinery; Volume: 10; Issue: 6 Linguagem: Inglês

10.1145/390016.808450

1558-1160

Kenneth G. Walter, Samuel I. Schaen, William F. Ogden, William C. Rounds, D. G. Shumway, D. D. Schaeffer, K. J. Biba, Franklyn T. Bradshaw, Stanley R. Ames, J. M. Gilligan,

Security and Verification in Computing

Certifying an entire operating system to be reliable is too large a task to be practicable. Instead, we are designing a Security Kernel which will provide information security. The kernel's job is to monitor information flow in order to prevent compromise of security. Sound design is encouraged by using a technique called Structured Specification , in which successively more detailed models of the Security Kernel are developed. The initial model, M 0 , is an abstract description which formalizes governmental security applied to computer systems. Subsequent levels of modeling provide increasingly more detail, and gradually the models begin to resemble a particular system (Multics in this case). The second model, M 1 , defines a tree-structured file system, and an interagent communication system while M 2 adds details concerning segmentation in a dynamic environment. It is intended that the final level of modeling will specify the primitive commands for the kernel of a Multics-like system and will enumerate precisely those assertions which must be proved about the implementation in order to establish correctness.