From 30aa672b6a96408a8115d6ebb1b761084fc4e2d4 Mon Sep 17 00:00:00 2001 From: bordumb Date: Sun, 22 Mar 2026 22:03:44 -0700 Subject: [PATCH] feat: harden SealProof with private field and value-based constructor --- crates/capsec-core/src/attenuate.rs | 14 ++ crates/capsec-core/src/cap.rs | 9 +- crates/capsec-core/src/cap_provider.rs | 189 +++++++++++++++++++++++++ crates/capsec-core/src/error.rs | 4 + crates/capsec-core/src/lib.rs | 1 + crates/capsec-core/src/permission.rs | 15 +- crates/capsec-macro/src/lib.rs | 4 +- crates/capsec/src/lib.rs | 8 +- proofs/Capsec/Has.lean | 17 +++ proofs/Capsec/Soundness.lean | 37 +++++ 10 files changed, 286 insertions(+), 12 deletions(-) create mode 100644 crates/capsec-core/src/cap_provider.rs diff --git a/crates/capsec-core/src/attenuate.rs b/crates/capsec-core/src/attenuate.rs index 130f28d..68f1d29 100644 --- a/crates/capsec-core/src/attenuate.rs +++ b/crates/capsec-core/src/attenuate.rs @@ -63,6 +63,20 @@ impl Attenuated { } } +// Note: Attenuated does NOT implement Has

(to prevent scope bypass), +// so the blanket CapProvider

impl for T: Has

does not apply. +// Instead, Attenuated implements CapProvider

directly with scope enforcement. +// +// This is sound because Rust's coherence rules guarantee no overlap: +// Attenuated never implements Has

, so the blanket impl cannot cover it. +// We use a negative-impl-style guarantee by never adding Has

for Attenuated. +impl crate::cap_provider::CapProvider

for Attenuated { + fn provide_cap(&self, target: &str) -> Result, CapSecError> { + self.check(target)?; + Ok(Cap::new()) + } +} + /// Restricts filesystem operations to a directory subtree. /// /// Paths are canonicalized before comparison to prevent `../` traversal attacks. diff --git a/crates/capsec-core/src/cap.rs b/crates/capsec-core/src/cap.rs index c57f5c2..ee7825b 100644 --- a/crates/capsec-core/src/cap.rs +++ b/crates/capsec-core/src/cap.rs @@ -48,12 +48,13 @@ impl Cap

{ /// Creates a new capability token for use by `#[capsec::permission]` generated code. /// /// This constructor is public so that derive macros can create `Cap

` for - /// user-defined permission types from external crates. The `SealProof` bound - /// ensures only types with a valid seal token can use this. + /// user-defined permission types from external crates. Requires both the + /// `SealProof` type bound AND a `SealProof` value (which can only be obtained + /// via `__capsec_seal()`). /// /// Do not call directly — use `#[capsec::permission]` instead. #[doc(hidden)] - pub fn __capsec_new_derived() -> Self + pub fn __capsec_new_derived(_seal: crate::__private::SealProof) -> Self where P: Permission<__CapsecSeal = crate::__private::SealProof>, { @@ -113,7 +114,7 @@ impl SendCap

{ /// /// Do not call directly — use `#[capsec::permission]` instead. #[doc(hidden)] - pub fn __capsec_new_send_derived() -> Self + pub fn __capsec_new_send_derived(_seal: crate::__private::SealProof) -> Self where P: Permission<__CapsecSeal = crate::__private::SealProof>, { diff --git a/crates/capsec-core/src/cap_provider.rs b/crates/capsec-core/src/cap_provider.rs new file mode 100644 index 0000000..c8b36a9 --- /dev/null +++ b/crates/capsec-core/src/cap_provider.rs @@ -0,0 +1,189 @@ +//! The [`CapProvider

`] trait — unified capability access with optional scope enforcement. +//! +//! `CapProvider

` generalizes [`Has

`](crate::has::Has) to support both unscoped +//! capabilities (which always succeed) and scoped capabilities +//! ([`Attenuated`](crate::attenuate::Attenuated)) which check the target against +//! a scope before granting access. + +use crate::cap::Cap; +use crate::error::CapSecError; +use crate::permission::Permission; + +/// A type that can provide a capability token for permission `P`, possibly +/// after performing a scope check against the target. +pub trait CapProvider { + /// Provides a `Cap

` for the given target, or returns an error if the + /// target is outside the capability's scope. + fn provide_cap(&self, target: &str) -> Result, CapSecError>; +} + +// We cannot use a blanket `impl> CapProvider

for T` because +// Rust's coherence rules can't prove Attenuated won't impl Has in the future. +// Instead, we require types to impl CapProvider explicitly. +// The #[capsec::context] macro and built-in types all get impls. +// For user-defined Has

impls, provide a convenience macro. + +/// Implement `CapProvider

` for a type that already implements `Has

`. +/// +/// Since `Has

` is infallible, the implementation always returns `Ok` +/// and ignores the target string. +/// +/// # Example +/// +/// ```rust,ignore +/// struct MyCtx { cap: Cap } +/// impl Has for MyCtx { fn cap_ref(&self) -> Cap { self.cap.clone() } } +/// capsec_core::impl_cap_provider_for_has!(MyCtx, FsRead); +/// ``` +#[macro_export] +macro_rules! impl_cap_provider_for_has { + ($ty:ty, $perm:ty) => { + impl $crate::cap_provider::CapProvider<$perm> for $ty { + fn provide_cap( + &self, + _target: &str, + ) -> Result<$crate::cap::Cap<$perm>, $crate::error::CapSecError> { + Ok(>::cap_ref(self)) + } + } + }; +} + +// ── Built-in impls: Cap

, SendCap

───────────────────────────── + +impl CapProvider

for Cap

{ + fn provide_cap(&self, _target: &str) -> Result, CapSecError> { + Ok(Cap::new()) + } +} + +impl CapProvider

for crate::cap::SendCap

{ + fn provide_cap(&self, _target: &str) -> Result, CapSecError> { + Ok(Cap::new()) + } +} + +// ── Subsumption ───────────────────────────────────────────────────── + +macro_rules! impl_cap_provider_subsumes { + ($super:ty => $($sub:ty),+) => { + $( + impl CapProvider<$sub> for Cap<$super> { + fn provide_cap(&self, _target: &str) -> Result, CapSecError> { + Ok(Cap::new()) + } + } + )+ + } +} + +use crate::permission::*; + +impl_cap_provider_subsumes!(FsAll => FsRead, FsWrite); +impl_cap_provider_subsumes!(NetAll => NetConnect, NetBind); + +// ── Ambient ───────────────────────────────────────────────────────── + +macro_rules! impl_cap_provider_ambient { + ($($perm:ty),+) => { + $( + impl CapProvider<$perm> for Cap { + fn provide_cap(&self, _target: &str) -> Result, CapSecError> { + Ok(Cap::new()) + } + } + )+ + } +} + +impl_cap_provider_ambient!( + FsRead, FsWrite, FsAll, NetConnect, NetBind, NetAll, EnvRead, EnvWrite, Spawn +); + +// ── Tuples ────────────────────────────────────────────────────────── + +macro_rules! impl_cap_provider_tuple_first { + ([$($a:ident),+]; $all:tt) => { + $( impl_cap_provider_tuple_first!(@inner $a; $all); )+ + }; + (@inner $a:ident; [$($b:ident),+]) => { + $( + impl CapProvider<$a> for Cap<($a, $b)> { + fn provide_cap(&self, _target: &str) -> Result, CapSecError> { + Ok(Cap::new()) + } + } + )+ + }; +} + +macro_rules! impl_cap_provider_tuple_second { + ($first:ident $(, $rest:ident)+) => { + $( + impl CapProvider<$first> for Cap<($rest, $first)> { + fn provide_cap(&self, _target: &str) -> Result, CapSecError> { + Ok(Cap::new()) + } + } + impl CapProvider<$rest> for Cap<($first, $rest)> { + fn provide_cap(&self, _target: &str) -> Result, CapSecError> { + Ok(Cap::new()) + } + } + )+ + impl_cap_provider_tuple_second!($($rest),+); + }; + ($single:ident) => {}; +} + +impl_cap_provider_tuple_first!( + [FsRead, FsWrite, FsAll, NetConnect, NetBind, NetAll, EnvRead, EnvWrite, Spawn, Ambient]; + [FsRead, FsWrite, FsAll, NetConnect, NetBind, NetAll, EnvRead, EnvWrite, Spawn, Ambient] +); + +impl_cap_provider_tuple_second!( + FsRead, FsWrite, FsAll, NetConnect, NetBind, NetAll, EnvRead, EnvWrite, Spawn, Ambient +); + +#[cfg(test)] +mod tests { + use super::*; + + #[test] + fn cap_provides() { + let root = crate::root::test_root(); + let cap = root.grant::(); + assert!(cap.provide_cap("/any").is_ok()); + } + + #[test] + fn sendcap_provides() { + let root = crate::root::test_root(); + let cap = root.grant::().make_send(); + assert!(cap.provide_cap("/any").is_ok()); + } + + #[test] + fn subsumption_provides() { + let root = crate::root::test_root(); + let cap = root.grant::(); + let result: Result, _> = cap.provide_cap("/any"); + assert!(result.is_ok()); + } + + #[test] + fn ambient_provides() { + let root = crate::root::test_root(); + let cap = root.grant::(); + let result: Result, _> = cap.provide_cap("/any"); + assert!(result.is_ok()); + } + + #[test] + fn tuple_provides() { + let root = crate::root::test_root(); + let cap = root.grant::<(FsRead, NetConnect)>(); + assert!(CapProvider::::provide_cap(&cap, "/any").is_ok()); + assert!(CapProvider::::provide_cap(&cap, "host").is_ok()); + } +} diff --git a/crates/capsec-core/src/error.rs b/crates/capsec-core/src/error.rs index 8cf89cf..6920e55 100644 --- a/crates/capsec-core/src/error.rs +++ b/crates/capsec-core/src/error.rs @@ -33,4 +33,8 @@ pub enum CapSecError { /// The capability requires multiple approvals, but not all have been granted. #[error("capability requires dual-key approval, but approvals are insufficient")] InsufficientApprovals, + + /// An environment variable lookup error. + #[error(transparent)] + Env(#[from] std::env::VarError), } diff --git a/crates/capsec-core/src/lib.rs b/crates/capsec-core/src/lib.rs index cbc8d12..4941833 100644 --- a/crates/capsec-core/src/lib.rs +++ b/crates/capsec-core/src/lib.rs @@ -41,6 +41,7 @@ pub mod attenuate; pub mod cap; +pub mod cap_provider; pub mod error; pub mod has; pub mod permission; diff --git a/crates/capsec-core/src/permission.rs b/crates/capsec-core/src/permission.rs index fa6d135..93948b5 100644 --- a/crates/capsec-core/src/permission.rs +++ b/crates/capsec-core/src/permission.rs @@ -162,17 +162,26 @@ impl Subsumes

for Ambient {} // Seal token — prevents manual Permission implementation. // The #[capsec::permission] macro generates the correct seal. -// Users could write this by hand (it's #[doc(hidden)], not private), -// but that's equivalent to writing `unsafe` — they own the consequences. +// The private field on SealProof prevents external construction — +// only `__capsec_seal()` can create one, and it's #[doc(hidden)]. #[doc(hidden)] pub mod __private { /// Proof token that a permission was registered via the capsec derive macro. - pub struct SealProof; + /// + /// Has a private field — cannot be constructed outside this module. + /// Use `__capsec_seal()` (generated by `#[capsec::permission]`) instead. + pub struct SealProof(()); /// Trait bound for the seal associated type. pub trait SealToken {} impl SealToken for SealProof {} + + /// Creates a seal proof. Only called by `#[capsec::permission]` generated code. + #[doc(hidden)] + pub const fn __capsec_seal() -> SealProof { + SealProof(()) + } } #[cfg(test)] diff --git a/crates/capsec-macro/src/lib.rs b/crates/capsec-macro/src/lib.rs index 44d5ae6..90283bb 100644 --- a/crates/capsec-macro/src/lib.rs +++ b/crates/capsec-macro/src/lib.rs @@ -126,13 +126,13 @@ fn permission_inner( impl capsec_core::has::Has<#sub> for capsec_core::cap::Cap<#struct_name> { fn cap_ref(&self) -> capsec_core::cap::Cap<#sub> { - capsec_core::cap::Cap::__capsec_new_derived() + capsec_core::cap::Cap::__capsec_new_derived(capsec_core::__private::__capsec_seal()) } } impl capsec_core::has::Has<#sub> for capsec_core::cap::SendCap<#struct_name> { fn cap_ref(&self) -> capsec_core::cap::Cap<#sub> { - capsec_core::cap::Cap::__capsec_new_derived() + capsec_core::cap::Cap::__capsec_new_derived(capsec_core::__private::__capsec_seal()) } } } diff --git a/crates/capsec/src/lib.rs b/crates/capsec/src/lib.rs index 6524c8c..25584e1 100644 --- a/crates/capsec/src/lib.rs +++ b/crates/capsec/src/lib.rs @@ -44,6 +44,8 @@ pub use capsec_core::root::test_root; pub use capsec_core::attenuate::{Attenuated, DirScope, HostScope, Scope}; +pub use capsec_core::cap_provider::CapProvider; + pub use capsec_core::runtime::{Revoker, RuntimeCap, RuntimeSendCap, TimedCap, TimedSendCap}; pub use capsec_core::prescript::{ @@ -120,8 +122,8 @@ pub mod tokio { /// ``` pub mod prelude { pub use crate::{ - Ambient, ApproverA, ApproverB, Attenuated, Cap, CapRoot, CapSecError, DirScope, DualKeyCap, - EnvRead, EnvWrite, FsAll, FsRead, FsWrite, Has, HostScope, LoggedCap, NetAll, NetBind, - NetConnect, Permission, Revoker, RuntimeCap, Spawn, Subsumes, TimedCap, + Ambient, ApproverA, ApproverB, Attenuated, Cap, CapProvider, CapRoot, CapSecError, DirScope, + DualKeyCap, EnvRead, EnvWrite, FsAll, FsRead, FsWrite, Has, HostScope, LoggedCap, NetAll, + NetBind, NetConnect, Permission, Revoker, RuntimeCap, Spawn, Subsumes, TimedCap, }; } diff --git a/proofs/Capsec/Has.lean b/proofs/Capsec/Has.lean index f958da0..bd84596 100644 --- a/proofs/Capsec/Has.lean +++ b/proofs/Capsec/Has.lean @@ -20,3 +20,20 @@ inductive Has : List Perm → Perm → Prop where | subsumes {a b : Perm} : Subsumes a b → Has [a] b | ambient (p : Perm) : Has [Perm.ambient] p | tuple {ps : List Perm} {p : Perm} : p ∈ ps → Has ps p + +/-! +# CapProvides judgment + +Models the `CapProvider

` trait from `capsec-core/src/cap_provider.rs`. + +`CapProvides ps p` means "a capability provider holding permissions `ps` can +provide permission `p`, possibly after a scope check." + +Two constructors: +1. `from_has` — any `Has ps p` implies `CapProvides ps p` (blanket impl for Has types) +2. `from_scope` — a scoped capability provides permission (Attenuated impl) +-/ + +inductive CapProvides : List Perm → Perm → Prop where + | from_has {ps : List Perm} {p : Perm} : Has ps p → CapProvides ps p + | from_scope (ps : List Perm) (p : Perm) : p ∈ ps → CapProvides ps p diff --git a/proofs/Capsec/Soundness.lean b/proofs/Capsec/Soundness.lean index bc3653b..4bfe683 100644 --- a/proofs/Capsec/Soundness.lean +++ b/proofs/Capsec/Soundness.lean @@ -115,3 +115,40 @@ theorem tuple_has_first (a b : Perm) : Has [a, b] a := /-- The second element of a pair is granted. -/ theorem tuple_has_second (a b : Perm) : Has [a, b] b := Has.tuple (List.mem_cons_of_mem a (List.mem_cons_self b [])) + +-- ============================================================================ +-- 5. CapProvides — non-transitive authority +-- ============================================================================ + +/-- Any Has judgment lifts to CapProvides (blanket impl). -/ +theorem has_implies_cap_provides {ps : List Perm} {p : Perm} (h : Has ps p) : + CapProvides ps p := + CapProvides.from_has h + +/-- A scoped capability provides its own permission. -/ +theorem cap_provides_scope_self (p : Perm) : CapProvides [p] p := + CapProvides.from_scope [p] p (List.mem_cons_self p []) + +/-- CapProvides through scoped FsRead does not grant FsWrite. -/ +theorem cap_provides_no_escalation_fs : + ¬ CapProvides [Perm.fsRead] Perm.fsWrite := by + intro h + cases h with + | from_has hhas => + cases hhas with + | direct => contradiction + | subsumes hs => cases hs + | ambient => contradiction + | tuple hm => simp [List.mem_cons, List.mem_nil_iff] at hm + | from_scope _ _ hm => + simp [List.mem_cons, List.mem_nil_iff] at hm + +/-- CapProvides through FsAll does not grant NetConnect. -/ +theorem cap_provides_no_cross_leak : + ¬ CapProvides [Perm.fsAll] Perm.netConnect := by + intro h + cases h with + | from_has hhas => + exact absurd hhas no_cross_leak_fs_net + | from_scope _ _ hm => + simp [List.mem_cons, List.mem_nil_iff] at hm