kernel/
taint.rs

1// This Source Code Form is subject to the terms of the Mozilla Public
2// License, v. 2.0. If a copy of the MPL was not distributed with this
3// file, You can obtain one at https://mozilla.org/MPL/2.0/.
4// Copyright (c) 2026 2youg1 and the sprawling contributors
5
6//! The taint ring. One axiom: external content is
7//! always data. `Tainted::new` is the city-wide sole entrance for foreign
8//! bytes; reads hand out borrows, derivation unions provenance, and no
9//! method ever returns the bare value — "washing it clean" is a compile
10//! error, not a review finding.
11//! The part `crates/kernel/spec/Taint.lean` specifies this module.
12//!
13//! Deliberately absent: serde on `Tainted` (deserialization would be a
14//! second entrance and a forged-empty-taint hole) and any `into_inner`.
15
16use std::collections::BTreeSet;
17
18use serde::{Deserialize, Serialize};
19
20/// Non-empty provenance label, e.g. `web:example.com`, `file:upload`.
21#[derive(Debug, Clone, PartialEq, Eq, PartialOrd, Ord, Serialize, Deserialize)]
22pub struct TaintSource(String);
23
24impl TaintSource {
25    pub fn new(label: impl Into<String>) -> Option<TaintSource> {
26        let label = label.into();
27        if label.is_empty() {
28            None
29        } else {
30            Some(TaintSource(label))
31        }
32    }
33
34    pub fn as_str(&self) -> &str {
35        &self.0
36    }
37}
38
39/// Union semilattice of provenance. Empty means internally produced.
40/// Serializable (event payloads and approval items carry source lists);
41/// order is BTreeSet's, hence deterministic.
42#[derive(Debug, Clone, Default, PartialEq, Eq, Serialize, Deserialize)]
43pub struct TaintSet(BTreeSet<TaintSource>);
44
45impl TaintSet {
46    pub fn empty() -> TaintSet {
47        TaintSet(BTreeSet::new())
48    }
49
50    pub fn of(source: TaintSource) -> TaintSet {
51        let mut set = BTreeSet::new();
52        set.insert(source);
53        TaintSet(set)
54    }
55
56    pub fn union(&self, other: &TaintSet) -> TaintSet {
57        TaintSet(self.0.union(&other.0).cloned().collect())
58    }
59
60    pub fn is_empty(&self) -> bool {
61        self.0.is_empty()
62    }
63
64    pub fn contains(&self, source: &TaintSource) -> bool {
65        self.0.contains(source)
66    }
67
68    pub fn len(&self) -> usize {
69        self.0.len()
70    }
71
72    pub fn sources(&self) -> impl Iterator<Item = &TaintSource> {
73        self.0.iter()
74    }
75}
76
77/// The sources, comma-separated in the set's order: the one wording
78/// every C15 refusal uses to say where a run's content came from.
79impl std::fmt::Display for TaintSet {
80    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
81        self.0.iter().enumerate().try_for_each(|(at, source)| {
82            let comma = if at == 0 { "" } else { ", " };
83            write!(f, "{comma}{}", source.as_str())
84        })
85    }
86}
87
88/// External content with its provenance welded on. The value is private;
89/// `peek` lends, `map`/`join` derive with automatic union, and nothing
90/// returns `T` by value.
91#[derive(Debug, Clone, PartialEq, Eq)]
92pub struct Tainted<T> {
93    value: T,
94    taint: TaintSet,
95}
96
97impl<T> Tainted<T> {
98    /// City-wide sole entrance for external content. Custody (secret scan
99    /// before CAS) composes at this call site in the effect layer;
100    /// the type itself stays pure.
101    pub fn new(value: T, source: TaintSource) -> Tainted<T> {
102        Tainted {
103            value,
104            taint: TaintSet::of(source),
105        }
106    }
107
108    /// Borrow the content: you can read it, you cannot walk away with it.
109    pub fn peek(&self) -> &T {
110        &self.value
111    }
112
113    pub fn taint(&self) -> &TaintSet {
114        &self.taint
115    }
116
117    /// Derivation keeps the full provenance. The closure borrows — moving
118    /// the value out through it cannot be spelled.
119    pub fn map<U>(self, f: impl FnOnce(&T) -> U) -> Tainted<U> {
120        Tainted {
121            value: f(&self.value),
122            taint: self.taint,
123        }
124    }
125
126    /// Two-source derivation: the result carries the union.
127    pub fn join<U, V>(self, other: Tainted<U>, f: impl FnOnce(&T, &U) -> V) -> Tainted<V> {
128        Tainted {
129            value: f(&self.value, &other.value),
130            taint: self.taint.union(&other.taint),
131        }
132    }
133}
134
135// No kani harness lives here. Union monotonicity is a proposition about
136// a `BTreeSet` of `String`s, which gives CBMC loops it cannot bound, and
137// a harness over two fixed labels would only restate the proptest below
138// over a narrower domain (`crates/kernel/Spec.lean` §2).
139
140#[cfg(test)]
141#[allow(
142    clippy::unwrap_used,
143    clippy::expect_used,
144    clippy::panic,
145    clippy::indexing_slicing,
146    reason = "test code"
147)]
148mod tests {
149    use super::*;
150    use proptest::prelude::*;
151
152    fn source(label: &str) -> TaintSource {
153        TaintSource::new(label).unwrap()
154    }
155
156    #[test]
157    fn empty_label_is_not_a_source() {
158        assert!(TaintSource::new("").is_none());
159    }
160
161    #[test]
162    fn map_keeps_the_full_set_and_join_unions() {
163        let web = Tainted::new("body".to_owned(), source("web:example.com"));
164        let derived = web.map(|s| s.len());
165        assert_eq!(derived.taint().len(), 1);
166        let upload = Tainted::new(3usize, source("file:upload"));
167        let joined = derived.join(upload, |a, b| a.saturating_add(*b));
168        assert_eq!(*joined.peek(), 7);
169        assert!(joined.taint().contains(&source("web:example.com")));
170        assert!(joined.taint().contains(&source("file:upload")));
171    }
172
173    #[test]
174    fn peek_lends_without_moving() {
175        let tainted = Tainted::new(vec![1u8, 2], source("mail:inbound"));
176        assert_eq!(tainted.peek().len(), 2);
177        // Still usable afterwards: peek did not consume.
178        assert_eq!(tainted.taint().len(), 1);
179    }
180
181    proptest! {
182        /// The kani mirror (union monotonicity), runnable on every host.
183        #[test]
184        fn join_output_contains_both_inputs(labels_a in proptest::collection::vec("[a-z]{1,8}", 1..4),
185                                            labels_b in proptest::collection::vec("[a-z]{1,8}", 1..4)) {
186            let mut a = Tainted::new(0u32, source(&format!("a:{}", labels_a[0])));
187            for label in &labels_a[1..] {
188                let extra = Tainted::new(1u32, source(&format!("a:{label}")));
189                a = a.join(extra, |x, y| x.saturating_add(*y));
190            }
191            let mut b = Tainted::new(0u32, source(&format!("b:{}", labels_b[0])));
192            for label in &labels_b[1..] {
193                let extra = Tainted::new(1u32, source(&format!("b:{label}")));
194                b = b.join(extra, |x, y| x.saturating_add(*y));
195            }
196            let a_set = a.taint().clone();
197            let b_set = b.taint().clone();
198            let joined = a.join(b, |x, y| x.saturating_add(*y));
199            for s in a_set.sources() {
200                prop_assert!(joined.taint().contains(s));
201            }
202            for s in b_set.sources() {
203                prop_assert!(joined.taint().contains(s));
204            }
205            prop_assert_eq!(joined.taint().len(), a_set.union(&b_set).len());
206        }
207    }
208}
kernel/taint.rs

kernel/
taint.rs
