krabka_verified/delegation_token/
token_mutation_decision.rs

1use {
2    super::{
3        ScramCredentialSource, TokenApi, TokenApiAdmission, TokenMutationDecision,
4        TokenMutationFacts, TokenMutationKind, TokenMutationState,
5    },
6    creusot_std::prelude::*,
7};
8
9/// Classify the credential for SCRAM round 1.
10///
11/// `token_mechanism` is whether the delegation-token store may be read: the
12/// broker passes the client-first `tokenauth` extension there, and leaves
13/// `has_regular_credential` false when it is set, so exactly one store is
14/// consulted, as in Kafka's `ScramSaslServer`.
15///
16/// A token in the store is a credential whether or not it has expired, as in
17/// Kafka's `ScramServerCallbackHandler`, which reads the token cache without
18/// an expiry check. An expired token's session has a lifetime of 0, so the
19/// connection's next request that does not begin a re-authentication closes
20/// it; the expiry sweep is what takes the token out of the store.
21#[ensures((result == ScramCredentialSource::Regular) == has_regular_credential)]
22#[ensures((result == ScramCredentialSource::DelegationToken) ==
23    (!has_regular_credential && token_mechanism && has_token))]
24#[ensures((result == ScramCredentialSource::Unknown) ==
25    (!has_regular_credential && (!token_mechanism || !has_token)))]
26#[must_use]
27pub fn scram_credential_source(
28    has_regular_credential: bool,
29    token_mechanism: bool,
30    has_token: bool,
31) -> ScramCredentialSource {
32    if has_regular_credential {
33        ScramCredentialSource::Regular
34    } else if token_mechanism && has_token {
35        ScramCredentialSource::DelegationToken
36    } else {
37        ScramCredentialSource::Unknown
38    }
39}
40
41/// Whether one delegation token is visible to a Describe caller.
42///
43/// Matches `DelegationTokenManager.filterToken` in Kafka trunk: a caller sees
44/// a token only when the (possibly absent) owner filter matches it, and even
45/// then only as the token's owner, its requester (the principal that created
46/// it, KIP-373), a listed renewer, or the holder of an ACL grant: `Describe`
47/// on that exact token, or KIP-373's `DescribeTokens` on the owner's `User`
48/// resource. `acl_allows` is either grant. The caller is never a delegation-token-
49/// authenticated identity here — [`token_api_admission`] refuses every such
50/// caller before the host ever builds this predicate, so this kernel does not
51/// re-derive that isolation; folding it into the owner/requester/renewer/ACL
52/// relation would let a filter-matching owner or ACL grant leak a
53/// token-authed caller's sibling tokens back in.
54#[ensures(result == (owner_filter_matches
55    && (caller_is_owner || caller_is_requester || caller_is_renewer || acl_allows)))]
56#[allow(
57    clippy::fn_params_excessive_bools,
58    reason = "the proof classifies independent token visibility relationships"
59)]
60#[must_use]
61pub fn token_describe_visible(
62    owner_filter_matches: bool,
63    caller_is_owner: bool,
64    caller_is_requester: bool,
65    caller_is_renewer: bool,
66    acl_allows: bool,
67) -> bool {
68    owner_filter_matches
69        && (caller_is_owner || caller_is_requester || caller_is_renewer || acl_allows)
70}
71
72/// Admit delegation-token APIs only for a securely authenticated, non-token
73/// identity.
74///
75/// Matches `KafkaApis.allowTokenRequests`: a delegation-token-authenticated
76/// identity may not invoke ANY delegation-token API, including
77/// `DescribeDelegationToken`. KIP-48 forbids a token-issued session from
78/// bootstrapping further token access; letting it describe would leak the
79/// HMACs of every other token the same owner holds. The host adapter is
80/// responsible for treating an anonymous listener principal as
81/// unauthenticated.
82#[ensures((result == TokenApiAdmission::Allow) == (
83    has_authenticated_identity && !authenticated_via_token
84))]
85#[ensures((result == TokenApiAdmission::Reject) == (
86    !has_authenticated_identity || authenticated_via_token
87))]
88#[must_use]
89pub fn token_api_admission(
90    has_authenticated_identity: bool,
91    authenticated_via_token: bool,
92    _api: TokenApi,
93) -> TokenApiAdmission {
94    if has_authenticated_identity && !authenticated_via_token {
95        TokenApiAdmission::Allow
96    } else {
97        TokenApiAdmission::Reject
98    }
99}
100
101// cargo-mutants: #[cfg(creusot)] spec function; not compiled outside Creusot, so no test can tell.
102#[cfg(creusot)]
103#[cfg_attr(test, mutants::skip)]
104#[logic(open)]
105fn token_generation_live(facts: TokenMutationFacts) -> bool {
106    pearlite! { facts.now_ms@ >= 0
107    && facts.expected_expiry_ms@ >= facts.now_ms@
108    && facts.max_timestamp_ms@ >= facts.now_ms@
109    && facts.expected_expiry_ms@ <= facts.max_timestamp_ms@ }
110}
111
112/// Fence a token mutation against its exact committed generation.
113///
114/// A retained log tail wins over retry classification. Exact already-applied
115/// updates and already-missing deletes are idempotent. No update may revive a
116/// token that has expired, which Kafka's `DelegationTokenControlManager`
117/// defines as a deadline strictly before `now`, or cross the token's immutable
118/// maximum timestamp. A renewal lands at or after `now` but, as in Kafka's
119/// `renewDelegationToken`, may shorten the current expiry.
120#[ensures((result == TokenMutationDecision::Append) == (
121    !facts.uncommitted_tail
122        && facts.state == TokenMutationState::Expected
123        && match facts.kind {
124            TokenMutationKind::Delete => true,
125            TokenMutationKind::Renew =>
126                token_generation_live(facts)
127                    && facts.incoming_expiry_ms@ != facts.expected_expiry_ms@
128                    && facts.incoming_expiry_ms@ >= facts.now_ms@
129                    && facts.incoming_expiry_ms@ <= facts.max_timestamp_ms@,
130            TokenMutationKind::Expire =>
131                token_generation_live(facts)
132                    && facts.incoming_expiry_ms@ >= 0
133                    && facts.incoming_expiry_ms@ <= facts.max_timestamp_ms@,
134        }))]
135#[ensures((result == TokenMutationDecision::Retry) == (
136    !facts.uncommitted_tail
137        && (facts.state == TokenMutationState::Applied
138            || (facts.kind == TokenMutationKind::Delete
139                && facts.state == TokenMutationState::Missing)
140            || (facts.kind == TokenMutationKind::Renew
141                && facts.state == TokenMutationState::Expected
142                && facts.incoming_expiry_ms@ == facts.expected_expiry_ms@
143                && token_generation_live(facts)))))]
144#[must_use]
145pub fn token_mutation_decision(facts: TokenMutationFacts) -> TokenMutationDecision {
146    if facts.uncommitted_tail {
147        return TokenMutationDecision::Reject;
148    }
149    match facts.state {
150        TokenMutationState::Applied => return TokenMutationDecision::Retry,
151        TokenMutationState::Missing => {
152            return match facts.kind {
153                TokenMutationKind::Delete => TokenMutationDecision::Retry,
154                TokenMutationKind::Renew | TokenMutationKind::Expire => {
155                    TokenMutationDecision::Reject
156                }
157            };
158        }
159        TokenMutationState::Stale => return TokenMutationDecision::Reject,
160        TokenMutationState::Expected => {}
161    }
162
163    match facts.kind {
164        TokenMutationKind::Delete => TokenMutationDecision::Append,
165        TokenMutationKind::Renew => {
166            if facts.now_ms < 0
167                || facts.expected_expiry_ms < facts.now_ms
168                || facts.max_timestamp_ms < facts.now_ms
169                || facts.expected_expiry_ms > facts.max_timestamp_ms
170            {
171                return TokenMutationDecision::Reject;
172            }
173            if facts.incoming_expiry_ms == facts.expected_expiry_ms {
174                TokenMutationDecision::Retry
175            } else if facts.incoming_expiry_ms >= facts.now_ms
176                && facts.incoming_expiry_ms <= facts.max_timestamp_ms
177            {
178                TokenMutationDecision::Append
179            } else {
180                TokenMutationDecision::Reject
181            }
182        }
183        TokenMutationKind::Expire => {
184            if facts.now_ms >= 0
185                && facts.expected_expiry_ms >= facts.now_ms
186                && facts.max_timestamp_ms >= facts.now_ms
187                && facts.expected_expiry_ms <= facts.max_timestamp_ms
188                && facts.incoming_expiry_ms >= 0
189                && facts.incoming_expiry_ms <= facts.max_timestamp_ms
190            {
191                TokenMutationDecision::Append
192            } else {
193                TokenMutationDecision::Reject
194            }
195        }
196    }
197}
krabka_verified/delegation_token/token_mutation_decision.rs

krabka_verified/delegation_token/
token_mutation_decision.rs
