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}