Skip to content

Commit 70a5655

Browse files
authored
Merge pull request #47 from auths-dev/dev-proofSeals
feat: harden SealProof with private field and value-based constructor
2 parents 63601c8 + 30aa672 commit 70a5655

10 files changed

Lines changed: 286 additions & 12 deletions

File tree

crates/capsec-core/src/attenuate.rs

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -63,6 +63,20 @@ impl<P: Permission, S: Scope> Attenuated<P, S> {
6363
}
6464
}
6565

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

crates/capsec-core/src/cap.rs

Lines changed: 5 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -48,12 +48,13 @@ impl<P: Permission> Cap<P> {
4848
/// Creates a new capability token for use by `#[capsec::permission]` generated code.
4949
///
5050
/// This constructor is public so that derive macros can create `Cap<P>` for
51-
/// user-defined permission types from external crates. The `SealProof` bound
52-
/// ensures only types with a valid seal token can use this.
51+
/// user-defined permission types from external crates. Requires both the
52+
/// `SealProof` type bound AND a `SealProof` value (which can only be obtained
53+
/// via `__capsec_seal()`).
5354
///
5455
/// Do not call directly — use `#[capsec::permission]` instead.
5556
#[doc(hidden)]
56-
pub fn __capsec_new_derived() -> Self
57+
pub fn __capsec_new_derived(_seal: crate::__private::SealProof) -> Self
5758
where
5859
P: Permission<__CapsecSeal = crate::__private::SealProof>,
5960
{
@@ -113,7 +114,7 @@ impl<P: Permission> SendCap<P> {
113114
///
114115
/// Do not call directly — use `#[capsec::permission]` instead.
115116
#[doc(hidden)]
116-
pub fn __capsec_new_send_derived() -> Self
117+
pub fn __capsec_new_send_derived(_seal: crate::__private::SealProof) -> Self
117118
where
118119
P: Permission<__CapsecSeal = crate::__private::SealProof>,
119120
{
Lines changed: 189 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,189 @@
1+
//! The [`CapProvider<P>`] trait — unified capability access with optional scope enforcement.
2+
//!
3+
//! `CapProvider<P>` generalizes [`Has<P>`](crate::has::Has) to support both unscoped
4+
//! capabilities (which always succeed) and scoped capabilities
5+
//! ([`Attenuated<P, S>`](crate::attenuate::Attenuated)) which check the target against
6+
//! a scope before granting access.
7+
8+
use crate::cap::Cap;
9+
use crate::error::CapSecError;
10+
use crate::permission::Permission;
11+
12+
/// A type that can provide a capability token for permission `P`, possibly
13+
/// after performing a scope check against the target.
14+
pub trait CapProvider<P: Permission> {
15+
/// Provides a `Cap<P>` for the given target, or returns an error if the
16+
/// target is outside the capability's scope.
17+
fn provide_cap(&self, target: &str) -> Result<Cap<P>, CapSecError>;
18+
}
19+
20+
// We cannot use a blanket `impl<T: Has<P>> CapProvider<P> for T` because
21+
// Rust's coherence rules can't prove Attenuated won't impl Has in the future.
22+
// Instead, we require types to impl CapProvider explicitly.
23+
// The #[capsec::context] macro and built-in types all get impls.
24+
// For user-defined Has<P> impls, provide a convenience macro.
25+
26+
/// Implement `CapProvider<P>` for a type that already implements `Has<P>`.
27+
///
28+
/// Since `Has<P>` is infallible, the implementation always returns `Ok`
29+
/// and ignores the target string.
30+
///
31+
/// # Example
32+
///
33+
/// ```rust,ignore
34+
/// struct MyCtx { cap: Cap<FsRead> }
35+
/// impl Has<FsRead> for MyCtx { fn cap_ref(&self) -> Cap<FsRead> { self.cap.clone() } }
36+
/// capsec_core::impl_cap_provider_for_has!(MyCtx, FsRead);
37+
/// ```
38+
#[macro_export]
39+
macro_rules! impl_cap_provider_for_has {
40+
($ty:ty, $perm:ty) => {
41+
impl $crate::cap_provider::CapProvider<$perm> for $ty {
42+
fn provide_cap(
43+
&self,
44+
_target: &str,
45+
) -> Result<$crate::cap::Cap<$perm>, $crate::error::CapSecError> {
46+
Ok(<Self as $crate::has::Has<$perm>>::cap_ref(self))
47+
}
48+
}
49+
};
50+
}
51+
52+
// ── Built-in impls: Cap<P>, SendCap<P> ─────────────────────────────
53+
54+
impl<P: Permission> CapProvider<P> for Cap<P> {
55+
fn provide_cap(&self, _target: &str) -> Result<Cap<P>, CapSecError> {
56+
Ok(Cap::new())
57+
}
58+
}
59+
60+
impl<P: Permission> CapProvider<P> for crate::cap::SendCap<P> {
61+
fn provide_cap(&self, _target: &str) -> Result<Cap<P>, CapSecError> {
62+
Ok(Cap::new())
63+
}
64+
}
65+
66+
// ── Subsumption ─────────────────────────────────────────────────────
67+
68+
macro_rules! impl_cap_provider_subsumes {
69+
($super:ty => $($sub:ty),+) => {
70+
$(
71+
impl CapProvider<$sub> for Cap<$super> {
72+
fn provide_cap(&self, _target: &str) -> Result<Cap<$sub>, CapSecError> {
73+
Ok(Cap::new())
74+
}
75+
}
76+
)+
77+
}
78+
}
79+
80+
use crate::permission::*;
81+
82+
impl_cap_provider_subsumes!(FsAll => FsRead, FsWrite);
83+
impl_cap_provider_subsumes!(NetAll => NetConnect, NetBind);
84+
85+
// ── Ambient ─────────────────────────────────────────────────────────
86+
87+
macro_rules! impl_cap_provider_ambient {
88+
($($perm:ty),+) => {
89+
$(
90+
impl CapProvider<$perm> for Cap<Ambient> {
91+
fn provide_cap(&self, _target: &str) -> Result<Cap<$perm>, CapSecError> {
92+
Ok(Cap::new())
93+
}
94+
}
95+
)+
96+
}
97+
}
98+
99+
impl_cap_provider_ambient!(
100+
FsRead, FsWrite, FsAll, NetConnect, NetBind, NetAll, EnvRead, EnvWrite, Spawn
101+
);
102+
103+
// ── Tuples ──────────────────────────────────────────────────────────
104+
105+
macro_rules! impl_cap_provider_tuple_first {
106+
([$($a:ident),+]; $all:tt) => {
107+
$( impl_cap_provider_tuple_first!(@inner $a; $all); )+
108+
};
109+
(@inner $a:ident; [$($b:ident),+]) => {
110+
$(
111+
impl CapProvider<$a> for Cap<($a, $b)> {
112+
fn provide_cap(&self, _target: &str) -> Result<Cap<$a>, CapSecError> {
113+
Ok(Cap::new())
114+
}
115+
}
116+
)+
117+
};
118+
}
119+
120+
macro_rules! impl_cap_provider_tuple_second {
121+
($first:ident $(, $rest:ident)+) => {
122+
$(
123+
impl CapProvider<$first> for Cap<($rest, $first)> {
124+
fn provide_cap(&self, _target: &str) -> Result<Cap<$first>, CapSecError> {
125+
Ok(Cap::new())
126+
}
127+
}
128+
impl CapProvider<$rest> for Cap<($first, $rest)> {
129+
fn provide_cap(&self, _target: &str) -> Result<Cap<$rest>, CapSecError> {
130+
Ok(Cap::new())
131+
}
132+
}
133+
)+
134+
impl_cap_provider_tuple_second!($($rest),+);
135+
};
136+
($single:ident) => {};
137+
}
138+
139+
impl_cap_provider_tuple_first!(
140+
[FsRead, FsWrite, FsAll, NetConnect, NetBind, NetAll, EnvRead, EnvWrite, Spawn, Ambient];
141+
[FsRead, FsWrite, FsAll, NetConnect, NetBind, NetAll, EnvRead, EnvWrite, Spawn, Ambient]
142+
);
143+
144+
impl_cap_provider_tuple_second!(
145+
FsRead, FsWrite, FsAll, NetConnect, NetBind, NetAll, EnvRead, EnvWrite, Spawn, Ambient
146+
);
147+
148+
#[cfg(test)]
149+
mod tests {
150+
use super::*;
151+
152+
#[test]
153+
fn cap_provides() {
154+
let root = crate::root::test_root();
155+
let cap = root.grant::<FsRead>();
156+
assert!(cap.provide_cap("/any").is_ok());
157+
}
158+
159+
#[test]
160+
fn sendcap_provides() {
161+
let root = crate::root::test_root();
162+
let cap = root.grant::<FsRead>().make_send();
163+
assert!(cap.provide_cap("/any").is_ok());
164+
}
165+
166+
#[test]
167+
fn subsumption_provides() {
168+
let root = crate::root::test_root();
169+
let cap = root.grant::<FsAll>();
170+
let result: Result<Cap<FsRead>, _> = cap.provide_cap("/any");
171+
assert!(result.is_ok());
172+
}
173+
174+
#[test]
175+
fn ambient_provides() {
176+
let root = crate::root::test_root();
177+
let cap = root.grant::<Ambient>();
178+
let result: Result<Cap<FsRead>, _> = cap.provide_cap("/any");
179+
assert!(result.is_ok());
180+
}
181+
182+
#[test]
183+
fn tuple_provides() {
184+
let root = crate::root::test_root();
185+
let cap = root.grant::<(FsRead, NetConnect)>();
186+
assert!(CapProvider::<FsRead>::provide_cap(&cap, "/any").is_ok());
187+
assert!(CapProvider::<NetConnect>::provide_cap(&cap, "host").is_ok());
188+
}
189+
}

crates/capsec-core/src/error.rs

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -33,4 +33,8 @@ pub enum CapSecError {
3333
/// The capability requires multiple approvals, but not all have been granted.
3434
#[error("capability requires dual-key approval, but approvals are insufficient")]
3535
InsufficientApprovals,
36+
37+
/// An environment variable lookup error.
38+
#[error(transparent)]
39+
Env(#[from] std::env::VarError),
3640
}

crates/capsec-core/src/lib.rs

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -41,6 +41,7 @@
4141
4242
pub mod attenuate;
4343
pub mod cap;
44+
pub mod cap_provider;
4445
pub mod error;
4546
pub mod has;
4647
pub mod permission;

crates/capsec-core/src/permission.rs

Lines changed: 12 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -162,17 +162,26 @@ impl<P: Permission> Subsumes<P> for Ambient {}
162162

163163
// Seal token — prevents manual Permission implementation.
164164
// The #[capsec::permission] macro generates the correct seal.
165-
// Users could write this by hand (it's #[doc(hidden)], not private),
166-
// but that's equivalent to writing `unsafe` — they own the consequences.
165+
// The private field on SealProof prevents external construction —
166+
// only `__capsec_seal()` can create one, and it's #[doc(hidden)].
167167

168168
#[doc(hidden)]
169169
pub mod __private {
170170
/// Proof token that a permission was registered via the capsec derive macro.
171-
pub struct SealProof;
171+
///
172+
/// Has a private field — cannot be constructed outside this module.
173+
/// Use `__capsec_seal()` (generated by `#[capsec::permission]`) instead.
174+
pub struct SealProof(());
172175

173176
/// Trait bound for the seal associated type.
174177
pub trait SealToken {}
175178
impl SealToken for SealProof {}
179+
180+
/// Creates a seal proof. Only called by `#[capsec::permission]` generated code.
181+
#[doc(hidden)]
182+
pub const fn __capsec_seal() -> SealProof {
183+
SealProof(())
184+
}
176185
}
177186

178187
#[cfg(test)]

crates/capsec-macro/src/lib.rs

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -126,13 +126,13 @@ fn permission_inner(
126126

127127
impl capsec_core::has::Has<#sub> for capsec_core::cap::Cap<#struct_name> {
128128
fn cap_ref(&self) -> capsec_core::cap::Cap<#sub> {
129-
capsec_core::cap::Cap::__capsec_new_derived()
129+
capsec_core::cap::Cap::__capsec_new_derived(capsec_core::__private::__capsec_seal())
130130
}
131131
}
132132

133133
impl capsec_core::has::Has<#sub> for capsec_core::cap::SendCap<#struct_name> {
134134
fn cap_ref(&self) -> capsec_core::cap::Cap<#sub> {
135-
capsec_core::cap::Cap::__capsec_new_derived()
135+
capsec_core::cap::Cap::__capsec_new_derived(capsec_core::__private::__capsec_seal())
136136
}
137137
}
138138
}

crates/capsec/src/lib.rs

Lines changed: 5 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -44,6 +44,8 @@ pub use capsec_core::root::test_root;
4444

4545
pub use capsec_core::attenuate::{Attenuated, DirScope, HostScope, Scope};
4646

47+
pub use capsec_core::cap_provider::CapProvider;
48+
4749
pub use capsec_core::runtime::{Revoker, RuntimeCap, RuntimeSendCap, TimedCap, TimedSendCap};
4850

4951
pub use capsec_core::prescript::{
@@ -120,8 +122,8 @@ pub mod tokio {
120122
/// ```
121123
pub mod prelude {
122124
pub use crate::{
123-
Ambient, ApproverA, ApproverB, Attenuated, Cap, CapRoot, CapSecError, DirScope, DualKeyCap,
124-
EnvRead, EnvWrite, FsAll, FsRead, FsWrite, Has, HostScope, LoggedCap, NetAll, NetBind,
125-
NetConnect, Permission, Revoker, RuntimeCap, Spawn, Subsumes, TimedCap,
125+
Ambient, ApproverA, ApproverB, Attenuated, Cap, CapProvider, CapRoot, CapSecError, DirScope,
126+
DualKeyCap, EnvRead, EnvWrite, FsAll, FsRead, FsWrite, Has, HostScope, LoggedCap, NetAll,
127+
NetBind, NetConnect, Permission, Revoker, RuntimeCap, Spawn, Subsumes, TimedCap,
126128
};
127129
}

proofs/Capsec/Has.lean

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -20,3 +20,20 @@ inductive Has : List Perm → Perm → Prop where
2020
| subsumes {a b : Perm} : Subsumes a b → Has [a] b
2121
| ambient (p : Perm) : Has [Perm.ambient] p
2222
| tuple {ps : List Perm} {p : Perm} : p ∈ ps → Has ps p
23+
24+
/-!
25+
# CapProvides judgment
26+
27+
Models the `CapProvider<P>` trait from `capsec-core/src/cap_provider.rs`.
28+
29+
`CapProvides ps p` means "a capability provider holding permissions `ps` can
30+
provide permission `p`, possibly after a scope check."
31+
32+
Two constructors:
33+
1. `from_has` — any `Has ps p` implies `CapProvides ps p` (blanket impl for Has types)
34+
2. `from_scope` — a scoped capability provides permission (Attenuated<P, S> impl)
35+
-/
36+
37+
inductive CapProvides : List Perm → Perm → Prop where
38+
| from_has {ps : List Perm} {p : Perm} : Has ps p → CapProvides ps p
39+
| from_scope (ps : List Perm) (p : Perm) : p ∈ ps → CapProvides ps p

proofs/Capsec/Soundness.lean

Lines changed: 37 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -115,3 +115,40 @@ theorem tuple_has_first (a b : Perm) : Has [a, b] a :=
115115
/-- The second element of a pair is granted. -/
116116
theorem tuple_has_second (a b : Perm) : Has [a, b] b :=
117117
Has.tuple (List.mem_cons_of_mem a (List.mem_cons_self b []))
118+
119+
-- ============================================================================
120+
-- 5. CapProvides — non-transitive authority
121+
-- ============================================================================
122+
123+
/-- Any Has judgment lifts to CapProvides (blanket impl). -/
124+
theorem has_implies_cap_provides {ps : List Perm} {p : Perm} (h : Has ps p) :
125+
CapProvides ps p :=
126+
CapProvides.from_has h
127+
128+
/-- A scoped capability provides its own permission. -/
129+
theorem cap_provides_scope_self (p : Perm) : CapProvides [p] p :=
130+
CapProvides.from_scope [p] p (List.mem_cons_self p [])
131+
132+
/-- CapProvides through scoped FsRead does not grant FsWrite. -/
133+
theorem cap_provides_no_escalation_fs :
134+
¬ CapProvides [Perm.fsRead] Perm.fsWrite := by
135+
intro h
136+
cases h with
137+
| from_has hhas =>
138+
cases hhas with
139+
| direct => contradiction
140+
| subsumes hs => cases hs
141+
| ambient => contradiction
142+
| tuple hm => simp [List.mem_cons, List.mem_nil_iff] at hm
143+
| from_scope _ _ hm =>
144+
simp [List.mem_cons, List.mem_nil_iff] at hm
145+
146+
/-- CapProvides through FsAll does not grant NetConnect. -/
147+
theorem cap_provides_no_cross_leak :
148+
¬ CapProvides [Perm.fsAll] Perm.netConnect := by
149+
intro h
150+
cases h with
151+
| from_has hhas =>
152+
exact absurd hhas no_cross_leak_fs_net
153+
| from_scope _ _ hm =>
154+
simp [List.mem_cons, List.mem_nil_iff] at hm

0 commit comments

Comments
 (0)