1use std::collections::{BTreeMap, BTreeSet};
8
9use serde::{Deserialize, Serialize};
10
11use crate::canonical::{CanonicalExecutable, CanonicalNetworkEndpoint, CanonicalPath, OpenIntent};
12use crate::{FileOperation, SpawnMechanism};
13
14pub const SEMANTICS_V3_PROTOTYPE_SCHEMA_VERSION: u32 = 3;
15
16#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Serialize, Deserialize)]
17#[serde(rename_all = "snake_case")]
18pub enum FdTableRelationState {
19 Shared,
20 IndependentCopy,
21 Unknown,
22}
23
24#[derive(Debug, Clone, PartialEq, Eq, PartialOrd, Ord, Serialize, Deserialize)]
25#[serde(tag = "proposition_kind", rename_all = "snake_case")]
26pub enum Proposition {
27 ProcessChildCreated {
28 actor: Option<CanonicalExecutable>,
29 mechanism: SpawnMechanism,
30 },
31 ProcessExecSucceeded {
32 from: Option<CanonicalExecutable>,
33 executable: CanonicalExecutable,
34 },
35 CausalExecLineageObserved {
36 execution_chain: Vec<CanonicalExecutable>,
37 },
38 FilePathnameAttemptObserved {
39 actor: Option<CanonicalExecutable>,
40 execution_chain: Vec<CanonicalExecutable>,
41 operation: FileOperation,
42 target: CanonicalPath,
43 open_intent: Option<OpenIntent>,
44 },
45 FileOpenObjectObserved {
46 actor: Option<CanonicalExecutable>,
47 execution_chain: Vec<CanonicalExecutable>,
48 target: CanonicalPath,
49 },
50 FileFdEffectObserved {
51 actor: Option<CanonicalExecutable>,
52 execution_chain: Vec<CanonicalExecutable>,
53 operation: FileOperation,
54 target: CanonicalPath,
55 },
56 FileRenameAttemptObserved {
57 actor: Option<CanonicalExecutable>,
58 execution_chain: Vec<CanonicalExecutable>,
59 from: CanonicalPath,
60 to: CanonicalPath,
61 },
62 NetworkConnectDestinationAttemptObserved {
63 actor: Option<CanonicalExecutable>,
64 execution_chain: Vec<CanonicalExecutable>,
65 endpoint: CanonicalNetworkEndpoint,
66 },
67 ObserverHealthObserved {
68 complete: bool,
69 warning_codes: BTreeSet<String>,
70 },
71 FdTableRelationObserved {
72 actor: Option<CanonicalExecutable>,
73 mechanism: SpawnMechanism,
74 relation: FdTableRelationState,
75 },
76}
77
78#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Serialize, Deserialize)]
79#[serde(rename_all = "snake_case")]
80pub enum ObservationPoint {
81 UserspaceArgumentPreKernel,
82 PtraceLifecycleEvent,
83 SyscallResultPostOperation,
84 DerivedRuntimeFdState,
85 KernelSecurityHook,
86 KernelTracepoint,
87 ImportedAttestedTrace,
88}
89
90#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Serialize, Deserialize)]
91#[serde(rename_all = "snake_case")]
92pub enum IdentityBasis {
93 None,
94 LexicalArgument,
95 TraceTimeDirfdResolvedArgument,
96 RuntimeFdPathCorrelated,
97 KernelObjectGrounded,
98 SocketAddressArgument,
99}
100
101#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Serialize, Deserialize)]
102#[serde(rename_all = "snake_case")]
103pub enum TemporalBinding {
104 PreOperationIntent,
105 SuccessfulOperationResult,
106 PostOperationDerivedState,
107 KernelDecisionPoint,
108 LifecycleTransition,
109}
110
111#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Serialize, Deserialize)]
112#[serde(rename_all = "snake_case")]
113pub enum CausalBinding {
114 DirectEvent,
115 StateMachineCorrelated,
116 LineageDerived,
117}
118
119#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize, Default)]
120pub struct EvidenceGuarantees {
121 pub observation_points: BTreeSet<ObservationPoint>,
122 pub identity_bases: BTreeSet<IdentityBasis>,
123 pub temporal_bindings: BTreeSet<TemporalBinding>,
124 pub causal_bindings: BTreeSet<CausalBinding>,
125}
126
127impl EvidenceGuarantees {
128 pub fn entails(&self, required: &Self) -> bool {
129 required
130 .observation_points
131 .is_subset(&self.observation_points)
132 && required.identity_bases.is_subset(&self.identity_bases)
133 && required
134 .temporal_bindings
135 .is_subset(&self.temporal_bindings)
136 && required.causal_bindings.is_subset(&self.causal_bindings)
137 }
138
139 fn is_empty(&self) -> bool {
140 self.observation_points.is_empty()
141 && self.identity_bases.is_empty()
142 && self.temporal_bindings.is_empty()
143 && self.causal_bindings.is_empty()
144 }
145}
146
147#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Serialize, Deserialize)]
148#[serde(rename_all = "snake_case")]
149pub enum CompletenessDimension {
150 SessionScope,
151 Lifecycle,
152 Transport,
153 ResourceBudget,
154 Capability,
155 ObjectIdentity,
156 FdTableRelation,
157 CausalLineage,
158}
159
160#[derive(Debug, Clone, PartialEq, Eq, PartialOrd, Ord, Serialize, Deserialize)]
161#[serde(tag = "state", rename_all = "snake_case")]
162pub enum CompletenessState {
163 NotRequired,
164 Complete,
165 Incomplete { reason_code: String },
166 Ambiguous { reason_code: String },
167 Unsupported { reason_code: String },
168}
169
170#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize, Default)]
171pub struct ProofRequirement {
172 #[serde(default)]
173 pub expected_proposition: Option<Proposition>,
174 pub guarantees: EvidenceGuarantees,
175 pub required_complete: BTreeSet<CompletenessDimension>,
176}
177
178impl ProofRequirement {
179 pub fn for_proposition(
180 proposition: Proposition,
181 guarantees: EvidenceGuarantees,
182 required_complete: BTreeSet<CompletenessDimension>,
183 ) -> Self {
184 Self {
185 expected_proposition: Some(proposition),
186 guarantees,
187 required_complete,
188 }
189 }
190
191 fn is_non_vacuous(&self) -> bool {
192 self.expected_proposition.is_some()
193 && (!self.guarantees.is_empty() || !self.required_complete.is_empty())
194 }
195}
196
197#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
198pub struct BackendSemanticProfile {
199 pub name: String,
200 pub semantic_profile_version: u32,
201}
202
203#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
204pub struct ProofCarryingObservation {
205 pub schema_version: u32,
206 pub proposition: Proposition,
207 pub guarantees: EvidenceGuarantees,
208 pub completeness: BTreeMap<CompletenessDimension, CompletenessState>,
209 pub backend_profile: BackendSemanticProfile,
210 pub ambiguity_codes: BTreeSet<String>,
211}
212
213impl ProofCarryingObservation {
214 pub fn new(
215 proposition: Proposition,
216 guarantees: EvidenceGuarantees,
217 backend_profile: BackendSemanticProfile,
218 ) -> Self {
219 Self {
220 schema_version: SEMANTICS_V3_PROTOTYPE_SCHEMA_VERSION,
221 proposition,
222 guarantees,
223 completeness: BTreeMap::new(),
224 backend_profile,
225 ambiguity_codes: BTreeSet::new(),
226 }
227 }
228
229 fn ambiguity_invalidates(&self, requirement: &ProofRequirement) -> bool {
230 for code in &self.ambiguity_codes {
231 match code.as_str() {
232 "object_identity_conflict" => {
233 if requirement
234 .required_complete
235 .contains(&CompletenessDimension::ObjectIdentity)
236 {
237 return true;
238 }
239 }
240 _ => {
241 return true;
243 }
244 }
245 }
246 false
247 }
248
249 pub fn satisfies(&self, requirement: &ProofRequirement) -> bool {
250 if self.schema_version != SEMANTICS_V3_PROTOTYPE_SCHEMA_VERSION {
251 return false;
252 }
253 if !requirement.is_non_vacuous() {
254 return false;
255 }
256 if requirement.expected_proposition.as_ref() != Some(&self.proposition) {
257 return false;
258 }
259 if !self.guarantees.entails(&requirement.guarantees) {
260 return false;
261 }
262 if self.ambiguity_invalidates(requirement) {
263 return false;
264 }
265 requirement
266 .required_complete
267 .iter()
268 .all(|dimension| self.completeness.get(dimension) == Some(&CompletenessState::Complete))
269 }
270}
271
272#[cfg(test)]
273mod tests {
274 use super::*;
275 use crate::canonical::{PathClass, PathResolution};
276
277 fn target_path() -> CanonicalPath {
278 CanonicalPath {
279 value: "$WORKSPACE/input.txt".to_owned(),
280 class: PathClass::Workspace,
281 resolution: PathResolution::Lexical,
282 }
283 }
284
285 fn pathname_attempt() -> Proposition {
286 Proposition::FilePathnameAttemptObserved {
287 actor: None,
288 execution_chain: vec![],
289 operation: FileOperation::Open,
290 target: target_path(),
291 open_intent: None,
292 }
293 }
294
295 fn ptrace_argument_guarantees() -> EvidenceGuarantees {
296 EvidenceGuarantees {
297 observation_points: BTreeSet::from([ObservationPoint::UserspaceArgumentPreKernel]),
298 identity_bases: BTreeSet::from([IdentityBasis::LexicalArgument]),
299 temporal_bindings: BTreeSet::from([TemporalBinding::PreOperationIntent]),
300 causal_bindings: BTreeSet::from([CausalBinding::DirectEvent]),
301 }
302 }
303
304 fn requirement_for(
305 guarantees: EvidenceGuarantees,
306 required_complete: BTreeSet<CompletenessDimension>,
307 ) -> ProofRequirement {
308 ProofRequirement::for_proposition(pathname_attempt(), guarantees, required_complete)
309 }
310
311 fn base_record() -> ProofCarryingObservation {
312 let mut record = ProofCarryingObservation::new(
313 pathname_attempt(),
314 ptrace_argument_guarantees(),
315 BackendSemanticProfile {
316 name: "linux-ptrace-semantics-v3-prototype".to_owned(),
317 semantic_profile_version: 1,
318 },
319 );
320 record.completeness.insert(
321 CompletenessDimension::SessionScope,
322 CompletenessState::Complete,
323 );
324 record.completeness.insert(
325 CompletenessDimension::Lifecycle,
326 CompletenessState::Complete,
327 );
328 record
329 }
330
331 #[test]
332 fn weak_path_argument_does_not_entail_kernel_object_grounding() {
333 let record = base_record();
334 let requirement = requirement_for(
335 EvidenceGuarantees {
336 identity_bases: BTreeSet::from([IdentityBasis::KernelObjectGrounded]),
337 ..EvidenceGuarantees::default()
338 },
339 BTreeSet::new(),
340 );
341
342 assert!(!record.satisfies(&requirement));
343 }
344
345 #[test]
346 fn ambiguity_blocks_required_completeness() {
347 let mut record = base_record();
348 record.completeness.insert(
349 CompletenessDimension::ObjectIdentity,
350 CompletenessState::Ambiguous {
351 reason_code: "shared_fd_table_ambiguity".to_owned(),
352 },
353 );
354 let requirement = requirement_for(
355 ptrace_argument_guarantees(),
356 BTreeSet::from([
357 CompletenessDimension::SessionScope,
358 CompletenessDimension::ObjectIdentity,
359 ]),
360 );
361
362 assert!(!record.satisfies(&requirement));
363 }
364
365 #[test]
366 fn exact_required_guarantees_and_completeness_are_admissible() {
367 let record = base_record();
368 let requirement = requirement_for(
369 ptrace_argument_guarantees(),
370 BTreeSet::from([
371 CompletenessDimension::SessionScope,
372 CompletenessDimension::Lifecycle,
373 ]),
374 );
375
376 assert!(record.satisfies(&requirement));
377 }
378
379 #[test]
380 fn default_requirement_fails_closed() {
381 let record = base_record();
382 assert!(!record.satisfies(&ProofRequirement::default()));
383 }
384
385 #[test]
386 fn proposition_mismatch_fails_closed() {
387 let record = base_record();
388 let mut wrong = pathname_attempt();
389 if let Proposition::FilePathnameAttemptObserved { target, .. } = &mut wrong {
390 target.value = "$WORKSPACE/other.txt".to_owned();
391 }
392 let requirement = ProofRequirement::for_proposition(
393 wrong,
394 ptrace_argument_guarantees(),
395 BTreeSet::from([CompletenessDimension::SessionScope]),
396 );
397 assert!(!record.satisfies(&requirement));
398 }
399
400 #[test]
401 fn explicit_object_identity_conflict_blocks_complete_claim() {
402 let mut record = base_record();
403 record.completeness.insert(
404 CompletenessDimension::ObjectIdentity,
405 CompletenessState::Complete,
406 );
407 record
408 .ambiguity_codes
409 .insert("object_identity_conflict".to_owned());
410 let requirement = requirement_for(
411 ptrace_argument_guarantees(),
412 BTreeSet::from([CompletenessDimension::ObjectIdentity]),
413 );
414 assert!(!record.satisfies(&requirement));
415 }
416
417 #[test]
418 fn unknown_ambiguity_code_fails_closed_for_admission() {
419 let mut record = base_record();
420 record
421 .ambiguity_codes
422 .insert("unrecognized_future_ambiguity".to_owned());
423 let requirement = requirement_for(
424 ptrace_argument_guarantees(),
425 BTreeSet::from([CompletenessDimension::SessionScope]),
426 );
427 assert!(!record.satisfies(&requirement));
428 }
429
430 #[test]
431 fn deterministic_serialization_is_independent_of_set_insertion_order() {
432 let mut first = base_record();
433 first.ambiguity_codes.insert("zeta".to_owned());
434 first.ambiguity_codes.insert("alpha".to_owned());
435
436 let mut second = base_record();
437 second.ambiguity_codes.insert("alpha".to_owned());
438 second.ambiguity_codes.insert("zeta".to_owned());
439
440 assert_eq!(
441 serde_json::to_vec(&first).expect("serialize first"),
442 serde_json::to_vec(&second).expect("serialize second")
443 );
444 }
445
446 #[test]
447 fn same_canonical_value_with_different_authority_is_not_equal_evidence() {
448 let first = base_record();
449 let mut second = base_record();
450 second
451 .guarantees
452 .identity_bases
453 .insert(IdentityBasis::KernelObjectGrounded);
454
455 assert_ne!(first, second);
456 }
457
458 #[test]
459 fn fd_table_relation_unknown_is_first_class_proposition_state() {
460 let proposition = Proposition::FdTableRelationObserved {
461 actor: None,
462 mechanism: SpawnMechanism::Clone,
463 relation: FdTableRelationState::Unknown,
464 };
465 let encoded = serde_json::to_vec(&proposition).expect("serialize fd-table relation");
466 let decoded: Proposition =
467 serde_json::from_slice(&encoded).expect("deserialize fd-table relation");
468 assert_eq!(decoded, proposition);
469 }
470
471 #[test]
472 fn observer_health_warning_codes_serialize_deterministically() {
473 let first = Proposition::ObserverHealthObserved {
474 complete: false,
475 warning_codes: BTreeSet::from(["zeta".to_owned(), "alpha".to_owned()]),
476 };
477 let second = Proposition::ObserverHealthObserved {
478 complete: false,
479 warning_codes: BTreeSet::from(["alpha".to_owned(), "zeta".to_owned()]),
480 };
481 assert_eq!(
482 serde_json::to_vec(&first).expect("serialize first health proposition"),
483 serde_json::to_vec(&second).expect("serialize second health proposition")
484 );
485 }
486}