Using SPARK-Ada to Model and Verify a MILS Message Router
IDAHO UNIV MOSCOW CENTER FOR SECURE AND DEPENDABLE SYSTEMS
Pagination or Media Count:
The concept of information classification is used by all nations to control information distribution and access. In the United States this is referred to as Multiple Levels of Security MLS, which includes designations for unclassified, confidential, secret, and top secret information. The U.S. Department of Defense has traditionally implemented MLS separation via discrete physical devices, but with the transformation of military doctrine to net-centric warfare, the desire to have a single device capable of Multiple Independent Levels of Security MILS emerged. In this paper we present a formal model of a MILS message router using SPARK-ADA. The model is presented as a case study for the design and verification of high assurance computing systems in the presence of an underlying separation kernel. We utilized the correctness-by-design approach to secure system development and discuss the limitations of that approach for the type of system we model.
- Computer Programming and Software
- Computer Systems Management and Standards