Please choose your delivery country and your customer group
This paper describes the VIKING (Verified Implementation of a Kernel IN Gypsy) research and development project in security kernels for communications applications. The paper will start out by describing the goals of our project. Past work on security kernels will then be briefly outlined. The results of an initial study are presented, which explain our basic method for meeting the project goals. Our security requirements for the VIKING kernel are described, along with the formal model of those requirements. Next, some preliminary design issues are addressed. Our formal verification approach is then discussed, and finally, the current status of the project is given. The author assumes the reader has a general knowledge of the Trusted Computer System Evaluation Criteria, and a basic understanding of formal verification and computer security.