GKaszewski/k-os
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

refactor(proofs): split into per-topic modules with shared helpers across types, domain, and kernel

Browse Source
This commit is contained in:
Gabriel Kaszewski
2026-10-18 01:08:05 +02:00
parent e5fd6372b3
commit 71518a93a4
16 changed files with 554 additions and 607 deletions
Download Patch File Download Diff File Expand all files Collapse all files

184
crates/domain/src/proofs.rs
View File

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

37
crates/domain/src/proofs/capability.rs Normal file
View File

@@ -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());
}

66
crates/domain/src/proofs/delegation.rs Normal file
View File

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

23
crates/domain/src/proofs/mod.rs Normal file
View File

@@ -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()
}

50
crates/domain/src/proofs/thread.rs Normal file
View File

@@ -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());
}

340
crates/kernel/src/proofs.rs
View File

@@ -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<Message>; 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<Message>; 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));
}
}

95
crates/kernel/src/proofs/delegation.rs Normal file
View File

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

66
crates/kernel/src/proofs/mediation.rs Normal file
View File

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

46
crates/kernel/src/proofs/message.rs Normal file
View File

@@ -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<Message>; 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<Message>; 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);
}

25
crates/kernel/src/proofs/mod.rs Normal file
View File

@@ -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()
}

63
crates/kernel/src/proofs/revocation.rs Normal file
View File

@@ -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"),
}
}

83
crates/types/src/proofs.rs
View File

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

32
crates/types/src/proofs/bounded.rs Normal file
View File

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

10
crates/types/src/proofs/generation.rs Normal file
View File

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

3
crates/types/src/proofs/mod.rs Normal file
View File

@@ -0,0 +1,3 @@
mod bounded;
mod generation;
mod permissions;

38
crates/types/src/proofs/permissions.rs Normal file
View File

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