feat(kernel): object lifetimes via slot generations
- SlotGenerations per table, never wraps, retires exhausted slots - caps to dead/reused process, endpoint, region rejected - endpoints owned, die w/ owner, waiters woken w/ error - DropCap syscall + libkos wrapper - irq table bounds-checked, routes dropped w/ thread - self-kill terminates caller, exit_thread full cleanup - sched run_now: switch to named thread, not queue head - lifetime tests, fuzz kills/recreates, kani gen proofs
This commit is contained in:
@@ -6,15 +6,22 @@ impl Generation {
|
||||
Self(0)
|
||||
}
|
||||
|
||||
pub fn next(&self) -> Self {
|
||||
Self(self.0.wrapping_add(1))
|
||||
/// The following generation, or `None` once the counter is exhausted.
|
||||
/// Never wraps: a wrapped counter would make stale capabilities valid.
|
||||
pub fn next(&self) -> Option<Self> {
|
||||
self.0.checked_add(1).map(Self)
|
||||
}
|
||||
|
||||
pub fn raw(&self) -> u32 {
|
||||
self.0
|
||||
}
|
||||
|
||||
pub fn is_valid_against(&self, current: &Generation) -> bool {
|
||||
self == current
|
||||
}
|
||||
|
||||
#[cfg(kani)]
|
||||
/// Only kernel code builds capabilities, so exposing this cannot
|
||||
/// forge one; it exists for tests and proofs.
|
||||
pub fn from_raw(value: u32) -> Self {
|
||||
Self(value)
|
||||
}
|
||||
|
||||
@@ -1,10 +1,17 @@
|
||||
use crate::generation::Generation;
|
||||
|
||||
/// Generations only ever increase, so a capability minted for an earlier
|
||||
/// generation can never match again. (The old wrapping counter returned to
|
||||
/// earlier values after 2^32 bumps.)
|
||||
#[kani::proof]
|
||||
fn generation_next_always_invalidates() {
|
||||
fn generation_next_is_strictly_greater_or_exhausted() {
|
||||
let value: u32 = kani::any();
|
||||
let current = Generation::from_raw(value);
|
||||
let next = current.next();
|
||||
|
||||
assert!(!current.is_valid_against(&next));
|
||||
match current.next() {
|
||||
Some(next) => {
|
||||
assert!(next.raw() > current.raw());
|
||||
assert!(!current.is_valid_against(&next));
|
||||
}
|
||||
None => assert!(value == u32::MAX),
|
||||
}
|
||||
}
|
||||
|
||||
@@ -20,3 +20,4 @@ pub const SYS_CREATE_ENDPOINT: usize = 18;
|
||||
pub const SYS_DEBUG_PUTCHAR: usize = 19;
|
||||
pub const SYS_MAP_PAGE: usize = 20;
|
||||
pub const SYS_SPAWN_THREAD_IN: usize = 21;
|
||||
pub const SYS_DROP_CAP: usize = 22;
|
||||
|
||||
Reference in New Issue
Block a user