feat: harden SealProof with private field and value-based constructor

crates/capsec-core/src/attenuate.rs

@@ -63,6 +63,20 @@ impl<P: Permission, S: Scope> Attenuated<P, S> {
     }
 }
 
+// Note: Attenuated<P, S> does NOT implement Has<P> (to prevent scope bypass),
+// so the blanket CapProvider<P> impl for T: Has<P> does not apply.
+// Instead, Attenuated implements CapProvider<P> directly with scope enforcement.
+//
+// This is sound because Rust's coherence rules guarantee no overlap:
+// Attenuated never implements Has<P>, so the blanket impl cannot cover it.
+// We use a negative-impl-style guarantee by never adding Has<P> for Attenuated.
+impl<P: Permission, S: Scope> crate::cap_provider::CapProvider<P> for Attenuated<P, S> {
+    fn provide_cap(&self, target: &str) -> Result<Cap<P>, CapSecError> {
+        self.check(target)?;
+        Ok(Cap::new())
+    }
+}
+
 /// Restricts filesystem operations to a directory subtree.
 ///
 /// Paths are canonicalized before comparison to prevent `../` traversal attacks.

crates/capsec-core/src/cap.rs

@@ -48,12 +48,13 @@ impl<P: Permission> Cap<P> {
     /// Creates a new capability token for use by `#[capsec::permission]` generated code.
     ///
     /// This constructor is public so that derive macros can create `Cap<P>` 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<P: Permission> SendCap<P> {
     ///
     /// 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>,
     {

crates/capsec-core/src/cap_provider.rs

@@ -0,0 +1,189 @@
+//! The [`CapProvider<P>`] trait — unified capability access with optional scope enforcement.
+//!
+//! `CapProvider<P>` generalizes [`Has<P>`](crate::has::Has) to support both unscoped
+//! capabilities (which always succeed) and scoped capabilities
+//! ([`Attenuated<P, S>`](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<P: Permission> {
+    /// Provides a `Cap<P>` for the given target, or returns an error if the
+    /// target is outside the capability's scope.
+    fn provide_cap(&self, target: &str) -> Result<Cap<P>, CapSecError>;
+}
+
+// We cannot use a blanket `impl<T: Has<P>> CapProvider<P> 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<P> impls, provide a convenience macro.
+
+/// Implement `CapProvider<P>` for a type that already implements `Has<P>`.
+///
+/// Since `Has<P>` is infallible, the implementation always returns `Ok`
+/// and ignores the target string.
+///
+/// # Example
+///
+/// ```rust,ignore
+/// struct MyCtx { cap: Cap<FsRead> }
+/// impl Has<FsRead> for MyCtx { fn cap_ref(&self) -> Cap<FsRead> { 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(<Self as $crate::has::Has<$perm>>::cap_ref(self))
+            }
+        }
+    };
+}
+
+// ── Built-in impls: Cap<P>, SendCap<P> ─────────────────────────────
+
+impl<P: Permission> CapProvider<P> for Cap<P> {
+    fn provide_cap(&self, _target: &str) -> Result<Cap<P>, CapSecError> {
+        Ok(Cap::new())
+    }
+}
+
+impl<P: Permission> CapProvider<P> for crate::cap::SendCap<P> {
+    fn provide_cap(&self, _target: &str) -> Result<Cap<P>, 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<Cap<$sub>, 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<Ambient> {
+                fn provide_cap(&self, _target: &str) -> Result<Cap<$perm>, 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<Cap<$a>, 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<Cap<$first>, CapSecError> {
+                    Ok(Cap::new())
+                }
+            }
+            impl CapProvider<$rest> for Cap<($first, $rest)> {
+                fn provide_cap(&self, _target: &str) -> Result<Cap<$rest>, 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::<FsRead>();
+        assert!(cap.provide_cap("/any").is_ok());
+    }
+
+    #[test]
+    fn sendcap_provides() {
+        let root = crate::root::test_root();
+        let cap = root.grant::<FsRead>().make_send();
+        assert!(cap.provide_cap("/any").is_ok());
+    }
+
+    #[test]
+    fn subsumption_provides() {
+        let root = crate::root::test_root();
+        let cap = root.grant::<FsAll>();
+        let result: Result<Cap<FsRead>, _> = cap.provide_cap("/any");
+        assert!(result.is_ok());
+    }
+
+    #[test]
+    fn ambient_provides() {
+        let root = crate::root::test_root();
+        let cap = root.grant::<Ambient>();
+        let result: Result<Cap<FsRead>, _> = 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::<FsRead>::provide_cap(&cap, "/any").is_ok());
+        assert!(CapProvider::<NetConnect>::provide_cap(&cap, "host").is_ok());
+    }
+}

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),
 }

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;

crates/capsec-core/src/permission.rs

@@ -162,17 +162,26 @@ impl<P: Permission> Subsumes<P> 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)]

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())
                     }
                 }
             }

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,
     };
 }

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<P>` 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<P, S> 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

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