From 8c2c00eadc209224af49991df621991f17181450 Mon Sep 17 00:00:00 2001 From: David Chisnall Date: Thu, 15 Aug 2024 11:02:17 +0100 Subject: [PATCH] Add support for auditing shared objects. --- README.md | 27 +++++++++++++++++++++++++++ compartment.hh | 38 ++++++++++++++++++++++++++++++++++++++ rtos.hh | 27 +++++++++++++++++++++++++++ 3 files changed, 92 insertions(+) diff --git a/README.md b/README.md index 02e39f9..be43cbf 100644 --- a/README.md +++ b/README.md @@ -207,6 +207,33 @@ Predicate that, given the name of a compartment and a regular expression that un Predicate that, given the name of a compartment, fails if any compartment not in the allow set is able to call any of the exported entry points from this function. +`shared_object_imports_for_compartment(compartment)` + +Given a compartment name, return a list of all of the imports of shared objects. + +`compartment_imports_shared_object(compartment, object)` + +Predicate that evaluates to true if the compartment named `compartment` imports the shared object named with the name given by the second. + +`compartment_imports_shared_object_writeable(compartment, object)` + +Predicate that evaluates to true if the compartment named `compartment` imports the shared object named with the name given by the second *and* that compartment can write to the shared object. + +`compartments_with_shared_object_import(object)` + +Given the name of a shared object, evaluates to a list of compartments that import that object. + +`compartments_with_shared_object_import_writeable(object)` + +Given the name of a shared object, evaluates to a list of compartments that import that object with permissions that allow writing. + +`shared_object_allow_list(objectName, allowList)` + +Predicate that, given the name of a shared object and a set of compartments that are allowed to access it, fails if any other compartment has access to the global. + +`shared_object_writeable_allow_list(objectName, allowList)` + +Predicate that, given the name of a shared object and a set of compartments that are allowed to access it, fails if any other compartment has write access to the global. ### The RTOS package diff --git a/compartment.hh b/compartment.hh index 3dc4c1e..fe9061d 100644 --- a/compartment.hh +++ b/compartment.hh @@ -73,6 +73,28 @@ namespace compartments = [i | c = input.compartments[i]; compartment_imports_device(c, device)] } + shared_object_imports_for_compartment(compartment) = entry { + entry := [e | e = compartment.imports[_]; e.kind = "SharedObject"] + } + + compartment_imports_shared_object(compartment, object) { + count([d | d = shared_object_imports_for_compartment(compartment)[_] ; d.shared_object = object)]) > 0 + } + + compartment_imports_shared_object_writeable(compartment, object) { + count([d | d = shared_object_imports_for_compartment(compartment)[_] ; d.shared_object = object + d.permits_store = true]) > 0 + } + + compartments_with_shared_object_import(object) = compartments { + compartments = [i | c = input.compartments[i]; compartment_imports_shared_object(c, object)] + } + + compartments_with_shared_object_import_writeable(object) = compartments { + compartments = [i | c = input.compartments[i]; compartment_imports_shared_object_writeable(c, object)] + } + + compartment_export_matching_symbol(compartmentName, symbol) = export { some compartment compartment = input.compartments[compartmentName] @@ -134,6 +156,15 @@ namespace allow_list(compartments_with_mmio_import(data.board.devices[mmioName]), allowList) } + shared_object_allow_list(objectName, allowList) { + allow_list(compartments_with_shared_object_import(objectName), allowList) + } + + shared_object_writeable_allow_list(objectName, allowList) { + allow_list(compartments_with_shared_object_import_writeable(objectName), allowList) + } + + compartment_call_allow_list(compartmentName, exportPattern, allowList) { allow_list(compartments_calling_export_matching(compartmentName, exportPattern), allowList) } @@ -142,5 +173,12 @@ namespace allow_list(compartments_calling(compartmentName), allowList) } + shared_object(name) = object { + some imports + imports = [ i | i = input.sharedObjects[_] ; i.name = name] + count(imports) == 1 + object := imports[0] + } + )"; } // namespace diff --git a/rtos.hh b/rtos.hh index 5cd5a21..66ef5c0 100644 --- a/rtos.hh +++ b/rtos.hh @@ -35,6 +35,17 @@ namespace } } + # Check that the allocator imports the hazard list with the correct permissions. + allocator_hazard_list_permissions_are_valid { + some hazardListImport + hazardListImport = [ i | i = input.compartments.allocator.imports[_] ; i.shared_object == "allocator_hazard_pointers"] + every i in hazardListImport { + i.permits_load == true + i.permits_load_store_capabilities == true + i.permits_load_mutable == false + i.permits_store == false + } + } valid { all_sealed_allocator_capabilities_are_valid @@ -43,6 +54,22 @@ namespace # Only the scheduler may access the interrupt controllers. data.compartment.mmio_allow_list("clint", {"scheduler"}) data.compartment.mmio_allow_list("plic", {"scheduler"}) + # Only the allocator may access the hazard list (the switcher can + # as well via another mechanism) + data.compartment.shared_object_allow_list("allocator_hazard_pointers", {"allocator"}) + # Only the allocator may write to the epoch. + # Currently, only the compartment-helpers library reads the epoch, + # but it isn't a security problem if anything else does. + data.compartment.shared_object_writeable_allow_list("allocator_epoch", {"allocator"}) + # Size of hazard list and allocator epoch. + some hazardList + hazardList = data.compartment.shared_object("allocator_hazard_pointers") + # Two hazard pointers per thread. + hazardList.end - hazardList.start = count(input.threads) * 2 * 8 + some epoch + epoch = data.compartment.shared_object("allocator_epoch") + # 32-bit epoch + epoch.end - epoch.start = 4 } )"; }