139 lines
3.9 KiB
Rust
139 lines
3.9 KiB
Rust
use domain::capability::{Capability, CapabilityTable};
|
|
use domain::endpoint::Endpoint;
|
|
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 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"),
|
|
}
|
|
}
|
|
|
|
#[kani::proof]
|
|
fn generation_revocation_invalidates_all_caps() {
|
|
let bits: u8 = kani::any();
|
|
let ep_id: u16 = kani::any();
|
|
kani::assume(ep_id < 256);
|
|
|
|
let mut endpoint = Endpoint::new(EndpointId::from_raw(ep_id));
|
|
let original_gen = *endpoint.generation();
|
|
|
|
let cap = Capability::new(
|
|
Resource::Endpoint(EndpointId::from_raw(ep_id)),
|
|
PermissionSet::from_bits(bits),
|
|
original_gen,
|
|
);
|
|
|
|
let mut table = CapabilityTable::new();
|
|
let slot = insert_cap(&mut table, cap);
|
|
|
|
assert!(table.get(slot).unwrap().generation().is_valid_against(&original_gen));
|
|
|
|
endpoint.revoke();
|
|
let new_gen = *endpoint.generation();
|
|
|
|
assert!(!table.get(slot).unwrap().generation().is_valid_against(&new_gen));
|
|
}
|
|
|
|
#[kani::proof]
|
|
fn cap_created_after_revoke_is_valid() {
|
|
let ep_id: u16 = kani::any();
|
|
kani::assume(ep_id < 256);
|
|
let bits: u8 = kani::any();
|
|
|
|
let mut endpoint = Endpoint::new(EndpointId::from_raw(ep_id));
|
|
endpoint.revoke();
|
|
let current_gen = *endpoint.generation();
|
|
|
|
let cap = Capability::new(
|
|
Resource::Endpoint(EndpointId::from_raw(ep_id)),
|
|
PermissionSet::from_bits(bits),
|
|
current_gen,
|
|
);
|
|
|
|
assert!(cap.generation().is_valid_against(¤t_gen));
|
|
}
|
|
|
|
#[kani::proof]
|
|
fn multiple_revocations_invalidate_all_prior_caps() {
|
|
let ep_id: u16 = kani::any();
|
|
kani::assume(ep_id < 256);
|
|
|
|
let mut endpoint = Endpoint::new(EndpointId::from_raw(ep_id));
|
|
|
|
let gen0 = *endpoint.generation();
|
|
let cap0 = Capability::new(
|
|
Resource::Endpoint(EndpointId::from_raw(ep_id)),
|
|
PermissionSet::empty().with(Permission::Read),
|
|
gen0,
|
|
);
|
|
|
|
endpoint.revoke();
|
|
let gen1 = *endpoint.generation();
|
|
let cap1 = Capability::new(
|
|
Resource::Endpoint(EndpointId::from_raw(ep_id)),
|
|
PermissionSet::empty().with(Permission::Read),
|
|
gen1,
|
|
);
|
|
|
|
endpoint.revoke();
|
|
let gen2 = *endpoint.generation();
|
|
|
|
assert!(!cap0.generation().is_valid_against(&gen2));
|
|
assert!(!cap1.generation().is_valid_against(&gen2));
|
|
}
|