krabka_verified/authz/
session.rs

1use creusot_std::prelude::*;
2
3/// Bind a SASL session to the earlier credential or positive listener cap.
4/// A sum beyond the clock range stays finite at `i64::MAX`.
5#[ensures((result.0 == None) == (credential_expiry_ms == None
6    && match reauth_ms { None => true, Some(cap) => cap@ <= 0 }))]
7#[ensures(match (credential_expiry_ms, result.0) {
8    (Some(credential), Some(at)) => at@ <= credential@,
9    _ => true,
10})]
11#[ensures(match (reauth_ms, result.0) {
12    (Some(cap), Some(at)) => cap@ > 0 ==> at@ <= now_ms@ + cap@,
13    _ => true,
14})]
15#[ensures(match result.0 {
16    None => true,
17    Some(at) => credential_expiry_ms == Some(at) || match reauth_ms {
18        None => false,
19        Some(cap) => cap@ > 0 && (at@ == now_ms@ + cap@ || at@ == i64::MAX@),
20    },
21})]
22#[ensures(match result.0 {
23    None => result.1@ == 0,
24    Some(at) => result.1@ == if at@ <= now_ms@ { 0 }
25        else if at@ - now_ms@ > i64::MAX@ { i64::MAX@ }
26        else { at@ - now_ms@ },
27})]
28#[must_use]
29pub fn sasl_session_expiry(
30    now_ms: i64,
31    credential_expiry_ms: Option<i64>,
32    reauth_ms: Option<i64>,
33) -> (Option<i64>, i64) {
34    let cap_expiry = match reauth_ms {
35        Some(cap) if cap > 0 => Some(now_ms.saturating_add(cap)),
36        _ => None,
37    };
38    let expiry = match (credential_expiry_ms, cap_expiry) {
39        (Some(credential), Some(cap)) => Some(credential.min(cap)),
40        (credential, cap) => credential.or(cap),
41    };
42    let Some(at) = expiry else {
43        return (expiry, 0);
44    };
45    (expiry, at.saturating_sub(now_ms).max(0))
46}
47
48/// Kafka's `KafkaChannel.MIN_REAUTH_INTERVAL_ONE_SECOND_NANOS`, in ms: a
49/// connection may not start a re-authentication more than once a second.
50pub const MIN_REAUTH_INTERVAL_MS: i64 = 1_000;
51
52/// Whether a `SaslHandshake` on a session that expires at `expiry_ms` begins
53/// a KIP-368 re-authentication.
54///
55/// Kafka's `KafkaChannel.maybeBeginServerReauthentication` decides it: the
56/// session must have an expiry, and the last re-authentication on the connection, if any,
57/// must have started [`MIN_REAUTH_INTERVAL_MS`] or more before `now_ms`.
58#[ensures(result == (expiry_ms != None && match last_start_ms {
59    None => true,
60    Some(last) => now_ms@ - last@ >= 1000,
61}))]
62#[must_use]
63pub fn reauthentication_begins(
64    expiry_ms: Option<i64>,
65    now_ms: i64,
66    last_start_ms: Option<i64>,
67) -> bool {
68    match (expiry_ms, last_start_ms) {
69        (None, _) => false,
70        (Some(_), None) => true,
71        (Some(_), Some(last)) => now_ms.saturating_sub(last) >= MIN_REAUTH_INTERVAL_MS,
72    }
73}
74
75/// Whether a request must close the connection because its KIP-368 session
76/// has expired, as Kafka's `Processor.processCompletedReceives` decides.
77///
78/// A session expires only strictly after its deadline, as in
79/// `KafkaChannel.serverAuthenticationSessionExpired`: a request at exactly
80/// `expiry_ms` is still served. Past the deadline the one exempt frame is a
81/// `SaslHandshake` (17) that [`reauthentication_begins`] accepts, because
82/// Kafka asks `maybeBeginServerReauthentication` before it checks the
83/// deadline. Every other frame closes, a `SaslAuthenticate` (36) with no
84/// handshake before it and a handshake inside the one-second interval
85/// included. Authentication phase admission is a separate gate, including
86/// during the re-authentication rounds.
87#[ensures(result == (match expiry_ms {
88    None => false,
89    Some(at) => now_ms@ > at@,
90} && !(api_key@ == 17 && match last_reauth_start_ms {
91    None => true,
92    Some(last) => now_ms@ - last@ >= 1000,
93})))]
94#[must_use]
95pub fn session_expired_for_request(
96    expiry_ms: Option<i64>,
97    api_key: i16,
98    now_ms: i64,
99    last_reauth_start_ms: Option<i64>,
100) -> bool {
101    match expiry_ms {
102        Some(at) if now_ms > at => {
103            !(api_key == 17 && reauthentication_begins(expiry_ms, now_ms, last_reauth_start_ms))
104        }
105        _ => false,
106    }
107}
krabka_verified/authz/session.rs

krabka_verified/authz/
session.rs
