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.
1. MILS (Multi Independent Levels of security) architecture
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:
- At least a processor and a core.
- Cheddar address spaces that represent MILS partitions.
- Cheddar tasks that represent MILS processes. Each task has to be assigned to an address space
- Cheddar shared resources such as messages and buffers that represent MILS Objects.
- For each task, object, and address space, there attributes that define their degree of sensitivity.
The Confidentiality_Level attribute can be Unclassified, or Classified, or Secret, or Top_Secret.
The Integrity_Level attribute can be Low, or Medium, or High.
- Each task and address space is characterized by the attribute MILS_component_type that specifies classification
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.
- Cheddar dependencies that represent MILS communications. MILS messages can be modeled by asynchronous communication
Cheddar dependencies.
- In MILS architecture, information flow control is performed through trustworthy components such as access control guard,
MILS Message Router (MMR), downgrader, collator, etc.... These components are represented by tasks in Cheddar.
Each task is characterized by an attribute MILS_Task_Type that specifies whether a task is a regular application or
a security monitor. It can be Application, MMR, Guard, Collator, Downgrader,
or Upgrader.
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;
MILS properties
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.
2. Security services
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.
- Bell-La Padula concerns confidentiality, which is the assurance of preventing the system from disclosing information.
It is based on the principle "No read up/No write-down". The implemented method "bell_lapadula (Sys: System )" checks
if the Cheddar ADL model "Sys" complies with the Bell-La Padula rules by returning the number of violations of
the "No read up/No write-down" rule.
- Biba concerns data integrity, meaning the protection of the system against unauthorized modifications.
It is based on the principle "No read down, no write up". The implemented method "biba (Sys: System)" checks
if the Cheddar ADL model "Sys" conforms to Biba rules by returning how many times the Read down and Write up rules are missed.
- Chinese wall model addresses conflicts of interest. The implemented method "chinese_wall
(Sys : System; COIs : array_tasks_set; M: in out matrice)" returns for the Cheddar ADL model "Sys",
the number of information flows that cause conflict of interest, based on the defined conflict of interest classes "COIs".
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.
décrire au moins 1 exercice (voire 2)