Using SPARK-Ada to Model and Verify a MILS Message Router
Bryan Rossebo, Paul Oman, Jim Alves-Foss, Ryan Blue, Paul Jaszkowiak · 2006
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. 1. The need for certifiably secure systems* One of the largest problems facing the field of computer science is that of computer and network security. With the increased connectivity of Information Technology (IT) systems and process control systems, security is needed to defend against malicious persons intent on abusing or attacking network resources. This is especially true for unbounded networks like the Global Information Grid (GIG) [1]. Every year, billions of dollars are lost due to cyber intrusions and computer viruses that threaten corporate and government systems. The "ILOVEYOU " virus alone