feat(kernel): derivation-tree revocation, region caps

- caps record parent (mint/delegate/ipc), CapRef w/ pid+slot gens
- Revoke = delete subtree, keep self; drop/death re-parents children
- CreateRegion/MapRegion; mapping lives only as long as its cap
- drop Permission::Revoke + object-wide revoke
- mint any cap (badge only ep/ntfn), process caps delegable
- kani: descendants == subtree; model-based fuzz vs spec
This commit is contained in:
2026-10-26 20:41:03 +01:00
parent 76f10ff1f1
commit 154599e3af
32 changed files with 1302 additions and 239 deletions

View File

@@ -6,6 +6,7 @@ use types::address::{EntryPoint, StackPointer, VirtualAddress};
use types::badge::Badge;
use types::bounded::{CapSlot, PageCount};
use types::id::ProcessId;
use types::mapping::PagePerms;
use types::permission::PermissionSet;
use types::syscall_abi::*;
use types::time::Ticks;
@@ -180,6 +181,30 @@ pub fn map_page(
.is_ok()
}
/// Allocates `pages` of physically contiguous shared memory, charged to
/// this process, and returns a capability to it.
pub fn create_region(pages: PageCount) -> Result<CapSlot> {
slot_of(raw(
SYS_CREATE_REGION,
[pages.value() as usize, 0, 0, 0, 0, 0],
))
}
/// Maps the region behind `region` at `va`. The mapping lasts as long as
/// the capability: dropping or having it revoked unmaps it.
pub fn map_region(region: CapSlot, va: VirtualAddress, perms: PagePerms) -> Result<()> {
let perms = match perms {
PagePerms::ReadOnly => PERMS_READ_ONLY,
PagePerms::ReadWrite => PERMS_READ_WRITE,
PagePerms::ReadExecute => PERMS_READ_EXECUTE,
};
raw(
SYS_MAP_REGION,
[region.value() as usize, va.raw(), perms, 0, 0, 0],
)
.map(|_| ())
}
// ---- capabilities ----
pub fn delegate(slot: CapSlot, to: CapSlot, permissions: PermissionSet) -> bool {
@@ -213,6 +238,8 @@ pub fn mint(slot: CapSlot, badge: Badge, permissions: PermissionSet) -> Result<C
))
}
/// Deletes every capability derived from `slot` (in any process) and keeps
/// `slot` itself.
pub fn revoke(slot: CapSlot) -> bool {
raw(SYS_REVOKE, [slot.value() as usize, 0, 0, 0, 0, 0]).is_ok()
}