Struct Authorized 

pub struct Authorized { /* private fields */ }

Authorization witness carrying all proofs required for a host call.

Corresponds to Lean: structure Authorized (s : State) (a : Action)

In Lean, this structure contains proofs that cannot be forged. In Rust, we validate these conditions at runtime.

TOCTTOU Prevention: The Authorized witness is ONLY constructible via validate_atomic() which both validates AND returns the witness in a single atomic operation. This prevents the vulnerability where:

1. Check capability validity
2. (capability revoked here)
3. Use capability

By making construction private and combining validation with use, we ensure authorization is always checked against the CURRENT state at the moment of execution.

Design rationale:

• h_cap: Capability matches the action
• h_pol: Policy permits the action
• h_valid: Capability chain is valid
• h_live: Target resource is live
• h_conf: Rights are confined
• h_biba: Biba integrity constraint for writes

Implementations

impl Authorized

pub fn validate_atomic( state: &State, cap: Capability, action: Action, ctx: PolicyContext, ) -> Result<Authorized, AuthorizationError>

Atomically validate and create an authorization witness.

TOCTTOU Prevention: This function validates ALL authorization conditions and returns the witness in a single atomic operation. The returned witness is ONLY valid for the state it was validated against.

Corresponds to Lean: constructing Authorized s a requires proofs for state s.

Arguments

• state - The CURRENT state to validate against
• cap - The capability to use
• action - The action to authorize
• ctx - Policy evaluation context

Errors

Returns AuthorizationError::HolderMismatch if the capability holder does not match the action subject. Returns AuthorizationError::TargetMismatch if the capability target does not match the action target. Returns AuthorizationError::InsufficientRights if the action requests rights not granted by the capability. Returns AuthorizationError::CapabilityNotHeld if the plugin does not hold the capability. Returns AuthorizationError::PolicyDenied if the policy does not permit the action. Returns AuthorizationError::CapabilityNotFound if the capability is not in the revocation table. Returns AuthorizationError::CapabilityRevoked if the capability or its parent is revoked. Returns AuthorizationError::ResourceNotLive if the target resource is not live. Returns AuthorizationError::BibaViolation if a write violates Biba integrity.

pub fn cap(&self) -> &Capability

Get the capability (read-only access)

pub fn action(&self) -> &Action

Get the action (read-only access)

pub fn ctx(&self) -> &PolicyContext

Get the policy context (read-only access)

pub fn cap_id(&self) -> CapId

Get the capability ID being used

pub fn holder_has_cap(&self, state: &State) -> bool

Check if holder has the capability (theorem correspondence)

Corresponds to Lean: theorem Authorized.holder_has_cap

pub fn policy_permitted(&self, state: &State) -> bool

Check if policy is permitted (theorem correspondence)

Corresponds to Lean: theorem Authorized.policy_permitted

pub fn rights_confined(&self) -> bool

Check if rights are confined (theorem correspondence)

Corresponds to Lean: theorem Authorized.rights_confined

pub fn biba_satisfied(&self, state: &State) -> bool

Check if Biba is satisfied (theorem correspondence)

Corresponds to Lean: theorem Authorized.biba_satisfied

Trait Implementations

impl Clone for Authorized

fn clone(&self) -> Authorized

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for Authorized

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.