1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
//! `dangerous-test-hooks` proof hooks for the Linux backend S1 coupling proof
//! (`coupling_proof.rs`): build representative profiles WITHOUT the live kernel,
//! expose the production [`BackendProfile`] ceiling + the [`ProfileFacts`] the §3
//! floor predicate is checked against. Split from backend_impl.rs to hold it under
//! the non-overridable file-size cap; the whole module is feature-gated so the
//! default public surface is unaffected.
use super::super::support_matrix;
use super::{default_secret_resolver, LinuxBackend, LANDLOCK_ABI_FLOOR};
use crate::contract::backend::Backend;
use crate::contract::capability::Enforcement;
use crate::contract::ids::BackendId;
use crate::contract::plan::BoundaryRequirement;
use crate::contract::support::{BackendProfile, RequirementKind};
impl LinuxBackend {
/// The minimum landlock ABI this backend floors `Filesystem` to `Enforced` at.
pub const LANDLOCK_ABI_FLOOR: i64 = LANDLOCK_ABI_FLOOR;
/// A representative profile with a FORCED cgroup confinement base at the FS ABI
/// floor — the production-shaped profile that backs Filesystem + Kill +
/// process_count Enforced. `pids_peak` controls the `ResourceUsage` evidence.
#[must_use]
pub fn with_cgroup_for_proof(pids_peak: bool) -> Self {
Self {
id: BackendId::new(Self::ID),
support: support_matrix(),
landlock_abi: LANDLOCK_ABI_FLOOR,
launcher_path: None,
cgroup_base: Some(std::path::PathBuf::from("/sys/fs/cgroup/proof-placeholder")),
cgroup_pids_peak: pids_peak,
// The production-shaped proof profile permits unprivileged userns+netns, so its
// ceiling backs NetworkDenyAll=Enforced and the coupling gate qualifies it.
netns_available: true,
// The production-shaped proof profile supports seccomp filter mode, so its ceiling
// backs ChildSpawnDenyNewTasks=Enforced and the coupling gate qualifies it.
seccomp_available: true,
secret_resolver: default_secret_resolver(),
}
}
/// A representative profile with a FORCED landlock ABI and NO cgroup base — for
/// proving the at-floor and below-floor FS ceilings without a live kernel.
#[must_use]
pub fn with_abi_for_proof(landlock_abi: i64) -> Self {
Self {
id: BackendId::new(Self::ID),
support: support_matrix(),
landlock_abi,
launcher_path: None,
cgroup_base: None,
cgroup_pids_peak: false,
// The ABI-focused proof profiles isolate the Filesystem floor; force netns OFF
// so NetworkDenyAll does not enter the ceiling and the FS/Kill coupling tests
// stay focused on exactly their cells.
netns_available: false,
// The ABI-focused proof profiles isolate the FS floor; force seccomp OFF so
// ChildSpawnDenyNewTasks does not enter the ceiling.
seccomp_available: false,
secret_resolver: default_secret_resolver(),
}
}
/// The PRODUCTION ceiling ([`BackendProfile`]) this profile advertises — the
/// per-kind enforcement table the coupling gate scans for `Enforced` cells.
#[must_use]
pub fn proof_ceiling(&self) -> BackendProfile {
self.ceiling()
}
/// The TYPED machine facts the §3
/// [`ProfileFloor`](crate::contract::qualification::ProfileFloor) predicate is checked against
/// (the live ABI integer + whether the cgroup base backs atomic kill / a peak
/// witness). Distinct from the ceiling: the floor is stated over these facts.
#[must_use]
pub fn proof_facts(&self) -> crate::contract::qualification::ProfileFacts {
crate::contract::qualification::ProfileFacts {
landlock_abi: self.landlock_abi,
has_cgroup_kill: self.cgroup_base.is_some(),
has_pids_peak: self.cgroup_pids_peak,
has_unprivileged_userns: self.netns_available,
has_seccomp_filter: self.seccomp_available,
}
}
/// The backend's live mechanism string for a requirement kind at an enforcement
/// level — the digest source the coupling gate matches the ledger against. Builds
/// a representative requirement for the kind so `mechanism(..)` names the
/// primitive (the mechanism is keyed on `RequirementKind::of(req)`, so any
/// representative of the kind yields the same primitive string).
#[must_use]
pub fn proof_mechanism(&self, kind: RequirementKind, enforcement: Enforcement) -> String {
self.mechanism(&representative_requirement(kind), enforcement)
}
}
/// Build a representative [`BoundaryRequirement`] for a [`RequirementKind`] so the
/// backend's `mechanism(..)` can name the primitive. Used ONLY by the coupling
/// proof hook; every cell whose mechanism the ledger commits is covered.
fn representative_requirement(kind: RequirementKind) -> BoundaryRequirement {
use crate::contract::capability::{
Capability, EnvPolicy, FdPolicy, FsAccess, FsConfinement, NetDest, NetPolicy, PathSet,
SpawnPolicy,
};
use crate::contract::host_control::{
CommitDurability, HostControl, KillGuarantee, KillTarget, PathView, StdStreams,
};
match kind {
RequirementKind::Filesystem => BoundaryRequirement::Capability(Capability::Filesystem {
access: FsAccess::Read,
scope: PathSet::empty(),
recursive: true,
confinement: FsConfinement::DeclaredRootsOnly,
}),
RequirementKind::NetworkDenyAll => BoundaryRequirement::Capability(Capability::Network {
policy: NetPolicy::DenyAll,
}),
RequirementKind::NetworkAllowList => BoundaryRequirement::Capability(Capability::Network {
policy: NetPolicy::AllowList(vec![NetDest {
host: "example".to_string(),
port: 443,
}]),
}),
RequirementKind::ChildSpawnDenyNewTasks => {
BoundaryRequirement::Capability(Capability::ChildSpawn {
policy: SpawnPolicy::DenyNewTasks,
})
}
RequirementKind::ChildSpawnAllowThreads => {
BoundaryRequirement::Capability(Capability::ChildSpawn {
policy: SpawnPolicy::AllowThreadsWithinBoundary,
})
}
RequirementKind::ChildSpawnAllowDescendants => {
BoundaryRequirement::Capability(Capability::ChildSpawn {
policy: SpawnPolicy::AllowDescendantsWithinBoundary,
})
}
RequirementKind::Environment => BoundaryRequirement::Capability(Capability::Environment {
policy: EnvPolicy::Exact(Vec::new()),
}),
RequirementKind::InheritedFdsNone => {
BoundaryRequirement::Capability(Capability::InheritedFds {
policy: FdPolicy::None,
})
}
RequirementKind::InheritedFdsOnly => {
BoundaryRequirement::Capability(Capability::InheritedFds {
policy: FdPolicy::Only(vec![3]),
})
}
RequirementKind::LaunchWorkload => {
BoundaryRequirement::HostControl(HostControl::LaunchWorkload)
}
RequirementKind::CaptureStreams => {
BoundaryRequirement::HostControl(HostControl::CaptureStreams {
streams: StdStreams::capture_out_err(),
})
}
RequirementKind::TempRoot => BoundaryRequirement::HostControl(HostControl::TempRoot {
visibility: PathView::PrivateToBoundary,
}),
RequirementKind::ExposePath => BoundaryRequirement::HostControl(HostControl::ExposePath {
source: String::new(),
dest: String::new(),
access: FsAccess::Read,
view: PathView::PrivateToBoundary,
}),
RequirementKind::CommitArtifact => {
BoundaryRequirement::HostControl(HostControl::CommitArtifact {
durability: CommitDurability::Atomic,
})
}
RequirementKind::DiscardArtifact => {
BoundaryRequirement::HostControl(HostControl::DiscardArtifact)
}
RequirementKind::Kill => BoundaryRequirement::HostControl(HostControl::Kill {
target: KillTarget::RunTree,
guarantee: KillGuarantee::Atomic,
}),
RequirementKind::ListOutputs => BoundaryRequirement::HostControl(HostControl::ListOutputs),
}
}