------------------------------------------------------------------------------ ------------------------------------------------------------------------------ -- Cheddar is a GNU GPL real-time scheduling analysis tool. -- This program provides services to automatically check schedulability and -- other performance criteria of real-time architecture models. -- -- Copyright (C) 2002-2020, Frank Singhoff, Alain Plantec, Jerome Legrand, -- Hai Nam Tran, Stephane Rubini -- -- The Cheddar project was started in 2002 by -- Frank Singhoff, Lab-STICC UMR 6285, Université de Bretagne Occidentale -- -- Cheddar has been published in the "Agence de Protection des Programmes/France" in 2008. -- Since 2008, Ellidiss technologies also contributes to the development of -- Cheddar and provides industrial support. -- -- The full list of contributors and sponsors can be found in AUTHORS.txt and SPONSORS.txt -- -- This program is free software; you can redistribute it and/or modify -- it under the terms of the GNU General Public License as published by -- the Free Software Foundation; either version 2 of the License, or -- (at your option) any later version. -- -- This program is distributed in the hope that it will be useful, -- but WITHOUT ANY WARRANTY; without even the implied warranty of -- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the -- GNU General Public License for more details. -- -- You should have received a copy of the GNU General Public License -- along with this program; if not, write to the Free Software -- Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA -- -- -- Contact : cheddar@listes.univ-brest.fr -- ------------------------------------------------------------------------------ -- Last update : -- $Rev$ -- $Date$ -- $Author: singhoff $ ------------------------------------------------------------------------------ ------------------------------------------------------------------------------ with Ada.Text_IO; use Ada.Text_IO; with Systems; use Systems; with Dependencies; use Dependencies; with Task_Dependencies; use Task_Dependencies; with Task_Dependencies; use Task_Dependencies.Half_Dep_Set; with Tasks; use Tasks; with Task_Set; use Task_Set; with Message_Set ; use Message_Set; with Messages; use Messages; with MILS_Security; use MILS_Security; with Ada.Strings.Unbounded; use Ada.Strings.Unbounded; with Debug; use Debug; with sets; package body mils_analysis is -- num_tasks: Tasks_Range:=0; function bell_lapadula (Sys : System ) return Tasks_Dependencies_Ptr is My_iterator: Tasks_Dependencies_Iterator; Dep_Ptr: Dependency_Ptr; My_dependencies: Tasks_Dependencies_Ptr; Risky_dependencies: Tasks_Dependencies_Ptr; begin Risky_dependencies:= new Tasks_Dependencies; My_dependencies:= Sys.Dependencies; if is_empty( My_dependencies.Depends) then -- return 0; Put_Line("NO dependencies"); return Risky_dependencies; else reset_iterator(My_dependencies.Depends, My_iterator); loop current_element(My_dependencies.Depends, Dep_Ptr, My_iterator); if (Dep_Ptr.type_of_dependency=asynchronous_communication_dependency)then if ((Dep_Ptr.asynchronous_communication_dependent_task.mils_task/=Downgrader) AND (Dep_Ptr.asynchronous_communication_dependent_task.mils_task/=Upgrader)) then if((Dep_Ptr.asynchronous_communication_dependent_task.MILS_Confidentiality_Level < Dep_Ptr.asynchronous_communication_dependency_object.MILS_Confidentiality_Level) AND ((Dep_Ptr.asynchronous_communication_orientation= From_Object_To_Task) OR (Dep_Ptr.asynchronous_communication_orientation= From_Object_To_Task))) then Add_One_Task_Dependency_asynchronous_communication(My_Dependencies => Risky_dependencies, A_Task => Dep_Ptr.asynchronous_communication_dependent_task, A_Dep => Dep_Ptr.asynchronous_communication_dependency_object, A_Type => Dep_Ptr.asynchronous_communication_orientation, protocol_property => First_Message) ; elsif ((Dep_Ptr.asynchronous_communication_dependency_object.MILS_Confidentiality_Level < Dep_Ptr.asynchronous_communication_dependent_task.MILS_Confidentiality_Level) AND (Dep_Ptr.asynchronous_communication_orientation= From_Task_To_Object)) Then Add_One_Task_Dependency_asynchronous_communication(My_Dependencies => Risky_dependencies, A_Task => Dep_Ptr.asynchronous_communication_dependent_task, A_Dep => Dep_Ptr.asynchronous_communication_dependency_object, A_Type => Dep_Ptr.asynchronous_communication_orientation, protocol_property => First_Message) ; end if; end if; elsif(Dep_Ptr.type_of_dependency=precedence_dependency)then if (Dep_Ptr.precedence_sink.mils_confidentiality_level Risky_dependencies, Source =>Dep_Ptr.precedence_source, Sink => Dep_Ptr.precedence_sink); end if; end if; end if; exit when is_last_element (My_Dependencies.Depends, My_Iterator); next_element (My_Dependencies.Depends, My_Iterator); end loop; return Risky_dependencies; end if; end bell_lapadula; function bell_lapadula (Sys : System ) return Integer is My_dependencies: Tasks_Dependencies_Ptr; begin My_dependencies:=bell_lapadula (Sys); if is_empty( My_dependencies.Depends) then return 0; else return Integer(get_number_of_elements(My_dependencies.Depends)); end if; end bell_lapadula; function bell_lapadula (Sys : System ) return Boolean is nb_violations:Integer:=bell_lapadula(Sys); Begin Put_Debug("Number of bell_lapadula rules violations :" & nb_violations'Img); if (nb_violations=0) then return True; else return False; end if; end bell_lapadula; function biba (Sys : System ) return Tasks_Dependencies_Ptr is My_iterator: Tasks_Dependencies_Iterator; Dep_Ptr: Dependency_Ptr; My_dependencies: Tasks_Dependencies_Ptr; Risky_dependencies: Tasks_Dependencies_Ptr; begin Risky_dependencies:= new Tasks_Dependencies; My_dependencies:= Sys.Dependencies; if is_empty( My_dependencies.Depends) then -- return 0; Put_Line("NO dependencies"); return Risky_dependencies; else reset_iterator(My_dependencies.Depends, My_iterator); loop current_element(My_dependencies.Depends, Dep_Ptr, My_iterator); if (Dep_Ptr.type_of_dependency=asynchronous_communication_dependency)then if ((Dep_Ptr.asynchronous_communication_dependent_task.mils_task/=Downgrader) AND (Dep_Ptr.asynchronous_communication_dependent_task.mils_task/=Upgrader)) then if ((Dep_Ptr.asynchronous_communication_dependency_object.mils_integrity_level < Dep_Ptr.asynchronous_communication_dependent_task.mils_integrity_level) AND (Dep_Ptr.asynchronous_communication_orientation= From_Object_To_Task)) Then Add_One_Task_Dependency_asynchronous_communication(My_Dependencies => Risky_dependencies, A_Task => Dep_Ptr.asynchronous_communication_dependent_task, A_Dep => Dep_Ptr.asynchronous_communication_dependency_object, A_Type => Dep_Ptr.asynchronous_communication_orientation, protocol_property => First_Message) ; elsif((Dep_Ptr.asynchronous_communication_dependent_task.mils_integrity_level < Dep_Ptr.asynchronous_communication_dependency_object.mils_integrity_level) AND (Dep_Ptr.asynchronous_communication_orientation= From_Task_To_Object)) then Add_One_Task_Dependency_asynchronous_communication(My_Dependencies => Risky_dependencies, A_Task => Dep_Ptr.asynchronous_communication_dependent_task, A_Dep => Dep_Ptr.asynchronous_communication_dependency_object, A_Type => Dep_Ptr.asynchronous_communication_orientation, protocol_property => First_Message) ; end if; end if; elsif (Dep_Ptr.type_of_dependency=remote_procedure_call_dependency)then if ((Dep_Ptr.remote_procedure_call_server.mils_task/=Downgrader) AND (Dep_Ptr.remote_procedure_call_server.mils_task/=Upgrader)AND (Dep_Ptr.remote_procedure_call_client.mils_task/=Downgrader)AND (Dep_Ptr.remote_procedure_call_client.mils_task/=Upgrader)) then if(Dep_Ptr.remote_procedure_call_server.mils_integrity_level < Dep_Ptr.remote_procedure_call_client.mils_integrity_level) then Add_One_Task_Dependency_remote_procedure_call(My_Dependencies => Risky_dependencies, client => Dep_Ptr.remote_procedure_call_client, server => Dep_Ptr.remote_procedure_call_server); end if; end if; elsif(Dep_Ptr.type_of_dependency=precedence_dependency)then if (Dep_Ptr.precedence_source.mils_integrity_level Risky_dependencies, Source =>Dep_Ptr.precedence_source, Sink => Dep_Ptr.precedence_sink); end if; end if; end if; exit when is_last_element (My_Dependencies.Depends, My_Iterator); next_element (My_Dependencies.Depends, My_Iterator); end loop; return Risky_dependencies ; end if; end biba; function biba (Sys : System) return Integer is My_dependencies: Tasks_Dependencies_Ptr; begin My_dependencies:=biba (Sys); if is_empty( My_dependencies.Depends) then return 0; else return Integer(get_number_of_elements(My_dependencies.Depends)); end if; end biba; function biba (Sys : System) return boolean is nb_violations:Integer:= biba(Sys); begin Put_Debug("Number of Biba rules violations :" & nb_violations'Img); if(nb_violations=0) then return True; else return False; end if; end biba; procedure Warshall(Sys: System; M: in out matrice) is My_iterator: Tasks_Dependencies_Iterator; My_iterator1: Tasks_Dependencies_Iterator; Dep_Ptr: Dependency_Ptr; Dep_Ptr1: Dependency_Ptr; My_dependencies: Tasks_Dependencies_Ptr; My_dependencies2: Tasks_Dependencies_Ptr; num_tasks: Tasks_Range:=0; begin for i in 1..Max_Tasks loop for j in 1.. Max_Tasks loop M(i,j):=0; end loop; end loop; num_tasks:= Get_Number_Of_Task_From_Processor(My_tasks => Sys.Tasks, Processor_Name => To_Unbounded_String("Processor")); My_dependencies := Sys.Dependencies; reset_iterator(My_dependencies.Depends, My_iterator); loop current_element(My_dependencies.Depends, Dep_Ptr, My_iterator); if (Dep_Ptr.type_of_dependency=asynchronous_communication_dependency)then if (Dep_Ptr.asynchronous_communication_orientation= From_Task_To_Object)then My_dependencies2 :=Sys.Dependencies; reset_iterator(My_dependencies2.Depends, My_iterator1); loop current_element(My_dependencies2.Depends, Dep_Ptr1, My_iterator1); if (Dep_Ptr1.type_of_dependency=asynchronous_communication_dependency)then if(( Dep_Ptr.asynchronous_communication_dependency_object.name=Dep_Ptr1.asynchronous_communication_dependency_object.name) AND (Dep_Ptr1.asynchronous_communication_orientation= From_Object_To_Task)) then M(Integer'Value(To_String(Dep_Ptr.asynchronous_communication_dependent_task.name)),Integer'Value(To_String(Dep_Ptr1.asynchronous_communication_dependent_task.name))):=1; end if; end if; exit when is_last_element (My_dependencies2.Depends, My_Iterator1); next_element (My_dependencies2.Depends, My_Iterator1); end loop; end if; elsif (Dep_Ptr.type_of_dependency=remote_procedure_call_dependency)then M(Integer'Value(To_String(Dep_Ptr.remote_procedure_call_server.name)),Integer'Value(To_String(Dep_Ptr.remote_procedure_call_client.name))):=1; elsif(Dep_Ptr.type_of_dependency=precedence_dependency)then M(Integer'Value(To_String(Dep_Ptr.precedence_source.name)),Integer'Value(To_String(Dep_Ptr.precedence_sink.name))):=1; elsif(Dep_Ptr.type_of_dependency=queueing_buffer_dependency)then if (Dep_Ptr.buffer_orientation= From_Task_To_Object)then My_dependencies2 :=Sys.Dependencies; reset_iterator(My_dependencies2.Depends, My_iterator1); loop current_element(My_dependencies2.Depends, Dep_Ptr1, My_iterator1); if (Dep_Ptr1.type_of_dependency=queueing_buffer_dependency)then if(( Dep_Ptr.buffer_dependency_object.name=Dep_Ptr1.buffer_dependency_object.name) AND (Dep_Ptr1.buffer_orientation= From_Object_To_Task)) Then M(Integer'Value(To_String(Dep_Ptr.buffer_dependent_task.name)),Integer'Value(To_String(Dep_Ptr1.buffer_dependent_task.name))):=1; end if; end if; exit when is_last_element (My_dependencies2.Depends, My_Iterator1); next_element (My_dependencies2.Depends, My_Iterator1); end loop; end if; end if; exit when is_last_element (My_Dependencies.Depends, My_Iterator); next_element (My_Dependencies.Depends, My_Iterator); end loop; for a in 1..Natural(num_tasks) loop for i in 1..Natural(num_tasks) loop for j in 1..Natural(num_tasks) loop for k in 1..Natural(num_tasks) loop if (M(i,k)*M(k,j)=1) then M(i, j):=1; end if; end loop; end loop; end loop; end loop; end Warshall; function chinese_wall (Sys : System; COIs : array_tasks_set;M: in out matrice) return Integer is My_COI_tasks: Tasks_Set; Tasks_Ptr: Generic_Task_Ptr; Tasks_Ptr1: Generic_Task_Ptr; My_iterator:Tasks_Iterator; My_iterator1:Tasks_Iterator; num_tasks: Tasks_Range:=0; nb_violations:Integer:=0; begin Warshall(Sys,M); num_tasks:= Get_Number_Of_Task_From_Processor(My_tasks => Sys.Tasks, Processor_Name => To_Unbounded_String("Processor")); Put_Line("Tasks_Number "&num_tasks'img); for i in 1..Natural(num_tasks) loop for j in 1..Natural(num_tasks) loop Put_Line(" "&M(i,j)'img); end loop; end loop; for i in COIs'Range loop My_COI_tasks:=COIs(i); reset_iterator (COIs(i), My_Iterator); loop current_element(COIs(i),Tasks_Ptr,My_iterator); reset_iterator (My_COI_tasks, My_Iterator1); loop current_element(My_COI_tasks,Tasks_Ptr1,My_iterator1); if ((Tasks_Ptr.name/=Tasks_Ptr1.name)AND ( M(Integer'Value(To_String(Tasks_Ptr.name)), Integer'Value(To_String(Tasks_Ptr1.name)))=1)) Then nb_violations:=nb_violations+1; end if; exit when is_last_element (My_COI_tasks, My_Iterator1); next_element (My_COI_tasks, My_Iterator1); end loop; exit when is_last_element (COIs(i), My_Iterator); next_element (COIs(i), My_Iterator); end loop; end loop; return nb_violations; end chinese_wall; function chinese_wall (Sys : System; COIs : array_tasks_set) return boolean is i:Integer:=0; M: matrice; begin i:= chinese_wall(Sys,COIs,M); Put_Debug("Number of chinese_wall violations:" & i'Img); if(i=0) then return True; else return False; end if; end chinese_wall; end mils_analysis;