krabka_verified/
worm.rs

1//! Admission decisions for signed WORM manifests and their object sets.
2
3use creusot_std::prelude::ensures;
4#[cfg(creusot)]
5use creusot_std::prelude::{DeepModel, logic};
6
7/// Why a manifest signature is not an accepted attestation.
8#[krabka_macros::model_type(proof(DeepModel), runtime(Debug, Clone, Copy, PartialEq, Eq))]
9pub enum WormSignatureDecision {
10    Unsigned,
11    Untrusted,
12    Invalid,
13    Admit,
14}
15
16/// Requires a present signature, an externally trusted key, and verification
17/// against the canonical manifest signing bytes.
18#[ensures(!present ==> result == WormSignatureDecision::Unsigned)]
19#[ensures(present && !trusted ==> result == WormSignatureDecision::Untrusted)]
20#[ensures(present && trusted && !canonical_valid
21    ==> result == WormSignatureDecision::Invalid)]
22#[ensures(present && trusted && canonical_valid
23    ==> result == WormSignatureDecision::Admit)]
24#[must_use]
25pub fn worm_signature_decision(
26    present: bool,
27    trusted: bool,
28    canonical_valid: bool,
29) -> WormSignatureDecision {
30    if !present {
31        WormSignatureDecision::Unsigned
32    } else if !trusted {
33        WormSignatureDecision::Untrusted
34    } else if !canonical_valid {
35        WormSignatureDecision::Invalid
36    } else {
37        WormSignatureDecision::Admit
38    }
39}
40
41/// Why the objects named by one manifest are not an exact archive set.
42#[krabka_macros::model_type(proof(DeepModel), runtime(Debug, Clone, Copy, PartialEq, Eq))]
43pub enum WormObjectSetDecision {
44    Empty,
45    DuplicateKey,
46    CoordinateMismatch,
47    MissingObject,
48    CountMismatch,
49    SizeMismatch,
50    DigestMismatch,
51    Admit,
52}
53
54/// Host observations about the objects belonging to one signed segment.
55#[krabka_macros::model_type(proof(DeepModel), runtime(Debug, Clone, Copy, PartialEq, Eq))]
56pub struct WormObjectIdentityFacts {
57    pub unique_keys: bool,
58    pub coordinates_match: bool,
59}
60
61#[krabka_macros::model_type(proof(DeepModel), runtime(Debug, Clone, Copy, PartialEq, Eq))]
62pub struct WormObjectAvailabilityFacts {
63    pub all_present: bool,
64    pub sizes_match: bool,
65}
66
67#[krabka_macros::model_type(proof(DeepModel), runtime(Debug, Clone, Copy, PartialEq, Eq))]
68pub struct WormDigestFacts {
69    pub require_digests: bool,
70    pub digests_match: bool,
71}
72
73#[krabka_macros::model_type(proof(DeepModel), runtime(Debug, Clone, Copy, PartialEq, Eq))]
74pub struct WormObjectSetFacts {
75    pub object_count: u64,
76    pub listed_count: u64,
77    pub identity: WormObjectIdentityFacts,
78    pub availability: WormObjectAvailabilityFacts,
79    pub digests: WormDigestFacts,
80}
81
82krabka_macros::worm_object_set! {
83    Model;
84{
85    /// The object-set rule, as the first failed check in diagnostic order: an
86    /// empty set, a repeated key, a key at the wrong coordinates, an object the
87    /// store does not hold, a listing with another object count, an object of
88    /// another size, and, when digests are required, a digest mismatch. A set
89    /// that passes every check is `Admit`.
90    // cargo-mutants: #[cfg(creusot)] spec function; not compiled outside Creusot, so no test can tell.
91    #[cfg(creusot)]
92    #[cfg_attr(test, mutants::skip)]
93    #[logic]
94    fn worm_object_set_model(facts: WormObjectSetFacts) -> WormObjectSetDecision
95}
96(facts);
97    count [facts.object_count@] listed [facts.listed_count@]
98}
99
100krabka_macros::worm_object_set! {
101    Runtime;
102{
103    /// Requires a nonempty, one-to-one object set with exact coordinates, sizes,
104    /// and, when requested, digests; see `worm_object_set_model`.
105    #[ensures(result == worm_object_set_model(facts))]
106    #[must_use]
107    pub fn worm_object_set_decision(facts: WormObjectSetFacts) -> WormObjectSetDecision
108}
109(facts);
110    count [facts.object_count] listed [facts.listed_count]
111}
112
113#[cfg(test)]
114mod tests {
115    use {
116        super::{
117            WormDigestFacts, WormObjectAvailabilityFacts, WormObjectIdentityFacts,
118            WormObjectSetDecision, WormObjectSetFacts, WormSignatureDecision,
119            worm_object_set_decision, worm_signature_decision,
120        },
121        assert2::assert,
122    };
123
124    #[test]
125    fn signatures_require_every_attestation_fact() {
126        assert!(worm_signature_decision(false, true, true) == WormSignatureDecision::Unsigned);
127        assert!(worm_signature_decision(true, false, true) == WormSignatureDecision::Untrusted);
128        assert!(worm_signature_decision(true, true, false) == WormSignatureDecision::Invalid);
129        assert!(worm_signature_decision(true, true, true) == WormSignatureDecision::Admit);
130    }
131
132    fn exact_object_set() -> WormObjectSetFacts {
133        WormObjectSetFacts {
134            object_count: 1,
135            listed_count: 1,
136            identity: WormObjectIdentityFacts {
137                unique_keys: true,
138                coordinates_match: true,
139            },
140            availability: WormObjectAvailabilityFacts {
141                all_present: true,
142                sizes_match: true,
143            },
144            digests: WormDigestFacts {
145                require_digests: true,
146                digests_match: true,
147            },
148        }
149    }
150
151    fn broken_object_set() -> WormObjectSetFacts {
152        // Every refusal also fails the checks after it, so each row shows the
153        // earlier check outranking the later ones.
154        WormObjectSetFacts {
155            object_count: 1,
156            listed_count: 2,
157            identity: WormObjectIdentityFacts {
158                unique_keys: false,
159                coordinates_match: false,
160            },
161            availability: WormObjectAvailabilityFacts {
162                all_present: false,
163                sizes_match: false,
164            },
165            digests: WormDigestFacts {
166                require_digests: true,
167                digests_match: false,
168            },
169        }
170    }
171
172    #[yare::parameterized(
173        empty = {
174            "an empty set",
175            WormObjectSetFacts { object_count: 0, listed_count: 0, ..broken_object_set() },
176            WormObjectSetDecision::Empty
177        },
178        duplicate_key = {
179            "a repeated key",
180            broken_object_set(),
181            WormObjectSetDecision::DuplicateKey,
182        },
183        coordinate_mismatch = {
184            "a key at the wrong coordinates",
185            WormObjectSetFacts {
186                identity: WormObjectIdentityFacts {
187                    unique_keys: true,
188                    coordinates_match: false,
189                },
190                ..broken_object_set()
191            },
192            WormObjectSetDecision::CoordinateMismatch,
193        },
194        missing_object = {
195            "a missing object",
196            WormObjectSetFacts {
197                identity: WormObjectIdentityFacts {
198                    unique_keys: true,
199                    coordinates_match: true,
200                },
201                ..broken_object_set()
202            },
203            WormObjectSetDecision::MissingObject,
204        },
205        count_mismatch = {
206            "another object count",
207            WormObjectSetFacts {
208                identity: WormObjectIdentityFacts {
209                    unique_keys: true,
210                    coordinates_match: true,
211                },
212                availability: WormObjectAvailabilityFacts {
213                    all_present: true,
214                    sizes_match: false,
215                },
216                ..broken_object_set()
217            },
218            WormObjectSetDecision::CountMismatch,
219        },
220        size_mismatch = {
221            "another object size",
222            WormObjectSetFacts {
223                identity: WormObjectIdentityFacts {
224                    unique_keys: true,
225                    coordinates_match: true,
226                },
227                availability: WormObjectAvailabilityFacts {
228                    all_present: true,
229                    sizes_match: false,
230                },
231                listed_count: 1,
232                ..broken_object_set()
233            },
234            WormObjectSetDecision::SizeMismatch,
235        },
236        required_digest_mismatch = {
237            "a required digest mismatch",
238            WormObjectSetFacts {
239                digests: WormDigestFacts {
240                    require_digests: true,
241                    digests_match: false,
242                },
243                ..exact_object_set()
244            },
245            WormObjectSetDecision::DigestMismatch,
246        },
247        optional_digest_mismatch = {
248            "a digest mismatch nobody required",
249            WormObjectSetFacts {
250                digests: WormDigestFacts {
251                    require_digests: false,
252                    digests_match: false,
253                },
254                ..exact_object_set()
255            },
256            WormObjectSetDecision::Admit,
257        },
258        exact = { "an exact set", exact_object_set(), WormObjectSetDecision::Admit },
259    )]
260    fn object_sets_fail_closed_in_diagnostic_order(
261        what: &'static str,
262        facts: WormObjectSetFacts,
263        expected: WormObjectSetDecision,
264    ) {
265        assert2::assert!(worm_object_set_decision(facts) == expected, "{what}");
266    }
267}
krabka_verified/worm.rs

krabka_verified/
worm.rs
