From 71518a93a41aed301ec7f201281941021252b6c4 Mon Sep 17 00:00:00 2001 From: Gabriel Kaszewski Date: Sun, 18 Oct 2026 01:08:05 +0200 Subject: [PATCH] refactor(proofs): split into per-topic modules with shared helpers across types, domain, and kernel --- crates/domain/src/proofs.rs | 184 ------------- crates/domain/src/proofs/capability.rs | 37 +++ crates/domain/src/proofs/delegation.rs | 66 +++++ crates/domain/src/proofs/mod.rs | 23 ++ crates/domain/src/proofs/thread.rs | 50 ++++ crates/kernel/src/proofs.rs | 340 ------------------------- crates/kernel/src/proofs/delegation.rs | 95 +++++++ crates/kernel/src/proofs/mediation.rs | 66 +++++ crates/kernel/src/proofs/message.rs | 46 ++++ crates/kernel/src/proofs/mod.rs | 25 ++ crates/kernel/src/proofs/revocation.rs | 63 +++++ crates/types/src/proofs.rs | 83 ------ crates/types/src/proofs/bounded.rs | 32 +++ crates/types/src/proofs/generation.rs | 10 + crates/types/src/proofs/mod.rs | 3 + crates/types/src/proofs/permissions.rs | 38 +++ 16 files changed, 554 insertions(+), 607 deletions(-) delete mode 100644 crates/domain/src/proofs.rs create mode 100644 crates/domain/src/proofs/capability.rs create mode 100644 crates/domain/src/proofs/delegation.rs create mode 100644 crates/domain/src/proofs/mod.rs create mode 100644 crates/domain/src/proofs/thread.rs delete mode 100644 crates/kernel/src/proofs.rs create mode 100644 crates/kernel/src/proofs/delegation.rs create mode 100644 crates/kernel/src/proofs/mediation.rs create mode 100644 crates/kernel/src/proofs/message.rs create mode 100644 crates/kernel/src/proofs/mod.rs create mode 100644 crates/kernel/src/proofs/revocation.rs delete mode 100644 crates/types/src/proofs.rs create mode 100644 crates/types/src/proofs/bounded.rs create mode 100644 crates/types/src/proofs/generation.rs create mode 100644 crates/types/src/proofs/mod.rs create mode 100644 crates/types/src/proofs/permissions.rs diff --git a/crates/domain/src/proofs.rs b/crates/domain/src/proofs.rs deleted file mode 100644 index 864669f..0000000 --- a/crates/domain/src/proofs.rs +++ /dev/null @@ -1,184 +0,0 @@ -#[cfg(kani)] -mod kani_proofs { - use crate::capability::{Capability, CapabilityTable}; - use crate::resource::Resource; - use crate::thread::{BlockReason, Thread, ThreadState}; - use types::bounded::Priority; - use types::generation::Generation; - use types::id::{CoreId, EndpointId, ProcessId, ThreadId}; - use types::permission::{Permission, PermissionSet}; - use types::time::TimeSlice; - - // --- Capability non-escalation --- - - #[kani::proof] - fn delegation_via_cap_table_never_escalates() { - let source_bits: u8 = kani::any(); - let restrict_bits: u8 = kani::any(); - let ep_id: u16 = kani::any(); - kani::assume(ep_id < 256); - - let source_perms = PermissionSet::from_bits(source_bits); - kani::assume(source_perms.allows(Permission::Delegate)); - - let resource = Resource::Endpoint(EndpointId::from_raw(ep_id)); - let source_cap = Capability::new(resource.clone(), source_perms, Generation::initial()); - - let mut source_table = CapabilityTable::new(); - let slot = source_table.insert(source_cap); - kani::assume(slot.is_ok()); - let slot = slot.unwrap(); - - let cap = source_table.get(slot).unwrap(); - let original_perms = *cap.permissions(); - let delegated_perms = original_perms.restrict_to(&PermissionSet::from_bits(restrict_bits)); - - let mut target_table = CapabilityTable::new(); - let delegated_cap = Capability::new(cap.resource().clone(), delegated_perms, Generation::initial()); - let target_slot = target_table.insert(delegated_cap); - kani::assume(target_slot.is_ok()); - - let result = target_table.get(target_slot.unwrap()).unwrap(); - assert!(result.permissions().is_subset_of(&original_perms)); - } - - #[kani::proof] - fn delegation_cannot_add_permissions_not_in_source() { - let source_bits: u8 = kani::any(); - let restrict_bits: u8 = kani::any(); - - let source = PermissionSet::from_bits(source_bits); - let restrict = PermissionSet::from_bits(restrict_bits); - let result = source.restrict_to(&restrict); - - if !source.allows(Permission::Read) { - assert!(!result.allows(Permission::Read)); - } - if !source.allows(Permission::Write) { - assert!(!result.allows(Permission::Write)); - } - if !source.allows(Permission::Execute) { - assert!(!result.allows(Permission::Execute)); - } - if !source.allows(Permission::Delegate) { - assert!(!result.allows(Permission::Delegate)); - } - if !source.allows(Permission::Revoke) { - assert!(!result.allows(Permission::Revoke)); - } - } - - // --- Capability table integrity --- - - #[kani::proof] - fn cap_table_insert_get_roundtrip() { - let bits: u8 = kani::any(); - let ep_id: u16 = kani::any(); - kani::assume(ep_id < 256); - - let perms = PermissionSet::from_bits(bits); - let resource = Resource::Endpoint(EndpointId::from_raw(ep_id)); - let cap = Capability::new(resource, perms, Generation::initial()); - - let mut table = CapabilityTable::new(); - let slot = table.insert(cap); - kani::assume(slot.is_ok()); - let slot = slot.unwrap(); - - let retrieved = table.get(slot).unwrap(); - assert!(*retrieved.permissions() == perms); - } - - #[kani::proof] - fn cap_table_remove_then_get_fails() { - let bits: u8 = kani::any(); - - let cap = Capability::new( - Resource::ProcessCreate, - PermissionSet::from_bits(bits), - Generation::initial(), - ); - - let mut table = CapabilityTable::new(); - let slot = table.insert(cap); - kani::assume(slot.is_ok()); - let slot = slot.unwrap(); - - table.remove(slot).unwrap(); - assert!(table.get(slot).is_err()); - } - - // --- Thread state machine safety --- - - #[kani::proof] - fn dead_thread_rejects_all_transitions() { - let mut thread = Thread::new( - ThreadId::from_raw(0), - ProcessId::from_raw(0), - Priority::new(16).unwrap(), - TimeSlice::new(100), - None, - ); - - thread.set_running(CoreId::from_raw(0)).unwrap(); - thread.exit().unwrap(); - - assert!(matches!(thread.state(), ThreadState::Dead)); - assert!(thread.set_running(CoreId::from_raw(0)).is_err()); - assert!(thread.block(BlockReason::WaitingAny).is_err()); - assert!(thread.unblock().is_err()); - assert!(thread.preempt().is_err()); - assert!(thread.exit().is_err()); - } - - #[kani::proof] - fn only_running_thread_can_block() { - let prio_val: u8 = kani::any(); - kani::assume(prio_val <= 31); - let prio = Priority::new(prio_val).unwrap(); - - let mut thread = Thread::new( - ThreadId::from_raw(0), - ProcessId::from_raw(0), - prio, - TimeSlice::new(100), - None, - ); - - assert!(matches!(thread.state(), ThreadState::Ready)); - assert!(thread.block(BlockReason::WaitingAny).is_err()); - } - - #[kani::proof] - fn blocked_thread_cannot_run_directly() { - let mut thread = Thread::new( - ThreadId::from_raw(0), - ProcessId::from_raw(0), - Priority::new(16).unwrap(), - TimeSlice::new(100), - None, - ); - - thread.set_running(CoreId::from_raw(0)).unwrap(); - thread.block(BlockReason::WaitingAny).unwrap(); - - assert!(thread.set_running(CoreId::from_raw(0)).is_err()); - } - - // --- Chained delegation --- - - #[kani::proof] - fn chained_delegation_never_escalates() { - let original_bits: u8 = kani::any(); - let restrict1_bits: u8 = kani::any(); - let restrict2_bits: u8 = kani::any(); - - let original = PermissionSet::from_bits(original_bits); - let after_first = original.restrict_to(&PermissionSet::from_bits(restrict1_bits)); - let after_second = after_first.restrict_to(&PermissionSet::from_bits(restrict2_bits)); - - assert!(after_first.is_subset_of(&original)); - assert!(after_second.is_subset_of(&after_first)); - assert!(after_second.is_subset_of(&original)); - } -} diff --git a/crates/domain/src/proofs/capability.rs b/crates/domain/src/proofs/capability.rs new file mode 100644 index 0000000..cfed119 --- /dev/null +++ b/crates/domain/src/proofs/capability.rs @@ -0,0 +1,37 @@ +use crate::capability::CapabilityTable; +use crate::resource::Resource; +use super::{arbitrary_endpoint_cap, insert_cap}; +use types::permission::PermissionSet; + +#[kani::proof] +fn cap_table_insert_get_roundtrip() { + let bits: u8 = kani::any(); + let ep_id: u16 = kani::any(); + kani::assume(ep_id < 256); + + let perms = PermissionSet::from_bits(bits); + let cap = arbitrary_endpoint_cap(bits, ep_id); + + let mut table = CapabilityTable::new(); + let slot = insert_cap(&mut table, cap); + + let retrieved = table.get(slot).unwrap(); + assert!(*retrieved.permissions() == perms); +} + +#[kani::proof] +fn cap_table_remove_then_get_fails() { + let bits: u8 = kani::any(); + + let cap = crate::capability::Capability::new( + Resource::ProcessCreate, + PermissionSet::from_bits(bits), + types::generation::Generation::initial(), + ); + + let mut table = CapabilityTable::new(); + let slot = insert_cap(&mut table, cap); + + table.remove(slot).unwrap(); + assert!(table.get(slot).is_err()); +} diff --git a/crates/domain/src/proofs/delegation.rs b/crates/domain/src/proofs/delegation.rs new file mode 100644 index 0000000..dcc16eb --- /dev/null +++ b/crates/domain/src/proofs/delegation.rs @@ -0,0 +1,66 @@ +use crate::capability::{Capability, CapabilityTable}; +use crate::resource::Resource; +use super::{arbitrary_endpoint_cap, insert_cap}; +use types::generation::Generation; +use types::id::EndpointId; +use types::permission::{Permission, PermissionSet}; + +#[kani::proof] +fn delegation_via_cap_table_never_escalates() { + let source_bits: u8 = kani::any(); + let restrict_bits: u8 = kani::any(); + let ep_id: u16 = kani::any(); + kani::assume(ep_id < 256); + + let source_perms = PermissionSet::from_bits(source_bits); + kani::assume(source_perms.allows(Permission::Delegate)); + + let mut source_table = CapabilityTable::new(); + let slot = insert_cap(&mut source_table, arbitrary_endpoint_cap(source_bits, ep_id)); + + let cap = source_table.get(slot).unwrap(); + let original_perms = *cap.permissions(); + let delegated_perms = original_perms.restrict_to(&PermissionSet::from_bits(restrict_bits)); + + let delegated_cap = Capability::new( + Resource::Endpoint(EndpointId::from_raw(ep_id)), + delegated_perms, + Generation::initial(), + ); + + let mut target_table = CapabilityTable::new(); + let target_slot = insert_cap(&mut target_table, delegated_cap); + + let result = target_table.get(target_slot).unwrap(); + assert!(result.permissions().is_subset_of(&original_perms)); +} + +#[kani::proof] +fn delegation_cannot_add_permissions_not_in_source() { + let source_bits: u8 = kani::any(); + let restrict_bits: u8 = kani::any(); + + let source = PermissionSet::from_bits(source_bits); + let result = source.restrict_to(&PermissionSet::from_bits(restrict_bits)); + + if !source.allows(Permission::Read) { assert!(!result.allows(Permission::Read)); } + if !source.allows(Permission::Write) { assert!(!result.allows(Permission::Write)); } + if !source.allows(Permission::Execute) { assert!(!result.allows(Permission::Execute)); } + if !source.allows(Permission::Delegate) { assert!(!result.allows(Permission::Delegate)); } + if !source.allows(Permission::Revoke) { assert!(!result.allows(Permission::Revoke)); } +} + +#[kani::proof] +fn chained_delegation_never_escalates() { + let original_bits: u8 = kani::any(); + let restrict1_bits: u8 = kani::any(); + let restrict2_bits: u8 = kani::any(); + + let original = PermissionSet::from_bits(original_bits); + let after_first = original.restrict_to(&PermissionSet::from_bits(restrict1_bits)); + let after_second = after_first.restrict_to(&PermissionSet::from_bits(restrict2_bits)); + + assert!(after_first.is_subset_of(&original)); + assert!(after_second.is_subset_of(&after_first)); + assert!(after_second.is_subset_of(&original)); +} diff --git a/crates/domain/src/proofs/mod.rs b/crates/domain/src/proofs/mod.rs new file mode 100644 index 0000000..065f2a7 --- /dev/null +++ b/crates/domain/src/proofs/mod.rs @@ -0,0 +1,23 @@ +mod capability; +mod delegation; +mod thread; + +use crate::capability::{Capability, CapabilityTable}; +use crate::resource::Resource; +use types::generation::Generation; +use types::id::EndpointId; +use types::permission::PermissionSet; + +fn arbitrary_endpoint_cap(bits: u8, ep_id: u16) -> Capability { + Capability::new( + Resource::Endpoint(EndpointId::from_raw(ep_id)), + PermissionSet::from_bits(bits), + Generation::initial(), + ) +} + +fn insert_cap(table: &mut CapabilityTable, cap: Capability) -> types::bounded::CapSlot { + let slot = table.insert(cap); + kani::assume(slot.is_ok()); + slot.unwrap() +} diff --git a/crates/domain/src/proofs/thread.rs b/crates/domain/src/proofs/thread.rs new file mode 100644 index 0000000..75bf400 --- /dev/null +++ b/crates/domain/src/proofs/thread.rs @@ -0,0 +1,50 @@ +use crate::thread::{BlockReason, Thread, ThreadState}; +use types::bounded::Priority; +use types::id::{CoreId, ProcessId, ThreadId}; +use types::time::TimeSlice; + +fn test_thread(prio: Priority) -> Thread { + Thread::new( + ThreadId::from_raw(0), + ProcessId::from_raw(0), + prio, + TimeSlice::new(100), + None, + ) +} + +#[kani::proof] +fn dead_thread_rejects_all_transitions() { + let mut thread = test_thread(Priority::new(16).unwrap()); + + thread.set_running(CoreId::from_raw(0)).unwrap(); + thread.exit().unwrap(); + + assert!(matches!(thread.state(), ThreadState::Dead)); + assert!(thread.set_running(CoreId::from_raw(0)).is_err()); + assert!(thread.block(BlockReason::WaitingAny).is_err()); + assert!(thread.unblock().is_err()); + assert!(thread.preempt().is_err()); + assert!(thread.exit().is_err()); +} + +#[kani::proof] +fn only_running_thread_can_block() { + let prio_val: u8 = kani::any(); + kani::assume(prio_val <= 31); + + let mut thread = test_thread(Priority::new(prio_val).unwrap()); + + assert!(matches!(thread.state(), ThreadState::Ready)); + assert!(thread.block(BlockReason::WaitingAny).is_err()); +} + +#[kani::proof] +fn blocked_thread_cannot_run_directly() { + let mut thread = test_thread(Priority::new(16).unwrap()); + + thread.set_running(CoreId::from_raw(0)).unwrap(); + thread.block(BlockReason::WaitingAny).unwrap(); + + assert!(thread.set_running(CoreId::from_raw(0)).is_err()); +} diff --git a/crates/kernel/src/proofs.rs b/crates/kernel/src/proofs.rs deleted file mode 100644 index 23ec2f7..0000000 --- a/crates/kernel/src/proofs.rs +++ /dev/null @@ -1,340 +0,0 @@ -#[cfg(kani)] -mod kani_proofs { - use domain::capability::{Capability, CapabilityTable}; - use domain::message::{Message, MAX_MESSAGE_WORDS}; - use domain::resource::Resource; - use types::bounded::CapSlot; - use types::generation::Generation; - use types::id::{EndpointId, ProcessId}; - use types::permission::{Permission, PermissionSet}; - - #[kani::proof] - fn kernel_delegate_path_never_escalates() { - let source_bits: u8 = kani::any(); - let restrict_bits: u8 = kani::any(); - let ep_id: u16 = kani::any(); - kani::assume(ep_id < 256); - - let source_perms = PermissionSet::from_bits(source_bits); - kani::assume(source_perms.allows(Permission::Delegate)); - - let resource = Resource::Endpoint(EndpointId::from_raw(ep_id)); - - // Step 1: source process has a capability (simulates check_cap) - let mut source_table = CapabilityTable::new(); - let source_cap = Capability::new(resource.clone(), source_perms, Generation::initial()); - let slot = source_table.insert(source_cap); - kani::assume(slot.is_ok()); - let slot = slot.unwrap(); - - // Step 2: kernel reads source cap and restricts (simulates handle_delegate) - let cap = source_table.get(slot).unwrap(); - let original_perms = *cap.permissions(); - let restricted = original_perms.restrict_to(&PermissionSet::from_bits(restrict_bits)); - - // Step 3: kernel inserts into target (simulates grant_cap) - let mut target_table = CapabilityTable::new(); - let delegated = Capability::new(cap.resource().clone(), restricted, Generation::initial()); - let target_slot = target_table.insert(delegated); - kani::assume(target_slot.is_ok()); - - // PROOF: the capability in the target table has permissions - // that are a strict subset of what the source held - let result = target_table.get(target_slot.unwrap()).unwrap(); - assert!(result.permissions().is_subset_of(&original_perms)); - - // PROOF: no individual permission was gained - if !original_perms.allows(Permission::Read) { - assert!(!result.permissions().allows(Permission::Read)); - } - if !original_perms.allows(Permission::Write) { - assert!(!result.permissions().allows(Permission::Write)); - } - if !original_perms.allows(Permission::Execute) { - assert!(!result.permissions().allows(Permission::Execute)); - } - if !original_perms.allows(Permission::Delegate) { - assert!(!result.permissions().allows(Permission::Delegate)); - } - if !original_perms.allows(Permission::Revoke) { - assert!(!result.permissions().allows(Permission::Revoke)); - } - } - - #[kani::proof] - fn kernel_chained_delegate_never_escalates() { - let original_bits: u8 = kani::any(); - let restrict1_bits: u8 = kani::any(); - let restrict2_bits: u8 = kani::any(); - let ep_id: u16 = kani::any(); - kani::assume(ep_id < 256); - - let original_perms = PermissionSet::from_bits(original_bits); - kani::assume(original_perms.allows(Permission::Delegate)); - - let resource = Resource::Endpoint(EndpointId::from_raw(ep_id)); - - // Process A has the original cap - let mut table_a = CapabilityTable::new(); - let cap_a = Capability::new(resource.clone(), original_perms, Generation::initial()); - let slot_a = table_a.insert(cap_a); - kani::assume(slot_a.is_ok()); - let slot_a = slot_a.unwrap(); - - // A delegates to B - let cap = table_a.get(slot_a).unwrap(); - let perms_for_b = cap.permissions().restrict_to(&PermissionSet::from_bits(restrict1_bits)); - let mut table_b = CapabilityTable::new(); - let cap_b = Capability::new(resource.clone(), perms_for_b, Generation::initial()); - let slot_b = table_b.insert(cap_b); - kani::assume(slot_b.is_ok()); - let slot_b = slot_b.unwrap(); - - // B delegates to C (if B has Delegate permission) - let cap_in_b = table_b.get(slot_b).unwrap(); - if cap_in_b.permissions().allows(Permission::Delegate) { - let perms_for_c = cap_in_b.permissions().restrict_to(&PermissionSet::from_bits(restrict2_bits)); - let mut table_c = CapabilityTable::new(); - let cap_c = Capability::new(resource, perms_for_c, Generation::initial()); - let slot_c = table_c.insert(cap_c); - kani::assume(slot_c.is_ok()); - - let result = table_c.get(slot_c.unwrap()).unwrap(); - - // C's permissions are subset of B's - assert!(result.permissions().is_subset_of(cap_in_b.permissions())); - // C's permissions are subset of A's original - assert!(result.permissions().is_subset_of(&original_perms)); - } - } - - #[kani::proof] - fn kernel_delegate_rejects_without_delegate_permission() { - let source_bits: u8 = kani::any(); - let ep_id: u16 = kani::any(); - kani::assume(ep_id < 256); - - let source_perms = PermissionSet::from_bits(source_bits); - kani::assume(!source_perms.allows(Permission::Delegate)); - - let resource = Resource::Endpoint(EndpointId::from_raw(ep_id)); - let cap = Capability::new(resource, source_perms, Generation::initial()); - - let mut table = CapabilityTable::new(); - let slot = table.insert(cap); - kani::assume(slot.is_ok()); - let slot = slot.unwrap(); - - // This is what check_cap does: look up the cap and check permission - let retrieved = table.get(slot).unwrap(); - let has_delegate = retrieved.permissions().allows(Permission::Delegate); - - // The guard MUST reject: a cap inserted without Delegate - // permission is never retrievable with Delegate permission - assert!(!has_delegate); - } - - #[kani::proof] - fn kernel_check_cap_faithfully_reflects_stored_permissions() { - let bits: u8 = kani::any(); - let ep_id: u16 = kani::any(); - kani::assume(ep_id < 256); - - let perms = PermissionSet::from_bits(bits); - let resource = Resource::Endpoint(EndpointId::from_raw(ep_id)); - let cap = Capability::new(resource, perms, Generation::initial()); - - let mut table = CapabilityTable::new(); - let slot = table.insert(cap); - kani::assume(slot.is_ok()); - let slot = slot.unwrap(); - - let retrieved = table.get(slot).unwrap(); - - // check_cap checks allows(needed). Prove the table doesn't - // corrupt permissions: every permission check on the retrieved - // cap matches what was stored. - assert!(retrieved.permissions().allows(Permission::Read) == perms.allows(Permission::Read)); - assert!(retrieved.permissions().allows(Permission::Write) == perms.allows(Permission::Write)); - assert!(retrieved.permissions().allows(Permission::Execute) == perms.allows(Permission::Execute)); - assert!(retrieved.permissions().allows(Permission::Delegate) == perms.allows(Permission::Delegate)); - assert!(retrieved.permissions().allows(Permission::Revoke) == perms.allows(Permission::Revoke)); - } - - #[kani::proof] - fn grant_cap_preserves_resource_identity() { - let ep_id: u16 = kani::any(); - kani::assume(ep_id < 256); - let bits: u8 = kani::any(); - - let resource = Resource::Endpoint(EndpointId::from_raw(ep_id)); - let perms = PermissionSet::from_bits(bits); - let cap = Capability::new(resource.clone(), perms, Generation::initial()); - - let mut table = CapabilityTable::new(); - let slot = table.insert(cap); - kani::assume(slot.is_ok()); - - let retrieved = table.get(slot.unwrap()).unwrap(); - match retrieved.resource() { - Resource::Endpoint(id) => assert!(id.raw() == ep_id), - _ => panic!("resource type changed"), - } - } - - // --- Complete mediation: every resource-accessing syscall checks caps --- - - #[kani::proof] - fn handle_send_rejects_without_execute_permission() { - let bits: u8 = kani::any(); - let ep_id: u16 = kani::any(); - kani::assume(ep_id < 256); - - let perms = PermissionSet::from_bits(bits); - kani::assume(!perms.allows(Permission::Execute)); - - let resource = Resource::Endpoint(EndpointId::from_raw(ep_id)); - let cap = Capability::new(resource, perms, Generation::initial()); - - let mut table = CapabilityTable::new(); - let slot = table.insert(cap); - kani::assume(slot.is_ok()); - let slot = slot.unwrap(); - - let retrieved = table.get(slot).unwrap(); - assert!(!retrieved.permissions().allows(Permission::Execute)); - } - - #[kani::proof] - fn handle_receive_rejects_without_read_permission() { - let bits: u8 = kani::any(); - let ep_id: u16 = kani::any(); - kani::assume(ep_id < 256); - - let perms = PermissionSet::from_bits(bits); - kani::assume(!perms.allows(Permission::Read)); - - let resource = Resource::Endpoint(EndpointId::from_raw(ep_id)); - let cap = Capability::new(resource, perms, Generation::initial()); - - let mut table = CapabilityTable::new(); - let slot = table.insert(cap); - kani::assume(slot.is_ok()); - let slot = slot.unwrap(); - - let retrieved = table.get(slot).unwrap(); - assert!(!retrieved.permissions().allows(Permission::Read)); - } - - #[kani::proof] - fn missing_cap_always_rejected() { - let slot_val: u8 = kani::any(); - kani::assume(slot_val <= 63); - let slot = CapSlot::new(slot_val).unwrap(); - - let table = CapabilityTable::new(); - assert!(table.get(slot).is_err()); - } - - // --- Message delivery integrity --- - - #[kani::proof] - fn message_survives_pending_storage_roundtrip() { - let w0: usize = kani::any(); - let w1: usize = kani::any(); - let w2: usize = kani::any(); - let w3: usize = kani::any(); - - let original = Message::from_words([w0, w1, w2, w3]); - - let mut pending: [Option; 4] = [const { None }; 4]; - let idx: usize = kani::any(); - kani::assume(idx < 4); - - pending[idx] = Some(original); - - let retrieved = pending[idx].take(); - assert!(retrieved.is_some()); - - let msg = retrieved.unwrap(); - assert!(msg.word(0) == w0); - assert!(msg.word(1) == w1); - assert!(msg.word(2) == w2); - assert!(msg.word(3) == w3); - } - - #[kani::proof] - fn message_storage_does_not_cross_slots() { - let w_a: usize = kani::any(); - let w_b: usize = kani::any(); - kani::assume(w_a != w_b); - - let msg_a = Message::from_words([w_a, 0, 0, 0]); - let msg_b = Message::from_words([w_b, 0, 0, 0]); - - let mut pending: [Option; 4] = [const { None }; 4]; - pending[0] = Some(msg_a); - pending[1] = Some(msg_b); - - let retrieved_a = pending[0].take().unwrap(); - let retrieved_b = pending[1].take().unwrap(); - - assert!(retrieved_a.word(0) == w_a); - assert!(retrieved_b.word(0) == w_b); - } - - // --- Revocation completeness --- - - #[kani::proof] - fn revoke_invalidates_cap_slot() { - let bits: u8 = kani::any(); - let ep_id: u16 = kani::any(); - kani::assume(ep_id < 256); - - let perms = PermissionSet::from_bits(bits); - let cap = Capability::new( - Resource::Endpoint(EndpointId::from_raw(ep_id)), - perms, - Generation::initial(), - ); - - let mut table = CapabilityTable::new(); - let slot = table.insert(cap); - kani::assume(slot.is_ok()); - let slot = slot.unwrap(); - - assert!(table.get(slot).is_ok()); - table.remove(slot).unwrap(); - assert!(table.get(slot).is_err()); - } - - #[kani::proof] - fn revoke_does_not_affect_other_slots() { - let bits_a: u8 = kani::any(); - let bits_b: u8 = kani::any(); - - let cap_a = Capability::new( - Resource::ProcessCreate, - PermissionSet::from_bits(bits_a), - Generation::initial(), - ); - let cap_b = Capability::new( - Resource::Endpoint(EndpointId::from_raw(0)), - PermissionSet::from_bits(bits_b), - Generation::initial(), - ); - - let mut table = CapabilityTable::new(); - let slot_a = table.insert(cap_a); - let slot_b = table.insert(cap_b); - kani::assume(slot_a.is_ok() && slot_b.is_ok()); - let slot_a = slot_a.unwrap(); - let slot_b = slot_b.unwrap(); - - table.remove(slot_a).unwrap(); - - assert!(table.get(slot_a).is_err()); - assert!(table.get(slot_b).is_ok()); - assert!(*table.get(slot_b).unwrap().permissions() == PermissionSet::from_bits(bits_b)); - } -} diff --git a/crates/kernel/src/proofs/delegation.rs b/crates/kernel/src/proofs/delegation.rs new file mode 100644 index 0000000..596e9f2 --- /dev/null +++ b/crates/kernel/src/proofs/delegation.rs @@ -0,0 +1,95 @@ +use domain::capability::{Capability, CapabilityTable}; +use domain::resource::Resource; +use super::{arbitrary_endpoint_cap, insert_cap}; +use types::generation::Generation; +use types::id::EndpointId; +use types::permission::{Permission, PermissionSet}; + +#[kani::proof] +fn kernel_delegate_path_never_escalates() { + let source_bits: u8 = kani::any(); + let restrict_bits: u8 = kani::any(); + let ep_id: u16 = kani::any(); + kani::assume(ep_id < 256); + + let source_perms = PermissionSet::from_bits(source_bits); + kani::assume(source_perms.allows(Permission::Delegate)); + + let mut source_table = CapabilityTable::new(); + let slot = insert_cap(&mut source_table, arbitrary_endpoint_cap(source_bits, ep_id)); + + let cap = source_table.get(slot).unwrap(); + let original_perms = *cap.permissions(); + let restricted = original_perms.restrict_to(&PermissionSet::from_bits(restrict_bits)); + + let delegated = Capability::new( + cap.resource().clone(), + restricted, + Generation::initial(), + ); + + let mut target_table = CapabilityTable::new(); + let target_slot = insert_cap(&mut target_table, delegated); + + let result = target_table.get(target_slot).unwrap(); + assert!(result.permissions().is_subset_of(&original_perms)); + + if !original_perms.allows(Permission::Read) { assert!(!result.permissions().allows(Permission::Read)); } + if !original_perms.allows(Permission::Write) { assert!(!result.permissions().allows(Permission::Write)); } + if !original_perms.allows(Permission::Execute) { assert!(!result.permissions().allows(Permission::Execute)); } + if !original_perms.allows(Permission::Delegate) { assert!(!result.permissions().allows(Permission::Delegate)); } + if !original_perms.allows(Permission::Revoke) { assert!(!result.permissions().allows(Permission::Revoke)); } +} + +#[kani::proof] +fn kernel_chained_delegate_never_escalates() { + let original_bits: u8 = kani::any(); + let restrict1_bits: u8 = kani::any(); + let restrict2_bits: u8 = kani::any(); + let ep_id: u16 = kani::any(); + kani::assume(ep_id < 256); + + let original_perms = PermissionSet::from_bits(original_bits); + kani::assume(original_perms.allows(Permission::Delegate)); + + let resource = Resource::Endpoint(EndpointId::from_raw(ep_id)); + + let mut table_a = CapabilityTable::new(); + let slot_a = insert_cap(&mut table_a, arbitrary_endpoint_cap(original_bits, ep_id)); + + let cap = table_a.get(slot_a).unwrap(); + let perms_for_b = cap.permissions().restrict_to(&PermissionSet::from_bits(restrict1_bits)); + + let mut table_b = CapabilityTable::new(); + let cap_b = Capability::new(resource.clone(), perms_for_b, Generation::initial()); + let slot_b = insert_cap(&mut table_b, cap_b); + + let cap_in_b = table_b.get(slot_b).unwrap(); + if cap_in_b.permissions().allows(Permission::Delegate) { + let perms_for_c = cap_in_b.permissions().restrict_to(&PermissionSet::from_bits(restrict2_bits)); + + let mut table_c = CapabilityTable::new(); + let cap_c = Capability::new(resource, perms_for_c, Generation::initial()); + let slot_c = insert_cap(&mut table_c, cap_c); + + let result = table_c.get(slot_c).unwrap(); + assert!(result.permissions().is_subset_of(cap_in_b.permissions())); + assert!(result.permissions().is_subset_of(&original_perms)); + } +} + +#[kani::proof] +fn kernel_delegate_rejects_without_delegate_permission() { + let source_bits: u8 = kani::any(); + let ep_id: u16 = kani::any(); + kani::assume(ep_id < 256); + + let source_perms = PermissionSet::from_bits(source_bits); + kani::assume(!source_perms.allows(Permission::Delegate)); + + let mut table = CapabilityTable::new(); + let slot = insert_cap(&mut table, arbitrary_endpoint_cap(source_bits, ep_id)); + + let retrieved = table.get(slot).unwrap(); + assert!(!retrieved.permissions().allows(Permission::Delegate)); +} diff --git a/crates/kernel/src/proofs/mediation.rs b/crates/kernel/src/proofs/mediation.rs new file mode 100644 index 0000000..04be40c --- /dev/null +++ b/crates/kernel/src/proofs/mediation.rs @@ -0,0 +1,66 @@ +use domain::capability::CapabilityTable; +use super::{arbitrary_endpoint_cap, insert_cap}; +use types::bounded::CapSlot; +use types::permission::{Permission, PermissionSet}; + +#[kani::proof] +fn handle_send_rejects_without_execute_permission() { + let bits: u8 = kani::any(); + let ep_id: u16 = kani::any(); + kani::assume(ep_id < 256); + + let perms = PermissionSet::from_bits(bits); + kani::assume(!perms.allows(Permission::Execute)); + + let mut table = CapabilityTable::new(); + let slot = insert_cap(&mut table, arbitrary_endpoint_cap(bits, ep_id)); + + let retrieved = table.get(slot).unwrap(); + assert!(!retrieved.permissions().allows(Permission::Execute)); +} + +#[kani::proof] +fn handle_receive_rejects_without_read_permission() { + let bits: u8 = kani::any(); + let ep_id: u16 = kani::any(); + kani::assume(ep_id < 256); + + let perms = PermissionSet::from_bits(bits); + kani::assume(!perms.allows(Permission::Read)); + + let mut table = CapabilityTable::new(); + let slot = insert_cap(&mut table, arbitrary_endpoint_cap(bits, ep_id)); + + let retrieved = table.get(slot).unwrap(); + assert!(!retrieved.permissions().allows(Permission::Read)); +} + +#[kani::proof] +fn missing_cap_always_rejected() { + let slot_val: u8 = kani::any(); + kani::assume(slot_val <= 63); + let slot = CapSlot::new(slot_val).unwrap(); + + let table = CapabilityTable::new(); + assert!(table.get(slot).is_err()); +} + +#[kani::proof] +fn check_cap_faithfully_reflects_stored_permissions() { + let bits: u8 = kani::any(); + let ep_id: u16 = kani::any(); + kani::assume(ep_id < 256); + + let perms = PermissionSet::from_bits(bits); + + let mut table = CapabilityTable::new(); + let slot = insert_cap(&mut table, arbitrary_endpoint_cap(bits, ep_id)); + + let retrieved = table.get(slot).unwrap(); + + assert!(retrieved.permissions().allows(Permission::Read) == perms.allows(Permission::Read)); + assert!(retrieved.permissions().allows(Permission::Write) == perms.allows(Permission::Write)); + assert!(retrieved.permissions().allows(Permission::Execute) == perms.allows(Permission::Execute)); + assert!(retrieved.permissions().allows(Permission::Delegate) == perms.allows(Permission::Delegate)); + assert!(retrieved.permissions().allows(Permission::Revoke) == perms.allows(Permission::Revoke)); +} diff --git a/crates/kernel/src/proofs/message.rs b/crates/kernel/src/proofs/message.rs new file mode 100644 index 0000000..278b2a3 --- /dev/null +++ b/crates/kernel/src/proofs/message.rs @@ -0,0 +1,46 @@ +use domain::message::Message; + +#[kani::proof] +fn message_survives_pending_storage_roundtrip() { + let w0: usize = kani::any(); + let w1: usize = kani::any(); + let w2: usize = kani::any(); + let w3: usize = kani::any(); + + let original = Message::from_words([w0, w1, w2, w3]); + + let mut pending: [Option; 4] = [const { None }; 4]; + let idx: usize = kani::any(); + kani::assume(idx < 4); + + pending[idx] = Some(original); + + let retrieved = pending[idx].take(); + assert!(retrieved.is_some()); + + let msg = retrieved.unwrap(); + assert!(msg.word(0) == w0); + assert!(msg.word(1) == w1); + assert!(msg.word(2) == w2); + assert!(msg.word(3) == w3); +} + +#[kani::proof] +fn message_storage_does_not_cross_slots() { + let w_a: usize = kani::any(); + let w_b: usize = kani::any(); + kani::assume(w_a != w_b); + + let msg_a = Message::from_words([w_a, 0, 0, 0]); + let msg_b = Message::from_words([w_b, 0, 0, 0]); + + let mut pending: [Option; 4] = [const { None }; 4]; + pending[0] = Some(msg_a); + pending[1] = Some(msg_b); + + let retrieved_a = pending[0].take().unwrap(); + let retrieved_b = pending[1].take().unwrap(); + + assert!(retrieved_a.word(0) == w_a); + assert!(retrieved_b.word(0) == w_b); +} diff --git a/crates/kernel/src/proofs/mod.rs b/crates/kernel/src/proofs/mod.rs new file mode 100644 index 0000000..a3551d3 --- /dev/null +++ b/crates/kernel/src/proofs/mod.rs @@ -0,0 +1,25 @@ +mod delegation; +mod mediation; +mod message; +mod revocation; + +use domain::capability::{Capability, CapabilityTable}; +use domain::resource::Resource; +use types::bounded::CapSlot; +use types::generation::Generation; +use types::id::EndpointId; +use types::permission::PermissionSet; + +fn arbitrary_endpoint_cap(bits: u8, ep_id: u16) -> Capability { + Capability::new( + Resource::Endpoint(EndpointId::from_raw(ep_id)), + PermissionSet::from_bits(bits), + Generation::initial(), + ) +} + +fn insert_cap(table: &mut CapabilityTable, cap: Capability) -> CapSlot { + let slot = table.insert(cap); + kani::assume(slot.is_ok()); + slot.unwrap() +} diff --git a/crates/kernel/src/proofs/revocation.rs b/crates/kernel/src/proofs/revocation.rs new file mode 100644 index 0000000..2169d11 --- /dev/null +++ b/crates/kernel/src/proofs/revocation.rs @@ -0,0 +1,63 @@ +use domain::capability::{Capability, CapabilityTable}; +use domain::resource::Resource; +use super::{arbitrary_endpoint_cap, insert_cap}; +use types::generation::Generation; +use types::id::EndpointId; +use types::permission::PermissionSet; + +#[kani::proof] +fn revoke_invalidates_cap_slot() { + let bits: u8 = kani::any(); + let ep_id: u16 = kani::any(); + kani::assume(ep_id < 256); + + let mut table = CapabilityTable::new(); + let slot = insert_cap(&mut table, arbitrary_endpoint_cap(bits, ep_id)); + + assert!(table.get(slot).is_ok()); + table.remove(slot).unwrap(); + assert!(table.get(slot).is_err()); +} + +#[kani::proof] +fn revoke_does_not_affect_other_slots() { + let bits_a: u8 = kani::any(); + let bits_b: u8 = kani::any(); + + let cap_a = Capability::new( + Resource::ProcessCreate, + PermissionSet::from_bits(bits_a), + Generation::initial(), + ); + let cap_b = Capability::new( + Resource::Endpoint(EndpointId::from_raw(0)), + PermissionSet::from_bits(bits_b), + Generation::initial(), + ); + + let mut table = CapabilityTable::new(); + let slot_a = insert_cap(&mut table, cap_a); + let slot_b = insert_cap(&mut table, cap_b); + + table.remove(slot_a).unwrap(); + + assert!(table.get(slot_a).is_err()); + assert!(table.get(slot_b).is_ok()); + assert!(*table.get(slot_b).unwrap().permissions() == PermissionSet::from_bits(bits_b)); +} + +#[kani::proof] +fn grant_cap_preserves_resource_identity() { + let ep_id: u16 = kani::any(); + kani::assume(ep_id < 256); + let bits: u8 = kani::any(); + + let mut table = CapabilityTable::new(); + let slot = insert_cap(&mut table, arbitrary_endpoint_cap(bits, ep_id)); + + let retrieved = table.get(slot).unwrap(); + match retrieved.resource() { + Resource::Endpoint(id) => assert!(id.raw() == ep_id), + _ => panic!("resource type changed"), + } +} diff --git a/crates/types/src/proofs.rs b/crates/types/src/proofs.rs deleted file mode 100644 index 4d43345..0000000 --- a/crates/types/src/proofs.rs +++ /dev/null @@ -1,83 +0,0 @@ -#[cfg(kani)] -mod kani_proofs { - use crate::bounded::{CapSlot, PageCount, Priority}; - use crate::generation::Generation; - use crate::permission::PermissionSet; - - #[kani::proof] - fn restrict_to_never_escalates() { - let a: u8 = kani::any(); - let b: u8 = kani::any(); - - let original = PermissionSet::from_bits(a); - let restrictor = PermissionSet::from_bits(b); - let result = original.restrict_to(&restrictor); - - assert!(result.is_subset_of(&original)); - assert!(result.is_subset_of(&restrictor)); - } - - #[kani::proof] - fn restrict_to_is_commutative_in_result() { - let a: u8 = kani::any(); - let b: u8 = kani::any(); - - let set_a = PermissionSet::from_bits(a); - let set_b = PermissionSet::from_bits(b); - - let ab = set_a.restrict_to(&set_b); - let ba = set_b.restrict_to(&set_a); - - assert!(ab == ba); - } - - #[kani::proof] - fn empty_permission_set_restricts_everything_to_empty() { - let a: u8 = kani::any(); - let set = PermissionSet::from_bits(a); - let empty = PermissionSet::empty(); - - let result = set.restrict_to(&empty); - assert!(result == empty); - } - - #[kani::proof] - fn generation_next_always_invalidates() { - let value: u32 = kani::any(); - let current = Generation::from_raw(value); - let next = current.next(); - - assert!(!current.is_valid_against(&next)); - } - - #[kani::proof] - fn capslot_always_valid_index() { - let value: u8 = kani::any(); - if let Some(slot) = CapSlot::new(value) { - assert!(slot.value() <= 63); - } - } - - #[kani::proof] - fn capslot_rejects_out_of_range() { - let value: u8 = kani::any(); - kani::assume(value > 63); - assert!(CapSlot::new(value).is_none()); - } - - #[kani::proof] - fn priority_always_fits_in_bitmap() { - let value: u8 = kani::any(); - if let Some(prio) = Priority::new(value) { - assert!((prio.value() as u32) < 32); - } - } - - #[kani::proof] - fn page_count_is_always_nonzero() { - let value: u16 = kani::any(); - if let Some(count) = PageCount::new(value) { - assert!(count.value() >= 1); - } - } -} diff --git a/crates/types/src/proofs/bounded.rs b/crates/types/src/proofs/bounded.rs new file mode 100644 index 0000000..99b15a3 --- /dev/null +++ b/crates/types/src/proofs/bounded.rs @@ -0,0 +1,32 @@ +use crate::bounded::{CapSlot, PageCount, Priority}; + +#[kani::proof] +fn capslot_always_valid_index() { + let value: u8 = kani::any(); + if let Some(slot) = CapSlot::new(value) { + assert!(slot.value() <= 63); + } +} + +#[kani::proof] +fn capslot_rejects_out_of_range() { + let value: u8 = kani::any(); + kani::assume(value > 63); + assert!(CapSlot::new(value).is_none()); +} + +#[kani::proof] +fn priority_always_fits_in_bitmap() { + let value: u8 = kani::any(); + if let Some(prio) = Priority::new(value) { + assert!((prio.value() as u32) < 32); + } +} + +#[kani::proof] +fn page_count_is_always_nonzero() { + let value: u16 = kani::any(); + if let Some(count) = PageCount::new(value) { + assert!(count.value() >= 1); + } +} diff --git a/crates/types/src/proofs/generation.rs b/crates/types/src/proofs/generation.rs new file mode 100644 index 0000000..beab2e2 --- /dev/null +++ b/crates/types/src/proofs/generation.rs @@ -0,0 +1,10 @@ +use crate::generation::Generation; + +#[kani::proof] +fn generation_next_always_invalidates() { + let value: u32 = kani::any(); + let current = Generation::from_raw(value); + let next = current.next(); + + assert!(!current.is_valid_against(&next)); +} diff --git a/crates/types/src/proofs/mod.rs b/crates/types/src/proofs/mod.rs new file mode 100644 index 0000000..4d45d1f --- /dev/null +++ b/crates/types/src/proofs/mod.rs @@ -0,0 +1,3 @@ +mod bounded; +mod generation; +mod permissions; diff --git a/crates/types/src/proofs/permissions.rs b/crates/types/src/proofs/permissions.rs new file mode 100644 index 0000000..8aa90cc --- /dev/null +++ b/crates/types/src/proofs/permissions.rs @@ -0,0 +1,38 @@ +use crate::permission::PermissionSet; + +#[kani::proof] +fn restrict_to_never_escalates() { + let a: u8 = kani::any(); + let b: u8 = kani::any(); + + let original = PermissionSet::from_bits(a); + let restrictor = PermissionSet::from_bits(b); + let result = original.restrict_to(&restrictor); + + assert!(result.is_subset_of(&original)); + assert!(result.is_subset_of(&restrictor)); +} + +#[kani::proof] +fn restrict_to_is_commutative_in_result() { + let a: u8 = kani::any(); + let b: u8 = kani::any(); + + let set_a = PermissionSet::from_bits(a); + let set_b = PermissionSet::from_bits(b); + + let ab = set_a.restrict_to(&set_b); + let ba = set_b.restrict_to(&set_a); + + assert!(ab == ba); +} + +#[kani::proof] +fn empty_permission_set_restricts_everything_to_empty() { + let a: u8 = kani::any(); + let set = PermissionSet::from_bits(a); + let empty = PermissionSet::empty(); + + let result = set.restrict_to(&empty); + assert!(result == empty); +}