Skip to main content

lion_core/step/
authorization.rs

1// Copyright (C) 2026 HaiyangLi
2// SPDX-License-Identifier: AGPL-3.0-or-later
3//! Lion Step Authorization
4//!
5//! Corresponds to: Lion/Step/Authorization.lean
6//!
7//! Authorization witness for proof-carrying steps.
8//! Bakes complete mediation into the type system.
9
10use crate::state::State;
11use crate::types::{Action, CapId, Capability, MemAddr, PolicyContext, Right, SecurityLevel};
12
13/// Error type for authorization failures
14#[derive(Debug, Clone, PartialEq, Eq)]
15pub enum AuthorizationError {
16    /// Capability not found in kernel
17    CapabilityNotFound(CapId),
18    /// Capability is revoked
19    CapabilityRevoked(CapId),
20    /// Capability holder mismatch
21    HolderMismatch {
22        /// Expected holder plugin ID
23        expected: u128,
24        /// Actual holder plugin ID
25        actual: u128,
26    },
27    /// Capability target mismatch
28    TargetMismatch {
29        /// Expected target resource ID
30        expected: u128,
31        /// Actual target resource ID
32        actual: u128,
33    },
34    /// Insufficient rights
35    InsufficientRights,
36    /// Policy denied the action
37    PolicyDenied,
38    /// Target resource not live
39    ResourceNotLive(MemAddr),
40    /// Biba integrity violation (write-up)
41    BibaViolation {
42        /// Security level of the writing plugin
43        writer_level: SecurityLevel,
44        /// Security level of the target resource
45        target_level: SecurityLevel,
46    },
47    /// Capability not held by plugin
48    CapabilityNotHeld(CapId),
49}
50
51impl std::fmt::Display for AuthorizationError {
52    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
53        match self {
54            AuthorizationError::CapabilityNotFound(id) => {
55                write!(f, "Capability {id} not found")
56            }
57            AuthorizationError::CapabilityRevoked(id) => {
58                write!(f, "Capability {id} is revoked")
59            }
60            AuthorizationError::HolderMismatch { expected, actual } => {
61                write!(f, "Holder mismatch: expected {expected}, got {actual}")
62            }
63            AuthorizationError::TargetMismatch { expected, actual } => {
64                write!(f, "Target mismatch: expected {expected}, got {actual}")
65            }
66            AuthorizationError::InsufficientRights => {
67                write!(f, "Insufficient rights")
68            }
69            AuthorizationError::PolicyDenied => {
70                write!(f, "Policy denied the action")
71            }
72            AuthorizationError::ResourceNotLive(addr) => {
73                write!(f, "Resource at {addr} is not live")
74            }
75            AuthorizationError::BibaViolation {
76                writer_level,
77                target_level,
78            } => {
79                write!(
80                    f,
81                    "Biba violation: writer level {writer_level:?} cannot write to target level {target_level:?}"
82                )
83            }
84            AuthorizationError::CapabilityNotHeld(id) => {
85                write!(f, "Capability {id} not held by plugin")
86            }
87        }
88    }
89}
90
91impl std::error::Error for AuthorizationError {}
92
93/// Resource integrity level based on owner.
94///
95/// Corresponds to Lean: `def resource_integrity`
96///
97/// Used for Biba "no write-up" enforcement.
98pub fn resource_integrity(state: &State, rid: MemAddr) -> SecurityLevel {
99    // Check if resource is allocated and get owner
100    if let Some(status) = state.ghost().get_status(rid) {
101        if let Some(owner) = status.owner() {
102            state.plugin_level(owner).unwrap_or(SecurityLevel::Public)
103        } else {
104            SecurityLevel::Public
105        }
106    } else {
107        // Unallocated/freed has no integrity
108        SecurityLevel::Public
109    }
110}
111
112/// Biba write check: writer's integrity level must dominate target's.
113///
114/// Corresponds to Lean: `def biba_write_ok`
115///
116/// This is the Biba "no write-up" enforcement for resource modification.
117pub fn biba_write_ok(state: &State, action: &Action) -> bool {
118    // If Write right is not requested, Biba is satisfied
119    if !action.rights.contains(Right::Write) {
120        return true;
121    }
122
123    let writer_level = state
124        .plugin_level(action.subject)
125        .unwrap_or(SecurityLevel::Public);
126    // action.target is ResourceId (u128); ghost uses MemAddr (u64) — truncate for address lookup
127    let target_level = resource_integrity(state, action.target as MemAddr);
128
129    writer_level >= target_level
130}
131
132/// Check capability seal and revocation status.
133///
134/// Corresponds to Lean: `def cap_isValid`
135#[allow(dead_code)] // Lean correspondence
136pub fn cap_is_valid(state: &State, cap: &Capability) -> bool {
137    // Check capability is not revoked
138    state.kernel().revocation().is_valid(cap.id())
139    // Note: seal verification would be done here with HMAC
140    // For now we assume seal is valid if in kernel table
141}
142
143/// Full capability check for authorization.
144///
145/// Corresponds to Lean: `def capability_check`
146#[allow(dead_code)] // Lean correspondence
147pub fn capability_check(state: &State, action: &Action, cap: &Capability) -> bool {
148    // 1. Holder matches subject
149    if cap.holder() != action.subject {
150        return false;
151    }
152
153    // 2. Target matches
154    if cap.target() != action.target {
155        return false;
156    }
157
158    // 3. Rights are sufficient
159    if !action.rights.is_subset_of(cap.rights()) {
160        return false;
161    }
162
163    // 4. Capability is valid (not revoked)
164    if !cap_is_valid(state, cap) {
165        return false;
166    }
167
168    // 5. Plugin holds the capability
169    if !state.plugin_holds(action.subject, cap.id()) {
170        return false;
171    }
172
173    true
174}
175
176/// Authorization witness carrying all proofs required for a host call.
177///
178/// Corresponds to Lean: `structure Authorized (s : State) (a : Action)`
179///
180/// In Lean, this structure contains proofs that cannot be forged.
181/// In Rust, we validate these conditions at runtime.
182///
183/// **TOCTTOU Prevention**:
184/// The Authorized witness is ONLY constructible via `validate_atomic()` which
185/// both validates AND returns the witness in a single atomic operation.
186/// This prevents the vulnerability where:
187///   1. Check capability validity
188///   2. (capability revoked here)
189///   3. Use capability
190///
191/// By making construction private and combining validation with use,
192/// we ensure authorization is always checked against the CURRENT state
193/// at the moment of execution.
194///
195/// Design rationale:
196/// - h_cap: Capability matches the action
197/// - h_pol: Policy permits the action
198/// - h_valid: Capability chain is valid
199/// - h_live: Target resource is live
200/// - h_conf: Rights are confined
201/// - h_biba: Biba integrity constraint for writes
202#[derive(Debug, Clone)]
203#[must_use = "authorization tokens must be consumed to enforce access control"]
204pub struct Authorized {
205    /// The capability being used
206    cap: Capability,
207
208    /// The action being authorized
209    action: Action,
210
211    /// Policy evaluation context
212    ctx: PolicyContext,
213
214    /// Marker to prevent external construction
215    /// This ensures Authorized can only be created via validate_atomic()
216    _private: (),
217}
218
219impl Authorized {
220    /// Create a new authorization witness (INTERNAL ONLY)
221    ///
222    /// This constructor is private to enforce atomic validation.
223    /// External code must use `validate_atomic()` to obtain an Authorized witness.
224    fn new_internal(cap: Capability, action: Action, ctx: PolicyContext) -> Self {
225        Authorized {
226            cap,
227            action,
228            ctx,
229            _private: (),
230        }
231    }
232
233    /// Atomically validate and create an authorization witness.
234    ///
235    /// **TOCTTOU Prevention**: This function validates ALL authorization conditions
236    /// and returns the witness in a single atomic operation. The returned witness
237    /// is ONLY valid for the state it was validated against.
238    ///
239    /// Corresponds to Lean: constructing `Authorized s a` requires proofs for state `s`.
240    ///
241    /// # Arguments
242    /// * `state` - The CURRENT state to validate against
243    /// * `cap` - The capability to use
244    /// * `action` - The action to authorize
245    /// * `ctx` - Policy evaluation context
246    ///
247    /// # Errors
248    ///
249    /// Returns `AuthorizationError::HolderMismatch` if the capability holder does not match the action subject.
250    /// Returns `AuthorizationError::TargetMismatch` if the capability target does not match the action target.
251    /// Returns `AuthorizationError::InsufficientRights` if the action requests rights not granted by the capability.
252    /// Returns `AuthorizationError::CapabilityNotHeld` if the plugin does not hold the capability.
253    /// Returns `AuthorizationError::PolicyDenied` if the policy does not permit the action.
254    /// Returns `AuthorizationError::CapabilityNotFound` if the capability is not in the revocation table.
255    /// Returns `AuthorizationError::CapabilityRevoked` if the capability or its parent is revoked.
256    /// Returns `AuthorizationError::ResourceNotLive` if the target resource is not live.
257    /// Returns `AuthorizationError::BibaViolation` if a write violates Biba integrity.
258    pub fn validate_atomic(
259        state: &State,
260        cap: Capability,
261        action: Action,
262        ctx: PolicyContext,
263    ) -> Result<Authorized, AuthorizationError> {
264        // Create provisional witness for validation
265        let provisional = Self::new_internal(cap, action, ctx);
266
267        // Validate all conditions atomically
268        // If ANY check fails, no witness is returned
269        provisional.check_capability(state)?;
270        provisional.check_policy(state)?;
271        provisional.check_validity(state)?;
272        provisional.check_liveness(state)?;
273        provisional.check_confinement()?;
274        provisional.check_biba(state)?;
275
276        // All checks passed - return the valid witness
277        Ok(provisional)
278    }
279
280    /// Validate all authorization conditions (internal use only)
281    ///
282    /// This is used for re-validation when needed but should NOT be the
283    /// primary mechanism for obtaining authorization.
284    ///
285    /// This checks all the conditions that would be baked into
286    /// the Lean `Authorized` structure as proof obligations:
287    ///
288    /// 1. Capability check passes
289    /// 2. Policy permits the action
290    /// 3. Capability is inductively valid
291    /// 4. Target resource is live
292    /// 5. Rights are confined
293    /// 6. Biba integrity satisfied
294    pub(crate) fn validate(&self, state: &State) -> Result<(), AuthorizationError> {
295        // 1. Capability check
296        self.check_capability(state)?;
297
298        // 2. Policy check
299        self.check_policy(state)?;
300
301        // 3. Capability validity (revocation chain)
302        self.check_validity(state)?;
303
304        // 4. Target liveness
305        self.check_liveness(state)?;
306
307        // 5. Rights confinement
308        self.check_confinement()?;
309
310        // 6. Biba integrity
311        self.check_biba(state)?;
312
313        Ok(())
314    }
315
316    /// Get the capability (read-only access)
317    pub fn cap(&self) -> &Capability {
318        &self.cap
319    }
320
321    /// Get the action (read-only access)
322    pub fn action(&self) -> &Action {
323        &self.action
324    }
325
326    /// Get the policy context (read-only access)
327    pub fn ctx(&self) -> &PolicyContext {
328        &self.ctx
329    }
330
331    /// Check capability matches action
332    fn check_capability(&self, state: &State) -> Result<(), AuthorizationError> {
333        // Check holder matches
334        if self.cap.holder() != self.action.subject {
335            return Err(AuthorizationError::HolderMismatch {
336                expected: self.action.subject,
337                actual: self.cap.holder(),
338            });
339        }
340
341        // Check target matches
342        if self.cap.target() != self.action.target {
343            return Err(AuthorizationError::TargetMismatch {
344                expected: self.action.target,
345                actual: self.cap.target(),
346            });
347        }
348
349        // Check rights are sufficient
350        if !self.action.rights.is_subset_of(self.cap.rights()) {
351            return Err(AuthorizationError::InsufficientRights);
352        }
353
354        // Check plugin holds capability
355        if !state.plugin_holds(self.action.subject, self.cap.id()) {
356            return Err(AuthorizationError::CapabilityNotHeld(self.cap.id()));
357        }
358
359        Ok(())
360    }
361
362    /// Check policy permits action
363    fn check_policy(&self, state: &State) -> Result<(), AuthorizationError> {
364        let decision = state.kernel().policy().eval(&self.action, &self.ctx);
365
366        if decision.is_permit() {
367            Ok(())
368        } else {
369            Err(AuthorizationError::PolicyDenied)
370        }
371    }
372
373    /// Check capability validity (not revoked)
374    fn check_validity(&self, state: &State) -> Result<(), AuthorizationError> {
375        // Check capability exists in kernel
376        let kernel_cap = state
377            .kernel()
378            .revocation()
379            .get(self.cap.id())
380            .ok_or(AuthorizationError::CapabilityNotFound(self.cap.id()))?;
381
382        // Check not revoked
383        if !kernel_cap.is_valid() {
384            return Err(AuthorizationError::CapabilityRevoked(self.cap.id()));
385        }
386
387        // Check parent chain is valid (if has parent)
388        if let Some(parent_id) = self.cap.parent() {
389            if !state.kernel().revocation().is_valid(parent_id) {
390                return Err(AuthorizationError::CapabilityRevoked(parent_id));
391            }
392        }
393
394        Ok(())
395    }
396
397    /// Check target resource is live
398    fn check_liveness(&self, state: &State) -> Result<(), AuthorizationError> {
399        // action.target is ResourceId (u128); ghost uses MemAddr (u64) — truncate for address lookup
400        let addr = self.action.target as MemAddr;
401        if !state.ghost().is_live(addr) {
402            return Err(AuthorizationError::ResourceNotLive(addr));
403        }
404        Ok(())
405    }
406
407    /// Check rights confinement
408    fn check_confinement(&self) -> Result<(), AuthorizationError> {
409        if !self.action.rights.is_subset_of(self.cap.rights()) {
410            return Err(AuthorizationError::InsufficientRights);
411        }
412        Ok(())
413    }
414
415    /// Check Biba integrity constraint
416    fn check_biba(&self, state: &State) -> Result<(), AuthorizationError> {
417        if !biba_write_ok(state, &self.action) {
418            let writer_level = state
419                .plugin_level(self.action.subject)
420                .unwrap_or(SecurityLevel::Public);
421            // action.target is ResourceId (u128); ghost uses MemAddr (u64) — truncate for address lookup
422            let target_level = resource_integrity(state, self.action.target as MemAddr);
423            return Err(AuthorizationError::BibaViolation {
424                writer_level,
425                target_level,
426            });
427        }
428        Ok(())
429    }
430
431    /// Get the capability ID being used
432    pub fn cap_id(&self) -> CapId {
433        self.cap.id()
434    }
435
436    /// Check if holder has the capability (theorem correspondence)
437    ///
438    /// Corresponds to Lean: `theorem Authorized.holder_has_cap`
439    pub fn holder_has_cap(&self, state: &State) -> bool {
440        state.plugin_holds(self.action.subject, self.cap.id())
441    }
442
443    /// Check if policy is permitted (theorem correspondence)
444    ///
445    /// Corresponds to Lean: `theorem Authorized.policy_permitted`
446    pub fn policy_permitted(&self, state: &State) -> bool {
447        state
448            .kernel()
449            .policy()
450            .eval(&self.action, &self.ctx)
451            .is_permit()
452    }
453
454    /// Check if rights are confined (theorem correspondence)
455    ///
456    /// Corresponds to Lean: `theorem Authorized.rights_confined`
457    pub fn rights_confined(&self) -> bool {
458        self.action.rights.is_subset_of(self.cap.rights())
459    }
460
461    /// Check if Biba is satisfied (theorem correspondence)
462    ///
463    /// Corresponds to Lean: `theorem Authorized.biba_satisfied`
464    pub fn biba_satisfied(&self, state: &State) -> bool {
465        biba_write_ok(state, &self.action)
466    }
467}
468
469/// Create an Authorized witness for legacy/test code.
470///
471/// **WARNING**: This bypasses atomic validation. Only use in tests
472/// or where you immediately call validate() in the same function.
473///
474/// For production code, use `Authorized::validate_atomic()` instead.
475#[cfg(test)]
476impl Authorized {
477    /// Create an `Authorized` token for testing, bypassing atomic validation.
478    pub fn new_for_test(cap: Capability, action: Action, ctx: PolicyContext) -> Self {
479        Authorized::new_internal(cap, action, ctx)
480    }
481}
482
483/// Action is properly mediated (has valid authorization)
484///
485/// Corresponds to Lean: `def properly_mediated`
486#[allow(dead_code)] // Lean correspondence
487pub fn properly_mediated(state: &State, auth: &Authorized) -> bool {
488    auth.validate(state).is_ok()
489}
490
491/// Combined authorization function
492///
493/// Corresponds to Lean: `def authorize`
494///
495/// authorize(p, c, a) = phi(p, a) AND kappa(c, a)
496#[allow(dead_code)] // Lean correspondence
497pub fn authorize(state: &State, cap: &Capability, action: &Action, ctx: &PolicyContext) -> bool {
498    // Policy check
499    let policy_ok = state.kernel().policy().eval(action, ctx).is_permit();
500
501    // Capability check
502    let cap_ok = capability_check(state, action, cap);
503
504    policy_ok && cap_ok
505}
506
507#[cfg(test)]
508mod tests {
509    use super::*;
510    use crate::state::PluginState;
511    use crate::types::{Rights, SealedTag};
512
513    fn make_test_cap(id: CapId, holder: u128, target: u128) -> Capability {
514        Capability::new(
515            id,
516            holder,
517            target,
518            Rights::singleton(Right::Read),
519            None,
520            0,
521            SealedTag::empty(),
522        )
523        .expect("valid capability")
524    }
525
526    #[test]
527    fn test_resource_integrity_unallocated() {
528        let state = State::empty();
529        // Unallocated resource has Public integrity
530        assert_eq!(resource_integrity(&state, 999), SecurityLevel::Public);
531    }
532
533    #[test]
534    fn test_biba_write_ok_no_write() {
535        let state = State::empty();
536        let action = Action {
537            subject: 1,
538            target: 100,
539            rights: Rights::singleton(Right::Read), // No write
540            kind: "read".to_string(),
541        };
542
543        // No write right means Biba is satisfied
544        assert!(biba_write_ok(&state, &action));
545    }
546
547    #[test]
548    fn test_cap_is_valid_not_found() {
549        let state = State::empty();
550        let cap = make_test_cap(1, 1, 100);
551
552        // Cap not in kernel is not valid
553        assert!(!cap_is_valid(&state, &cap));
554    }
555
556    #[test]
557    fn test_cap_is_valid_in_kernel() {
558        let mut state = State::empty();
559
560        let cap = make_test_cap(1, 1, 100);
561        state
562            .apply_cap_delegate_mut(cap.clone(), 1)
563            .expect("delegate should succeed");
564
565        // Cap in kernel is valid
566        assert!(cap_is_valid(&state, &cap));
567    }
568
569    #[test]
570    fn test_capability_check_holder_mismatch() {
571        let mut state = State::empty();
572        let _ = state.insert_plugin(1, PluginState::empty(SecurityLevel::Public, 0));
573
574        let cap = make_test_cap(1, 2, 100); // Holder is 2
575        let action = Action {
576            subject: 1, // Subject is 1
577            target: 100,
578            rights: Rights::singleton(Right::Read),
579            kind: "read".to_string(),
580        };
581
582        assert!(!capability_check(&state, &action, &cap));
583    }
584
585    #[test]
586    fn test_authorized_validate_cap_not_held() {
587        let mut state = State::empty();
588        let _ = state.insert_plugin(1, PluginState::empty(SecurityLevel::Public, 0));
589
590        let cap = make_test_cap(1, 1, 100);
591        let action = Action {
592            subject: 1,
593            target: 100,
594            rights: Rights::singleton(Right::Read),
595            kind: "read".to_string(),
596        };
597        let ctx = PolicyContext::default();
598
599        // Use validate_atomic which should fail since cap is not held
600        let result = Authorized::validate_atomic(&state, cap, action, ctx);
601
602        assert!(matches!(
603            result,
604            Err(AuthorizationError::CapabilityNotHeld(_))
605        ));
606    }
607
608    #[test]
609    fn test_authorize_both_pass() {
610        let mut state = State::empty();
611        let mut ps = PluginState::empty(SecurityLevel::Public, 0);
612        ps.grant_cap_mut(1);
613        state.insert_plugin(1, ps).unwrap();
614
615        let cap = make_test_cap(1, 1, 100);
616        state
617            .apply_cap_delegate_mut(cap.clone(), 1)
618            .expect("delegate should succeed");
619
620        // Allocate the target resource
621        let mut ghost = state.ghost().clone();
622        ghost.alloc_mut(100, 1);
623
624        let action = Action {
625            subject: 1,
626            target: 100,
627            rights: Rights::singleton(Right::Read),
628            kind: "read".to_string(),
629        };
630        let _ctx = PolicyContext::default();
631
632        // With default policy (permit-all), should pass cap check
633        // Note: full authorize requires policy to permit
634        assert!(capability_check(&state, &action, &cap));
635    }
636}