krabka_verified/
oauth.rs

1//! OAuth session-lifetime and reauthentication admission.
2
3use creusot_std::prelude::ensures;
4#[cfg(creusot)]
5use creusot_std::prelude::{DeepModel, Int, logic};
6
7/// Whether token validation supplied an absolute expiry.
8#[krabka_macros::model_type]
9pub enum OAuthExpiryPresence {
10    Missing,
11    Present,
12}
13
14/// Whether the broker applies a maximum session lifetime.
15#[krabka_macros::model_type]
16pub enum OAuthSessionCap {
17    Disabled,
18    Enabled,
19}
20
21/// Authentication phase being admitted.
22#[krabka_macros::model_type]
23pub enum OAuthAuthenticationKind {
24    Initial,
25    Reauthentication,
26}
27
28/// Relationship between the prior and validated principals.
29#[krabka_macros::model_type]
30pub enum OAuthPrincipalMatch {
31    Matches,
32    Differs,
33}
34
35/// Inputs that bind a validated token to one broker session.
36#[krabka_macros::model_type]
37pub struct OAuthSessionFacts {
38    pub expiry: OAuthExpiryPresence,
39    pub token_expires_at_ms: i64,
40    pub now_ms: i64,
41    pub cap: OAuthSessionCap,
42    pub cap_ms: i64,
43    pub authentication: OAuthAuthenticationKind,
44    pub principal: OAuthPrincipalMatch,
45}
46
47/// Session state selected after token validation.
48#[krabka_macros::model_type]
49pub enum OAuthSessionDecision {
50    Reject,
51    Admit {
52        session_lifetime_ms: i64,
53        effective_expires_at_ms: i64,
54    },
55}
56
57// cargo-mutants: #[cfg(creusot)] spec function; not compiled outside Creusot, so no test can tell.
58#[cfg(creusot)]
59#[cfg_attr(test, mutants::skip)]
60#[logic(open)]
61/// Session admissibility at the clock when token validation completes.
62pub(crate) fn oauth_session_admissible_at(facts: OAuthSessionFacts, now: Int) -> bool {
63    pearlite! {
64        facts.expiry == OAuthExpiryPresence::Present
65            && facts.token_expires_at_ms@ > now
66            && facts.token_expires_at_ms@ - now <= i64::MAX@
67            && (facts.cap == OAuthSessionCap::Disabled || facts.cap_ms@ > 0)
68            && (facts.authentication == OAuthAuthenticationKind::Initial
69                || facts.principal == OAuthPrincipalMatch::Matches)
70    }
71}
72
73/// Whether a validated token may bind a session: it carries an expiry
74/// strictly in the future, its remaining lifetime fits an `i64`, an enabled
75/// cap is positive, and a reauthentication keeps the prior principal
76/// (KIP-368).
77// cargo-mutants: #[cfg(creusot)] spec function; not compiled outside Creusot, so no test can tell.
78#[cfg(creusot)]
79#[cfg_attr(test, mutants::skip)]
80#[logic(open(crate))]
81pub fn oauth_session_admissible(facts: OAuthSessionFacts) -> bool {
82    pearlite! { oauth_session_admissible_at(facts, facts.now_ms@) }
83}
84
85/// The session lifetime: the token's remaining lifetime, bounded above by an
86/// enabled cap.
87// cargo-mutants: #[cfg(creusot)] spec function; not compiled outside Creusot, so no test can tell.
88#[cfg(creusot)]
89#[cfg_attr(test, mutants::skip)]
90#[logic(open(crate))]
91pub fn oauth_session_lifetime(facts: OAuthSessionFacts) -> Int {
92    pearlite! {
93        let token_lifetime = facts.token_expires_at_ms@ - facts.now_ms@;
94        if facts.cap == OAuthSessionCap::Enabled && facts.cap_ms@ < token_lifetime {
95            facts.cap_ms@
96        } else {
97            token_lifetime
98        }
99    }
100}
101
102/// Admit exactly the admissible sessions, with the smaller of the token
103/// lifetime and the enabled cap, and the matching absolute expiry.
104#[ensures(match result {
105    OAuthSessionDecision::Reject => !oauth_session_admissible(facts),
106    OAuthSessionDecision::Admit {
107        session_lifetime_ms,
108        effective_expires_at_ms,
109    } => oauth_session_admissible(facts)
110        && session_lifetime_ms@ == oauth_session_lifetime(facts)
111        && effective_expires_at_ms@ == facts.now_ms@ + session_lifetime_ms@,
112})]
113#[must_use]
114pub fn oauth_session_admission(facts: OAuthSessionFacts) -> OAuthSessionDecision {
115    if matches!(facts.expiry, OAuthExpiryPresence::Missing) {
116        return OAuthSessionDecision::Reject;
117    }
118    if facts.token_expires_at_ms <= facts.now_ms {
119        return OAuthSessionDecision::Reject;
120    }
121    if matches!(
122        (facts.authentication, facts.principal),
123        (
124            OAuthAuthenticationKind::Reauthentication,
125            OAuthPrincipalMatch::Differs
126        )
127    ) {
128        return OAuthSessionDecision::Reject;
129    }
130    if matches!(facts.cap, OAuthSessionCap::Enabled) && facts.cap_ms <= 0 {
131        return OAuthSessionDecision::Reject;
132    }
133    let Some(token_lifetime_ms) = facts.token_expires_at_ms.checked_sub(facts.now_ms) else {
134        return OAuthSessionDecision::Reject;
135    };
136    let session_lifetime_ms = match facts.cap {
137        OAuthSessionCap::Enabled => token_lifetime_ms.min(facts.cap_ms),
138        OAuthSessionCap::Disabled => token_lifetime_ms,
139    };
140    let Some(effective_expires_at_ms) = facts.now_ms.checked_add(session_lifetime_ms) else {
141        return OAuthSessionDecision::Reject;
142    };
143    OAuthSessionDecision::Admit {
144        session_lifetime_ms,
145        effective_expires_at_ms,
146    }
147}
148
149#[cfg(test)]
150mod tests {
151    use super::{
152        OAuthAuthenticationKind, OAuthExpiryPresence, OAuthPrincipalMatch, OAuthSessionCap,
153        OAuthSessionDecision, OAuthSessionFacts, oauth_session_admission,
154    };
155
156    fn facts() -> OAuthSessionFacts {
157        OAuthSessionFacts {
158            expiry: OAuthExpiryPresence::Present,
159            token_expires_at_ms: 1_100,
160            now_ms: 1_000,
161            cap: OAuthSessionCap::Disabled,
162            cap_ms: 0,
163            authentication: OAuthAuthenticationKind::Initial,
164            principal: OAuthPrincipalMatch::Matches,
165        }
166    }
167
168    #[yare::parameterized(
169        default_lifetime = {
170            facts(),
171            OAuthSessionDecision::Admit { session_lifetime_ms: 100, effective_expires_at_ms: 1_100 },
172        },
173        capped_lifetime = {
174            OAuthSessionFacts { cap: OAuthSessionCap::Enabled, cap_ms: 40, ..facts() },
175            OAuthSessionDecision::Admit { session_lifetime_ms: 40, effective_expires_at_ms: 1_040 },
176        },
177        longer_cap = {
178            OAuthSessionFacts { cap: OAuthSessionCap::Enabled, cap_ms: 500, ..facts() },
179            OAuthSessionDecision::Admit { session_lifetime_ms: 100, effective_expires_at_ms: 1_100 },
180        },
181        same_principal_reauthentication = {
182            OAuthSessionFacts { authentication: OAuthAuthenticationKind::Reauthentication, ..facts() },
183            OAuthSessionDecision::Admit { session_lifetime_ms: 100, effective_expires_at_ms: 1_100 },
184        },
185        max_lifetime = {
186            OAuthSessionFacts { token_expires_at_ms: i64::MAX, now_ms: 0, ..facts() },
187            OAuthSessionDecision::Admit { session_lifetime_ms: i64::MAX, effective_expires_at_ms: i64::MAX },
188        },
189    )]
190    fn session_expiry_is_exact_and_capped(
191        facts: OAuthSessionFacts,
192        expected: OAuthSessionDecision,
193    ) {
194        assert2::check!(oauth_session_admission(facts) == expected);
195    }
196
197    #[yare::parameterized(
198        missing_expiry = { OAuthSessionFacts { expiry: OAuthExpiryPresence::Missing, ..facts() } },
199        expired = { OAuthSessionFacts { token_expires_at_ms: 1_000, ..facts() } },
200        overflowing_lifetime = {
201            OAuthSessionFacts { token_expires_at_ms: i64::MAX, now_ms: -1, ..facts() },
202        },
203        nonpositive_cap = {
204            OAuthSessionFacts { cap: OAuthSessionCap::Enabled, cap_ms: 0, ..facts() },
205        },
206        changed_principal = {
207            OAuthSessionFacts {
208                authentication: OAuthAuthenticationKind::Reauthentication,
209                principal: OAuthPrincipalMatch::Differs,
210                ..facts()
211            },
212        },
213    )]
214    fn invalid_lifetime_or_principal_fails_closed(rejected: OAuthSessionFacts) {
215        assert2::check!(oauth_session_admission(rejected) == OAuthSessionDecision::Reject);
216    }
217}
218
219mod completion;
220pub use completion::oauth_validation_admission;
krabka_verified/oauth.rs

krabka_verified/
oauth.rs
