added briefcase files

Cyber-Resilient-UAV/CASE_Model_Transformations.aadl

@@ -0,0 +1,318 @@
+package CASE_Model_Transformations
+public
+
+	with Base_Types;
+	with CASE_Properties;
+
+	-- COMMUNICATIONS
+
+	-- CASE message header
+	data CASE_MsgHeader
+	end CASE_MsgHeader;
+	data implementation CASE_MsgHeader.Impl
+		subcomponents
+			src: data Base_Types::Integer_32;
+			dst: data Base_Types::Integer_32;
+			trusted: data Base_Types::Boolean;
+			HMAC: data Base_Types::Boolean;
+	end CASE_MsgHeader.Impl;
+
+	-- CASE RF Message structure
+	data CASE_RF_Msg
+	end CASE_RF_Msg;
+
+	data implementation CASE_RF_Msg.Impl
+		subcomponents
+			header: data CASE_MsgHeader.Impl;
+			payload: data;
+	end CASE_RF_Msg.Impl;
+
+	-- UART Message structure
+	data CASE_UART_Msg
+	end CASE_UART_Msg;
+
+	data implementation CASE_UART_Msg.Impl
+		subcomponents
+			crc: data Base_Types::Boolean;
+--			message: data Base_Types::String;
+	end CASE_UART_Msg.Impl;
+
+	-- WIFI Message structure
+	data CASE_WIFI_Msg
+	end CASE_WIFI_Msg;
+
+	data implementation CASE_WIFI_Msg.Impl
+		subcomponents
+			crc: data Base_Types::Boolean;
+--			message: data Base_Types::String;
+	end CASE_WIFI_Msg.Impl;
+
+	-- ATTESTATION MANAGER
+
+	-- This is the structure of an Attestation Request message
+	-- that the Attestation Manager sends to the comm driver
+	data CASE_AttestationRequestMsg
+	end CASE_AttestationRequestMsg;
+
+	data implementation CASE_AttestationRequestMsg.Impl
+		subcomponents
+			header: data CASE_MsgHeader.Impl;
+	end CASE_AttestationRequestMsg.Impl;
+
+	-- This is the structure of an Attestation Response message
+	-- that the comm driver returns to the Attestation Manager
+	-- when it gets a response from the Ground Station
+	data CASE_AttestationResponseMsg
+	end CASE_AttestationResponseMsg;
+
+	data implementation CASE_AttestationResponseMsg.Impl
+		subcomponents
+			header: data CASE_MsgHeader.Impl;
+			status: data Base_Types::Boolean;
+	end CASE_AttestationResponseMsg.Impl;
+
+
+
+	annex Resolute {**
+
+		---------------------------
+		-- MODEL TRANSFORMATIONS --
+		---------------------------
+
+		-- Strategy for proper insertion of a filter
+		strategy add_filter(comp_context : string, filter : string, conn : string, msg_type : data) <=
+			** "Filter " filter " is properly added to component " comp_context **
+			let ctx : component = ModelAccess.getComponent(comp_context);
+			let flt : component = ModelAccess.getComponent(filter);
+			let cnx : connection = ModelAccess.getConnection(conn);
+			filter_exists(flt, ctx, cnx) and component_not_bypassed(flt, ctx, msg_type) and component_implemented(flt, "SPLAT")
+
+		-- Strategy for proper insertion of attestation manager
+		strategy add_attestation_manager(comm_driver : string, attestation_manager : string, attestation_gate : string) <=
+			** "Attestation Manager added for communications driver " comm_driver **
+			let driver : component = ModelAccess.GetComponent(comm_driver);
+			let manager : component = ModelAccess.GetComponent(attestation_manager);
+			let gate : component = ModelAccess.GetComponent(attestation_gate);
+			attestation_manager_exists(driver, manager) and attestation_components_not_bypassed(driver, manager, gate) and component_implemented(manager, "attestation") and component_implemented(gate, "SPLAT")
+
+		-- Strategy for proper insertion of virtualization
+		strategy add_virtualization(bound_components : string, virtual_machine : string) <=
+			** bound_components " contained in VM " virtual_machine **
+			let vm_comps : {component} = ModelAccess.getComponentSet(bound_components);
+			let vm : component = ModelAccess.getComponent(virtual_machine);
+			vm_bound_to_processor(vm) and components_bound_to_vm(vm_comps, vm) and subcomponents_not_bound_to_other_processors(vm_comps, vm)
+
+		-- Strategy for proper insertion of a monitor
+		strategy add_monitor(comp_context : string, monitor : string, alert_port : string) <=
+			** "Monitor " monitor " is properly added to " comp_context **
+			let ctx : component = ModelAccess.getComponent(comp_context);
+			let mon : component = ModelAccess.getComponent(monitor);
+			let alert : feature = ModelAccess.getPort(alert_port);
+			component_exists(mon, CASE_Properties::Monitoring) and alert_connected(mon, alert) and independent_reset(mon, ctx) and component_implemented(mon, "SPLAT")
+
+		-- Strategy for proper insertion of a monitor with a gate
+		strategy add_monitor_gate(comp_context : string, monitor : string, alert_port : string, gate_context : string, message_type : data) <=
+			** "Monitor " monitor " is properly added to " comp_context **
+			let ctx : component = ModelAccess.getComponent(comp_context);
+			let mon : component = ModelAccess.getComponent(monitor);
+			let alert : feature = ModelAccess.getPort(alert_port);
+			let gate : component = ModelAccess.getComponent(gate_context);
+			component_exists(mon, CASE_Properties::Monitoring) and alert_connected(mon, alert) and independent_reset(mon, ctx) and component_not_bypassed(mon, gate, message_type) and component_implemented(mon, "SPLAT")
+
+		-- Strategy claim for proper insertion of a switch
+		strategy add_switch(comp_context : string, switch : string, message_type : data) <=
+			** "Switch inserted after " comp_context **
+			let ctx : component = ModelAccess.getComponent(comp_context);
+			let gate : component = ModelAccess.getComponent(switch);
+			component_exists(gate, CASE_Properties::Gating) and component_not_bypassed(gate, ctx, message_type) and component_implemented(gate, "SPLAT")
+
+		-- Strategy for proper transformation of model for seL4 build
+		strategy sel4_transform(comp_context : string) <=
+			** "Component " comp_context " transformed for seL4 build" **
+			let ctx : component = ModelAccess.getComponent(comp_context);
+			each_thread_in_separate_process(ctx)
+
+
+		----------------
+		-- SUB CLAIMS --
+		----------------
+
+		-- This connects to evidence that AGREE was previously run on the current version of the design.
+		goal agree_property_checked(c : string, property_id : string) <=
+			** "Formal verification proves model satisfies requirement" **
+			agree_passes_on_current_model(c, property_id) and confidence_in_agree_results()
+
+		goal agree_passes_on_current_model(c : string, property_id : string) <=
+			** "AGREE is run on most recent version of model and passes" **
+			let comp : component = ModelAccess.getComponent(c);
+			AgreeLib.hasAgreeProperty(comp, property_id) and analysis("AgreeCheck", type(parent(comp)))
+
+		-- Check to see if there is a filter immediately before 
+		-- the component on the communication pathway.
+		filter_exists(filter : component, comp_context : component, conn : connection) <=
+			** "A filter " filter " is connected to component " comp_context " by connection " conn **
+			let filters : {component} = recursive_backwards_filter_reach({comp_context});
+			let filter_parents : {component} = {(component)parent(f) for (f : filters) | has_parent(f) and (parent(f) instanceof component) and has_mitigation_type((component)parent(f), CASE_Properties::Filtering)};
+			let all_filters : {component} = union(filters, filter_parents);			
+			has_mitigation_type(filter, CASE_Properties::Filtering) and --connected(filter, conn, comp_context)
+			member(filter, all_filters) and exists(c : all_filters) . is_source_component(conn, c)						
+
+		recursive_backwards_filter_reach(curr : {component}) : {component} = 
+			let p_reach : {component} = {c for (c : prev_reach(curr)) | has_mitigation_type(c, CASE_Properties::Filtering)};
+			let prev : {component} = union(curr, p_reach); 
+			if prev = curr then 
+				curr
+			else 
+				recursive_backwards_filter_reach(prev)
+
+		-- Check to see if the specified component exists
+		component_exists(comp : component, mitigation_type : property<int>) <=
+			** comp " exists in the model" **
+			has_mitigation_type(comp, mitigation_type) and exists(m : component) . m = comp
+
+
+		-- Make sure there is no communication pathway that avoids the component
+		component_not_bypassed(comp : component, comp_context : component, msg_type : data) <=
+			** "Component " comp " cannot be bypassed" **
+			let comp_srcs : {component} = get_filter_sources(comp_context, comp, msg_type); 
+			let non_comp_srcs : {component} = get_non_filter_sources(comp_context, comp, msg_type); 
+			size(intersect(comp_srcs, non_comp_srcs)) = 0
+
+		-- This provides evidence that the high-assurance component was correctly generated for the appropriate os
+	    -- and that the proof was emitted and checked.
+	    component_implemented(comp : component, tool : string) <=
+		    ** "Component property implemented" **
+			implementation_language_assurance(comp) 
+--			and component_proof_checked(comp, tool)
+
+		-- Checks that a proof has been generated showing the component implementation
+		-- matches the AGREE contract
+		component_proof_checked(comp : component, tool : string) <=
+			** "Component proof checked" **
+			is_seL4_component(comp) => analysis("ToolCheck", tool)
+
+		has_mitigation_type(comp : component, mitigation_type : property<int>) : bool =
+			has_property(comp, mitigation_type) and property(comp, mitigation_type) = 100
+
+		is_comm_driver(comp : component) : bool =
+			has_property(comp, CASE_Properties::Comm_Driver) and property(comp, CASE_Properties::Comm_Driver) = true
+
+		-- Returns the set of components that are ancestors of a target component through communication pathways that don't pass through a filter
+		get_non_filter_sources(target : component, filter : component, msg_type : data) : {component} = 
+			let srcs : {component} = {c for (conn : connections(target)) (c : source_component(conn)) | has_type(conn) and type(conn) = msg_type and not is_source_component(conn, filter) and not is_source_component(conn, target)}; 
+			recursive_backwards_reach(srcs)
+
+		-- Returns the set of components that are ancestors of the filter on a target component
+		get_filter_sources(target : component, filter : component, msg_type : data) : {component} = 
+			let srcs : {component} = {c for (conn : connections(target)) (c : source_component(conn)) | has_type(conn) and type(conn) = msg_type and is_source_component(conn, filter)};
+			prev_reach(srcs)
+
+		recursive_backwards_reach(curr : {component}) : {component} = 
+			let prev : {component} = union(curr, prev_reach(curr)); 
+			if prev = curr then 
+				curr
+			else 
+				recursive_backwards_reach(prev)
+
+		prev_reach(curr : {component}) : {component} = 
+			{y for (x : curr) (y : backwards_reachable_components(x))}
+
+		backwards_reachable_components(comp : component) : {component} = 
+			{c for (conn : connections (comp)) (c : backwards_reachable_components_via_connection(comp, conn))}
+
+		backwards_reachable_components_via_connection(comp : component, conn : connection) : {component} = 
+			if is_port_connection(conn) then 
+				if is_destination_component(conn, comp) and not is_source_component(conn, comp) then
+					{source_component(conn)} 
+				else 
+					{} 
+			else 
+				{}
+
+		-- Evidence that an attestation manager component exists for a given communication driver
+		attestation_manager_exists(comm_driver : component, attestation_manager : component) <=
+			** "An attestation manager on " comm_driver " exists" **
+			-- check that the attestation manager only has attestation request/response connections to the comm driver
+			is_comm_driver(comm_driver) and has_mitigation_type(attestation_manager, CASE_Properties::Attesting) 
+
+		-- Evidence that communication from the comm driver cannot bypass attestation components
+		attestation_components_not_bypassed(comm_driver : component, attestation_manager : component, attestation_gate : component) <=
+			** "Attestation components cannot be bypassed" **
+			-- all outgoing connections from the comm driver to components inside the 
+			-- parent of the comm driver connect to the attestation manager or attestation gate
+			let out_conns : {connection} = {conn for (conn : connections(comm_driver)) | source_component(conn) = comm_driver and not (destination_component(conn) = parent(comm_driver))};
+			forall(conn : out_conns) . (not is_software_component(destination_component(conn)) or has_mitigation_type(destination_component(conn), CASE_Properties::Attesting) or has_mitigation_type(destination_component(conn), CASE_Properties::Gating))
+
+		-- Checks if the specified virtual processor is a CASE Virtualization and is bound to a processor
+		vm_bound_to_processor(virtual_machine : component) <=
+			** virtual_machine " is bound to a processor" **
+			has_mitigation_type(virtual_machine, CASE_Properties::Isolating) and exists(p : processor) . is_bound_to(virtual_machine, p)
+
+		-- Checks that bindings exist between specified virtualized components and virtual processor
+		components_bound_to_vm(bound_components : {component}, virtual_machine : component) <=
+			** "Components are bound to virtual processor " virtual_machine **
+			forall (c : bound_components) . check_vm_binding(c, virtual_machine)
+
+		-- Checks that the specified component is bound to the specified virtual processor
+		check_vm_binding(c : component, virtual_machine : component) <=
+			** "Component " c " is bound to virtual processor " virtual_machine **
+			is_bound_to(c, virtual_machine)
+
+		-- Checks that subcomponents of specified virtualized components are not bound to processors other than the 
+		-- specified VM
+		subcomponents_not_bound_to_other_processors(bound_components : {component}, virtual_machine : component) <=
+			** "Subcomponents are not bound to other processors" **
+			let subs : {component} = get_subcomponents(next_subcomponent(bound_components));
+			forall (s : subs) . not exists (v : component) . (is_bound_to_processor(s, v) and not (v = virtual_machine))
+
+		-- Get set of descendants
+		get_subcomponents(curr : {component}) : {component} =
+			let next : {component} = union(curr, next_subcomponent(curr));
+			if next = curr then
+				curr
+			else
+				get_subcomponents(next)
+
+		next_subcomponent(curr : {component}) : {component} =
+			{y for (x : curr) (y : subcomponents(x))}
+
+		implementation_language_assurance(comp : component) <=
+			** comp " implementation is appropriate for OS" **
+			is_seL4_component(comp) => is_cakeml_component(comp)
+
+		is_cakeml_component(comp : component) : bool =
+			if is_thread(comp) then (has_property(comp, CASE_Properties::Component_Language) and property(comp, CASE_Properties::Component_Language) = "CakeML")
+			else if is_process(comp) then size(subcomponents(comp)) > 0 and forall(t : subcomponents(comp)) . is_cakeml_component(t)
+			else false
+
+		-- checks that a component will run on seL4 by checking that the processors it is bound to have the seL4 OS property
+		is_seL4_component(comp : component) : bool =
+			let proc : {component} = {c for (c : component) | is_bound_to_processor(comp, c)};
+			(size(proc) > 0) and forall (p : proc) . (has_property(p, CASE_Properties::OS) and property(p, CASE_Properties::OS) = "seL4")
+
+		is_bound_to_processor(c : component, p : component) : bool =
+			is_bound_to(c, p) and (is_processor(p) or is_virtual_processor(p))
+
+		alert_connected(monitor : component, alert_port : feature) <=
+			** "Monitor Alert port is connected" **
+			contained(alert_port, monitor) and length(connections(alert_port)) > 0
+
+		independent_reset(monitor : component, comp_context : component) <=
+			** "Monitor reset port cannot be triggered by source of observed signal" **
+			let reset_ancestors : {component} = {comp for (conn : connections(monitor)) (comp : recursive_backwards_reach({source_component(conn)})) | destination_component(conn) = monitor and name(destination(conn)) = "Reset"};
+			length(intersect(reset_ancestors, {comp_context})) = 0
+
+		is_software_component(comp : component) : bool =
+			is_process(comp) or is_thread_group(comp) or is_thread(comp)
+
+		is_high_assurance_component(comp : component) : bool =
+			has_mitigation_type(comp, CASE_Properties::Filtering) or has_mitigation_type(comp, CASE_Properties::Monitoring) or has_mitigation_type(comp, CASE_Properties::Gating)
+
+		each_thread_in_separate_process(root : component) <=
+			** "Each thread runs in a separate process" **
+			let comps : {component} = get_subcomponents({root});
+			forall (c : comps) . ((is_system(c) or is_thread(c) or is_process(c)) and is_process(c) => (length(subcomponents(c)) = 1 and is_thread(head(as_list(subcomponents(c))))))
+
+	**};
+
+end CASE_Model_Transformations;