Add support for auditing shared objects.

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
 

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

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
 		}
 		)";
 }