MILS is a high-assurance security architecture characterized by untrusted and trusted components and based on security models. This chapter describes how to model a RTCS based on security architecture and services to perform security analysis.
MILS uses the divide and conquer approach to reduce the effort for security evaluation of a system.
MILS adopts a classification level for subjects and objects that guides information control.
MILS introduces many concepts that are represented in Cheddar.
A real-time critical system based on MILS security architecture is defined as follows:
package mils_example public with Cheddar_mils; data my_data end my_data; thread a_thread features input : in data port my_data; output : out data port my_data; properties Dispatch_Protocol => Periodic; Compute_Execution_Time => 3 ms .. 3 ms; Period => 20 ms; Priority => 100; Deadline => 20 ms; Cheddar_mils::Mils_component => SLS; Cheddar_mils::Mils_Thread => Application; end a_thread; thread secret_high extends a_thread properties Cheddar_mils::Mils_confidentiality_Level => SECRET; Cheddar_mils::Mils_integrity_Level => HIGH; end secret_high; thread secret_medium extends a_thread properties Cheddar_mils::Mils_confidentiality_Level => SECRET; Cheddar_mils::Mils_integrity_Level => MEDIUM; end secret_medium; thread top_secret_high extends a_thread properties Cheddar_mils::Mils_confidentiality_Level => TOP_SECRET; Cheddar_mils::Mils_integrity_Level => HIGH; end top_secret_high; process my_process end my_process; PROCESSOR cpu PROPERTIES Scheduling_Protocol=>(RMS); END cpu; SYSTEM mils END mils; process implementation my_process.impl subcomponents T1 : thread secret_high; T2 : thread secret_high; T3 : thread secret_high; T4 : thread secret_high; T5 : thread secret_high; T6 : thread secret_high; T13: thread secret_high; T8 : thread secret_medium; T9 : thread secret_medium; T11 : thread secret_medium; T12 : thread secret_medium; T17 : thread secret_medium; T18 : thread secret_medium; T19 : thread secret_medium; T7 : thread top_secret_high; T10 : thread top_secret_high; T14 : thread top_secret_high; T15 : thread top_secret_high; T16 : thread top_secret_high; T20 : thread top_secret_high; connections C1 : port T1.output -> T2.input; C2 : port T1.output -> T3.input; C3 : port T1.output -> T4.input; C4 : port T1.output -> T5.input; C5 : port T1.output -> T6.input; C6 : port T2.output -> T7.input; C7 : port T3.output -> T8.input; C8 : port T4.output -> T8.input; C9 : port T5.output -> T8.input; C10: port T4.output -> T9.input; C11: port T6.output -> T9.input; C12: port T7.output -> T8.input; C13: port T10.output -> T7.input; C14: port T11.output -> T14.input; C15: port T9.output -> T13.input; C16: port T13.output -> T15.input; C17: port T12.output -> T9.input; C18: port T17.output -> T19.input; C19: port T18.output -> T19.input; C20: port T19.output -> T20.input; end my_process.impl; system implementation mils.impl subcomponents process1 : process my_process.impl; my_platform : processor cpu; properties Actual_Processor_Binding => ( reference(my_platform) ) applies to process1; end mils.impl; end mils_example;
property set Cheddar_MILS is MILS_Compliant : aadlboolean applies to (thread, process); MILS_Confidentiality_Level_Type : type enumeration (UnClassified, Classified, Secret, Top_Secret); MILS_Confidentiality_Level : Cheddar_MILS::MILS_Confidentiality_Level_Type applies to (thread, process); MILS_Integrity_Level_Type : type enumeration (Low, Medium, High); MILS_Integrity_Level : Cheddar_MILS::MILS_Integrity_Level_Type applies to (thread, process); MILS_Component_Type : type enumeration (SLS, MSLS, MLS); MILS_Component : Cheddar_MILS::MILS_Component_Type applies to (thread, process); MILS_Partition_Type : type enumeration (Equipment, Application); MILS_Partition : Cheddar_MILS::MILS_Partition_Type applies to (process); MILS_Thread_Type : type enumeration (Application, MMR, Guard, Collator, Downgrader, Upgrader); MILS_Thread : Cheddar_MILS::MILS_Thread_Type applies to (thread); end Cheddar_MILS;process $mils_{-}confidentiality_{-}level$ : It defines the level of confidentiality of an address space. $mils_{-}confidentiality_{-}level$ can be UnClassified, or $Classified$, or $Secret$, or $Top_{-}Secret$ \\ $mils_{-}integrity_{-}level$ : It defines the level of integrity of an address space. $mils_{-}integrity_level$ can be $Low$, or $Medium$, or $High$ \\ $mils_{-}component$ : It defines the type of an address space according to the classification of components in MILS architecture. It can have the $SLS$ value for Single Level Secure component, or $MLS$ for Multi-Level Secure component, or $MSLS$ for Multi Single-Level Secure component.\\ $mils_{-}partition$ : It defines the kind of MILS component modeled by the address space. It can have either the $Device$ value or the $Application$ value.\\ $mils_{-}compliant$ : It is a boolean that specifies if an address space models a component of MILS or not.\\ thread $mils_{-}confidentiality_{-}level$ : It defines the level of confidentiality of a task. $mils_{-}confidentiality_{-}level$ can be $UnClassified$, or $Classified$, or $Secret$, or $Top_{-}Secret$ \\ $mils_{-}integrity_{-}level$ : It defines the level of integrity of a task. $mils_{-}integrity_{-}level$ can be $Low$, or $Medium$, or $High$ \\ $mils_{-}component$ : It defines the type of a task according to the classification of components in mils architecture. It can be SLS for Single Level Secure component, or MLS for Multi-Level Secure component, or MSLS for Multi Single-Level Secure component.\\ $mils_{-}task$ : It defines a task as a common application or a particular element of mils architecture. It can be application, or MMR for MILS Message Router, or Guard, or Collator, or Downgrader, or Upgrader \\ $mils_{-}compliant$ : It is a boolean that specifies if a task models a component of MILS or not. \\
Users should consider the above information in the XML file of a Cheddar-ADL system model.
This section is dedicated to how to perform security analysis based on some security models. A security model describes the security strategy for a system to ensure security objectives. Bell-La Padula, Biba, and chinese wall are examples of security models. They were implemented in Cheddar to verify Cheddar ADL models which are their main point of entry.
In this section we present an example of ARINC 653 scheduling with Cheddar. This example is stored in the file security.xmlv3. It contains tasks with different security levels that lead to some security violations. Some of these violations are already solved by the use of downgraders. The security analysis of this model is shown in the screenshot below. In this screenshot, there are 3 communications that violate integrity and 0 violations of confidentiality. The confidentiality issues have been solved by downgraders in the model.