wiki:ArincMilsValidation
close Warning: Can't synchronize with repository "(default)" (Couldn't open Subversion repository /var/repositories/svn/aadl: SubversionException: ("Failed to load module for FS type 'fsfs'", 160033)). Look in the Trac log for more information.

ARINC653 and MILS validation

ARINC653 defines the concept of partitioned kernel. In such systems, software is isolated in terms of space and time. It means that each system has its own address space to store its data and code as well as its own time slice to execute their threads.

On the other hand, MILS (Multiple Independent Level of Security) defines a concept where communication are isolated according to their security requirements. It means that each communication should be a the same security level and prevent communication channels that use different security levels.

On this page, we propose validation and verification patterns to validate ARINC653 and MILS architectures. These validation patterns are performed on AADL model. Our modeling guidelines are detailed on this page.

Note that these validation steps are automatically integrated in the POK toolchain. We you build a system with our POK runtime using AADL models, it automatically check these rules to check your model consistency.

Space isolation, memory segments

In ARINC653 and MILS systems, each partition is isolated in terms of space and time. It means that each process is bound to a memory segment. And there is no overlap between memory segments. So, we can check in AADL models that for each process on each node is bound to a distinct memory component.

To check that, we rely on the REAL language. The associated REAL theorem is:

theorem Isolated_Memories

foreach m in memory_set do

P := {x in Process_Set | is_bound_to (x, m)};

check (Cardinal (P) <= 1);

end Isolated_Memories;

Security Level

In MILS requirements, it is required that all processes that are executing on the same processor have the same security levels. Security levels are provided through virtual bus components and a processor can provide several security levels. So, we check that all security layers provided by a virtual bus share the same security levels so a processor has only one security level.

The associated REAL theorem that proves this requirements is:

theorem One_Security_Level_By_Memory

foreach m in memory_set do

P := {x in Process_Set | is_bound_to (x, m)};

VP := {x in Virtual_Processor_Set | is_bound_to (P, x)};

B := {x in Virtual_Bus_Set | is_provided_class (VP, x)};

check (all_equals (property (B, "POK::Security_Level")));

end One_Security_Level_By_Memory;

Bell-Lapadula

The Bell-Lapadula security policy states that we have no read-up and no write-down. It means that, for each connection in a system, the sender has a fewer security level than the receiver. In other word, SecurityLevel? (Sender) < SecurityLevel? (Receiver).

We check that with the following REAL theorem:

theorem bell_lapadula

foreach p_src in process_set do

VP1 := {x in Virtual_Processor_Set | is_bound_to (p_src, x)};

B_Src := {x in Virtual_Bus_Set | is_provided_class (VP1, x)};

P_Dest := {x in Process_Set | Is_Connected_To (p_src, x)};

VP2 := {x in Virtual_Processor_Set | is_bound_to (P_Dest, x)};

B_Dst := {x in Virtual_Bus_Set | is_provided_class (VP2, x)};

check (Cardinal (P_Dest) = 0 or

(max (property (B_Src, "POK::Security_Level")) <=

min (property (B_Dst, "POK::Security_Level"))));

end bell_lapadula;

Biba

The biba security policy states that for each connection, there is no read-down and no write-up. So, we check that for each process i the AADL model, the security level of the sender is higher than the one of the receiver.

theorem biba

foreach p_src in process_set do

VP1 := {x in Virtual_Processor_Set | is_bound_to (p_src, x)};

B_Src := {x in Virtual_Bus_Set | is_provided_class (VP1, x)};

P_Dest := {x in Process_Set | Is_Connected_To (p_src, x)};

VP2 := {x in Virtual_Processor_Set | is_bound_to (P_Dest, x)};

B_Dst := {x in Virtual_Bus_Set | is_provided_class (VP2, x)};

check (Cardinal (P_Dest) = 0 or

(min (property (B_Src, "POK::Security_Level")) >=

max (property (B_Dst, "POK::Security_Level"))));

end biba;

Connections correctness regarding MILS requirements

MILS stands for Multiple Independent Level of Security. So, if a MILS architecture connects processes that have distinct adress space, we must ensure that their security levels are equals. We do that with the following REAL theorem:

theorem MILS_1

foreach p_src in process_set do

VP1 := {x in Virtual_Processor_Set | is_bound_to (p_src, x)};

B_Src := {x in Virtual_Bus_Set | is_provided_class (VP1, x)};

P_Dest := {x in Process_Set | Is_Connected_To (p_src, x)};

VP2 := {x in Virtual_Processor_Set | is_bound_to (P_Dest, x)};

B_Dst := {x in Virtual_Bus_Set | is_provided_class (VP2, x)};

check (Cardinal (P_Dest) = 0 or

((max (property (B_Src, "POK::Security_Level")) =

max (property (B_Dst, "POK::Security_Level"))) and

(min (property (B_Src, "POK::Security_Level")) =

min (property (B_Dst, "POK::Security_Level")))));

end MILS_1;

Moreover, we can make another verification. In fact, the connection should be bound to a bus. So, if we have a connection between two processes, we must ensure that the security levels of the processes are the same. But we must also ensure that the security level of the bus equal to the security level of the partitions. The following REAL theorem demonstrate that:

theorem MILS_2

foreach p_src in process_set do

VP1 := {x in Virtual_Processor_Set | is_bound_to (p_src, x)};

B_Src := {x in Virtual_Bus_Set | is_provided_class (VP1, x)};

Cnx := {x in Connection_Set | is_accessing_to (p_src, x)};

P_Dest := {x in Process_Set | is_accessing_to (x, Cnx)};

VP2 := {x in Virtual_Processor_Set | is_bound_to (P_Dest, x)};

B_Dst := {x in Virtual_Bus_Set | is_provided_class (VP2, x)};

B_Cnx := {x in Virtual_Bus_Set | is_bound_to (Cnx, x)};

check (Cardinal (Cnx) = 0 or

((max (property (B_Src, "POK::Security_Level")) =

max (property (B_Dst, "POK::Security_Level"))) and

(min (property (B_Src, "POK::Security_Level")) =

min (property (B_Dst, "POK::Security_Level")))) and

((min (property (B_Dst, "POK::Security_Level")) =

min (property (B_Cnx, "POK::Security_Level"))) and

(max (property (B_Dst, "POK::Security_Level")) =

max (property (B_Cnx, "POK::Security_Level")))));

end MILS_2;

Last modified 8 years ago Last modified on 05/26/09 22:29:19