feat(kernel): shared ABI decoder+proofs, no-panic gate, syscall storm, kani on shrunk kernel

crates/kernel/src/proofs/authority.rs

@@ -0,0 +1,118 @@
+//! Mint creates no authority. The real kernel, with tables shrunk under
+//! `cfg(kani)`, runs `mint` with arbitrary arguments in a small state
+//! whose capabilities carry arbitrary rights. Afterwards every capability
+//! to an object that already existed carries no more rights than some
+//! capability to that object carried before.
+//!
+//! Only this harness is kept. The same check over delegate, delete,
+//! revoke, create and kill either exceeded 12 GB in CBMC or tripped
+//! modelling artifacts ("unreachable code" on safe `Option` matches that
+//! an exhaustive host replay never reaches). Those operations are covered
+//! by the syscall storm's global invariants (tests/storm.rs) and the
+//! capability-tree model test (tests/captree_model.rs) instead.
+
+use super::platform::KaniPlatform;
+use crate::Kernel;
+use domain::{capability::MAX_CAPS_PER_PROCESS, process::MAX_PROCESSES, resource::Resource};
+use types::{
+    address::PhysicalAddress,
+    badge::Badge,
+    bounded::{CapSlot, Priority},
+    id::ProcessId,
+    permission::PermissionSet,
+    time::TimeSlice,
+};
+
+#[derive(Clone, Copy, PartialEq)]
+struct Held {
+    resource: Resource,
+    perms: PermissionSet,
+    badge: Badge,
+}
+
+type Snapshot = [[Option<Held>; MAX_CAPS_PER_PROCESS]; MAX_PROCESSES];
+
+fn snapshot(k: &Kernel<KaniPlatform>) -> Snapshot {
+    let mut s = [[None; MAX_CAPS_PER_PROCESS]; MAX_PROCESSES];
+    for (p, row) in s.iter_mut().enumerate() {
+        if let Ok(process) = k.processes.get(ProcessId::from_raw(p as u16)) {
+            for (slot, cap) in process.capabilities().iter() {
+                row[slot.value() as usize] = Some(Held {
+                    resource: *cap.resource(),
+                    perms: *cap.permissions(),
+                    badge: cap.badge(),
+                });
+            }
+        }
+    }
+    s
+}
+
+/// Whether `resource` named a live object before the operation.
+fn existed(before: &Snapshot, resource: &Resource) -> bool {
+    before
+        .iter()
+        .flatten()
+        .flatten()
+        .any(|h| h.resource == *resource)
+}
+
+/// Some capability before the operation already granted at least `h`.
+fn justified(before: &Snapshot, h: &Held) -> bool {
+    before.iter().flatten().flatten().any(|b| {
+        b.resource == h.resource
+            && h.perms.is_subset_of(&b.perms)
+            && (b.badge == h.badge || b.badge.is_none())
+    })
+}
+
+fn any_perms() -> PermissionSet {
+    PermissionSet::from_bits(kani::any::<u8>() & 0b1111)
+}
+
+fn any_slot() -> CapSlot {
+    CapSlot::new(kani::any::<u8>() % (CapSlot::MAX + 1)).unwrap()
+}
+
+/// Init and one more process, an endpoint, a notification, and caps with
+/// arbitrary rights spread over both, including a cap to the other process.
+fn small_world() -> Kernel<KaniPlatform> {
+    let mut k = Kernel::new(KaniPlatform, PhysicalAddress::from_raw(0x8400_0000), 6);
+    let (init, _) = k.boot(Priority::DEFAULT, TimeSlice::DEFAULT).unwrap();
+    let b = k.create_process_internal().unwrap();
+    k.spawn_thread_internal(b).unwrap();
+    let ep = k.create_endpoint(init).unwrap();
+    let n = k.create_notification(b).unwrap();
+    k.grant_capability(init, Resource::Endpoint(ep), any_perms())
+        .unwrap();
+    k.grant_capability(init, Resource::Process(b), any_perms())
+        .unwrap();
+    k.grant_capability(b, Resource::Endpoint(ep), any_perms())
+        .unwrap();
+    k.grant_capability(b, Resource::Notification(n), any_perms())
+        .unwrap();
+    k
+}
+
+/// The caller is concrete: a symbolic pid turns every table lookup into a
+/// symbolic index and blows CBMC's formula up past 30 GB.
+#[kani::proof]
+#[kani::unwind(8)]
+fn mint_creates_no_authority() {
+    let mut k = small_world();
+    let (slot, badge, perms) = (any_slot(), Badge::new(kani::any()), any_perms());
+    let before = snapshot(&k);
+    let _ = k.mint(ProcessId::from_raw(0), slot, badge, perms);
+    let after = snapshot(&k);
+    for (p, row) in after.iter().enumerate() {
+        for (s, held) in row.iter().enumerate() {
+            let Some(h) = held else { continue };
+            if before[p][s] == Some(*h) {
+                continue; // untouched
+            }
+            if existed(&before, &h.resource) {
+                assert!(justified(&before, h), "authority appeared from nowhere");
+            }
+        }
+    }
+}