diff --git a/README.md b/README.md index 5962a6f..02e39f9 100644 --- a/README.md +++ b/README.md @@ -145,6 +145,10 @@ Given an entry from a compartment's `imports` array, returns the corresponding ` Type predicates that, given an entry from a compartment's `imports` array, hold if the import refers to a cross-compartment call, a cross-library call, or an MMIO capability. +`import_is_callable(a)` + +Type predicate that, given an entry from a compartment's `imports` array, holds if the import refers to either a compartment or library call. + `mmio_imports_for_compartment(compartment)` Helper that returns all of the MMIO imports for a compartment. @@ -178,6 +182,13 @@ Returns an array of all compartments that can directly call a specific export ta Given a compartment name and a regular expression (uniquely) describing an exported function, return the array of compartments that may directly call that function. +`compartment_exports_function(callee, importEntry)` + +Predicate that matches if the compartment (or library) named by `callee` is the compartment that exports the entry point given by `importEntry`. + +`compartments_calling(callee)` + +Returns the names of all compartments that call the compartment named by `callee` (via any exported function). `allow_list(testArray, allowSet)` @@ -192,6 +203,10 @@ Predicate that, given the name of a device and a set of compartments that are al Predicate that, given the name of a compartment and a regular expression that uniquely identifies one of its exported functions, fails if any compartment not in the allow set is able to call it. +`compartment_allow_list(compartmentName, allowSet)` + +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. + ### The RTOS package diff --git a/compartment.hh b/compartment.hh index ea8435d..3dc4c1e 100644 --- a/compartment.hh +++ b/compartment.hh @@ -10,11 +10,12 @@ namespace compartment.exports[_] == export } - files_for_export(export) = f { - some compartments - compartments = [compartment | compartment = input.compartments[_]; compartment_contains_export(compartment, export)] - # FIXME: Look in data sections as well - f = {f2 | compartments[_].code.inputs[_].file = f2} + compartment_includes_file(compartment, filename) { + compartment.code.inputs[_].file == filename + } + + compartment_includes_file(compartment, filename) { + compartment.data.inputs[_].file == filename } export_matches_import(export, importEntry) { @@ -26,10 +27,10 @@ namespace some possibleEntries some allExports allExports = {export | input.compartments[_].exports[_] = export} - possibleEntries = [entry | entry = allExports[_]; export_matches_import(entry, importEntry)] + possibleEntries = [{"compartment": compartment, "entry": entry} | entry = input.compartments[compartment].exports[_]; export_matches_import(entry, importEntry)] count(possibleEntries) == 1 - files_for_export(possibleEntries[0])[_] == importEntry.provided_by - entry := possibleEntries[0] + compartment_includes_file(input.compartments[possibleEntries[0].compartment], importEntry.provided_by) + entry := possibleEntries[0].entry } import_is_library_call(a) { a.kind = "LibraryFunction" } @@ -39,6 +40,14 @@ namespace a.function } + import_is_call { + import_is_library_call(importEntry) + } + + import_is_call { + import_is_compartment_call(importEntry) + } + mmio_imports_for_compartment(compartment) = entry { entry := [e | e = compartment.imports[_]; import_is_MMIO(e)] } @@ -81,6 +90,36 @@ namespace compartments = compartments_calling_export(compartment_export_matching_symbol(compartmentName, export)) } + # Helper that builds a map from symbol names to compartments. This is + # to avoid some O(n^2) lookups. Or would, if rego-cpp didn't recompute + # this every evaluation. + #entry_point_map := { entry.export_symbol : compartment | entry = input.compartments[compartment].exports[_] ; entry.kind = "Function"} + + compartment_exports_function(callee, importEntry) { + #entry_point_map[importEntry.export_symbol] == callee + some possibleEntries + possibleEntries = [entry | entry = input.compartments[callee].exports[_]; export_matches_import(entry, importEntry)] + count(possibleEntries) == 1 + compartment_includes_file(input.compartments[callee], importEntry.provided_by) + } + + # Helper to work around rego-cpp#117 + check_export(exports, importEntry, compartment) { + exports[importEntry.export_symbol] == compartment + } + + compartments_calling(callee) = compartments { + # Create a reverse map that maps from exported symbols to + # compartments. This avoids some O(n^2) lookups. It would be nice + # to cache this globally but rego-cpp doesn't support that yet. + # This reduces the time for this query on the test suite from over + # 6s to under 0.5s for me. + some entry_point_map + entry_point_map = { entry.export_symbol : compartment | entry = input.compartments[compartment].exports[_] ; entry.kind = "Function"} + compartments = {c | i = input.compartments[c].imports[_]; check_export(entry_point_map, i, callee)} + } + + # Helper for allow lists. Functions cannot return sets, so this # accepts an array of compartment names that match some property and # evaluates to true if and only if each one is also present in the allow @@ -98,5 +137,10 @@ namespace compartment_call_allow_list(compartmentName, exportPattern, allowList) { allow_list(compartments_calling_export_matching(compartmentName, exportPattern), allowList) } + + compartment_allow_list(compartmentName, allowList) { + allow_list(compartments_calling(compartmentName), allowList) + } + )"; } // namespace