krabka_verified/
opa.rs

1//! OPA authorization-cache admission and error policy.
2//!
3//! All deadlines here are milliseconds on the host's monotonic clock. The
4//! kernels compare and add them; that the clock never steps backwards is a
5//! host responsibility, discharged by reading a `MonotonicClock`.
6
7use creusot_std::prelude::*;
8
9/// Binary authorization result used at the OPA proof boundary.
10#[krabka_macros::model_type]
11pub enum OpaAuthorizationDecision {
12    Allow,
13    Deny,
14}
15
16/// Result of checking one exact-key cache entry.
17#[krabka_macros::model_type]
18pub enum OpaCacheAdmission {
19    Miss,
20    Hit(OpaAuthorizationDecision),
21}
22
23/// Result of computing a monotonic cache deadline.
24#[krabka_macros::model_type]
25pub enum OpaCacheExpiry {
26    DoNotCache,
27    CacheUntil { expires_at_ms: i128 },
28}
29
30/// Reuse an entry's decision only while its deadline is strictly in the
31/// future.
32///
33/// The caller passes only an entry found under the complete authorization
34/// key; the host's hash-map lookup on that key is what makes it an exact
35/// match. The exact deadline is already stale.
36#[ensures(match result {
37    OpaCacheAdmission::Miss => expires_at_ms@ <= now_ms@,
38    OpaCacheAdmission::Hit(decision) => expires_at_ms@ > now_ms@
39        && decision == cached_decision,
40})]
41#[must_use]
42pub fn opa_cache_admission(
43    now_ms: i128,
44    expires_at_ms: i128,
45    cached_decision: OpaAuthorizationDecision,
46) -> OpaCacheAdmission {
47    if expires_at_ms > now_ms {
48        OpaCacheAdmission::Hit(cached_decision)
49    } else {
50        OpaCacheAdmission::Miss
51    }
52}
53
54/// Compute a deadline `ttl_ms` after `now_ms`.
55///
56/// A decision is cached exactly when the TTL is positive and the deadline is
57/// representable: `DoNotCache` iff `ttl_ms <= 0` or `now_ms + ttl_ms`
58/// overflows `i128`.
59#[ensures(match result {
60    OpaCacheExpiry::DoNotCache => ttl_ms@ <= 0 || now_ms@ + ttl_ms@ > i128::MAX@,
61    OpaCacheExpiry::CacheUntil { expires_at_ms } => ttl_ms@ > 0
62        && expires_at_ms@ == now_ms@ + ttl_ms@,
63})]
64#[must_use]
65pub fn opa_cache_expiry(now_ms: i128, ttl_ms: i64) -> OpaCacheExpiry {
66    if ttl_ms <= 0 {
67        return OpaCacheExpiry::DoNotCache;
68    }
69    let Some(expires_at_ms) = now_ms.checked_add(i128::from(ttl_ms)) else {
70        return OpaCacheExpiry::DoNotCache;
71    };
72    OpaCacheExpiry::CacheUntil { expires_at_ms }
73}
74
75/// Map the explicit outage policy without changing successful OPA decisions.
76#[ensures((result == OpaAuthorizationDecision::Allow) == allow_on_error)]
77#[must_use]
78pub fn opa_error_decision(allow_on_error: bool) -> OpaAuthorizationDecision {
79    if allow_on_error {
80        OpaAuthorizationDecision::Allow
81    } else {
82        OpaAuthorizationDecision::Deny
83    }
84}
85
86#[cfg(test)]
87mod tests {
88    use super::{
89        OpaAuthorizationDecision, OpaCacheAdmission, OpaCacheExpiry, opa_cache_admission,
90        opa_cache_expiry, opa_error_decision,
91    };
92
93    #[yare::parameterized(
94        allow_before_expiry = {
95            9,
96            10,
97            OpaAuthorizationDecision::Allow,
98            OpaCacheAdmission::Hit(OpaAuthorizationDecision::Allow),
99        },
100        deny_before_expiry = {
101            9,
102            10,
103            OpaAuthorizationDecision::Deny,
104            OpaCacheAdmission::Hit(OpaAuthorizationDecision::Deny),
105        },
106        exact_expiry = {
107            10,
108            10,
109            OpaAuthorizationDecision::Allow,
110            OpaCacheAdmission::Miss,
111        },
112        after_expiry = {
113            11,
114            10,
115            OpaAuthorizationDecision::Deny,
116            OpaCacheAdmission::Miss,
117        },
118    )]
119    fn cache_requires_strict_freshness(
120        now_ms: i128,
121        expires_at_ms: i128,
122        cached: OpaAuthorizationDecision,
123        expected: OpaCacheAdmission,
124    ) {
125        assert2::check!(opa_cache_admission(now_ms, expires_at_ms, cached) == expected);
126    }
127
128    #[test]
129    fn expiry_and_error_mapping_fail_safely() {
130        assert2::check!(
131            opa_cache_expiry(10, 5) == OpaCacheExpiry::CacheUntil { expires_at_ms: 15 }
132        );
133        assert2::check!(opa_cache_expiry(10, 0) == OpaCacheExpiry::DoNotCache);
134        assert2::check!(opa_cache_expiry(10, -1) == OpaCacheExpiry::DoNotCache);
135        assert2::check!(
136            opa_cache_expiry(i128::MAX - 1, 1)
137                == OpaCacheExpiry::CacheUntil {
138                    expires_at_ms: i128::MAX
139                }
140        );
141        assert2::check!(opa_cache_expiry(i128::MAX, 1) == OpaCacheExpiry::DoNotCache);
142        assert2::check!(
143            opa_error_decision(false) == OpaAuthorizationDecision::Deny
144                && opa_error_decision(true) == OpaAuthorizationDecision::Allow
145        );
146    }
147}
krabka_verified/opa.rs

krabka_verified/
opa.rs
