krabka_verified/authz/
acl_decision.rs

1use {
2    super::{
3        AclDecision, AclDefault, AclFacts, AclOperationKind, AclPatternKind, AclResourceFacts,
4        AclResourceTypeMatch, RequestAuthState,
5    },
6    creusot_std::prelude::*,
7};
8
9/// Match a principal or host by exact equality or its axis-specific wildcard.
10#[ensures(result == (wildcard || exact))]
11#[must_use]
12pub fn acl_identity_match(wildcard: bool, exact: bool) -> bool { wildcard || exact }
13
14/// Match an ACL resource type and literal or prefixed name pattern.
15///
16/// Kafka's `AclAuthorizer.matchingAcls`: a LITERAL ACL applies to its exact
17/// name and, when that name is `*`, to every name; a PREFIXED ACL applies to
18/// every name that starts with its name. Neither applies across resource
19/// types.
20#[ensures(result == (facts.resource_type == AclResourceTypeMatch::Same && match pattern {
21    AclPatternKind::Literal => facts.exact_name || facts.wildcard_name,
22    AclPatternKind::Prefixed => facts.name_has_prefix,
23}))]
24#[must_use]
25pub fn acl_resource_match(pattern: AclPatternKind, facts: AclResourceFacts) -> bool {
26    match (facts.resource_type, pattern) {
27        (AclResourceTypeMatch::Different, _) => false,
28        (AclResourceTypeMatch::Same, AclPatternKind::Literal) => {
29            facts.exact_name || facts.wildcard_name
30        }
31        (AclResourceTypeMatch::Same, AclPatternKind::Prefixed) => facts.name_has_prefix,
32    }
33}
34
35/// Match exact operations, `All`, and Kafka's one-way implication arrows.
36///
37/// The implication arrows (`Read`/`Write`/`Delete`/`Alter` → `Describe`, and
38/// `AlterConfigs` → `DescribeConfigs`) apply only when the stored ACL is an
39/// ALLOW entry: Kafka's operation-implication table never widens what a DENY
40/// ACL blocks.
41#[ensures(result == (stored == requested
42    || stored == AclOperationKind::All
43    || (is_allow && stored == AclOperationKind::Read && requested == AclOperationKind::Describe)
44    || (is_allow && stored == AclOperationKind::Write && requested == AclOperationKind::Describe)
45    || (is_allow && stored == AclOperationKind::Delete && requested == AclOperationKind::Describe)
46    || (is_allow && stored == AclOperationKind::Alter && requested == AclOperationKind::Describe)
47    || (is_allow
48        && stored == AclOperationKind::AlterConfigs
49        && requested == AclOperationKind::DescribeConfigs)))]
50#[must_use]
51pub fn acl_operation_match(
52    stored: AclOperationKind,
53    requested: AclOperationKind,
54    is_allow: bool,
55) -> bool {
56    match stored {
57        AclOperationKind::All => true,
58        AclOperationKind::Read => {
59            matches!(requested, AclOperationKind::Read)
60                || (is_allow && matches!(requested, AclOperationKind::Describe))
61        }
62        AclOperationKind::Write => {
63            matches!(requested, AclOperationKind::Write)
64                || (is_allow && matches!(requested, AclOperationKind::Describe))
65        }
66        AclOperationKind::Delete => {
67            matches!(requested, AclOperationKind::Delete)
68                || (is_allow && matches!(requested, AclOperationKind::Describe))
69        }
70        AclOperationKind::Alter => {
71            matches!(requested, AclOperationKind::Alter)
72                || (is_allow && matches!(requested, AclOperationKind::Describe))
73        }
74        AclOperationKind::AlterConfigs => {
75            matches!(requested, AclOperationKind::AlterConfigs)
76                || (is_allow && matches!(requested, AclOperationKind::DescribeConfigs))
77        }
78        AclOperationKind::Create => matches!(requested, AclOperationKind::Create),
79        AclOperationKind::Describe => matches!(requested, AclOperationKind::Describe),
80        AclOperationKind::ClusterAction => matches!(requested, AclOperationKind::ClusterAction),
81        AclOperationKind::DescribeConfigs => {
82            matches!(requested, AclOperationKind::DescribeConfigs)
83        }
84        AclOperationKind::IdempotentWrite => {
85            matches!(requested, AclOperationKind::IdempotentWrite)
86        }
87        AclOperationKind::TwoPhaseCommit => {
88            matches!(requested, AclOperationKind::TwoPhaseCommit)
89        }
90        AclOperationKind::CreateTokens => matches!(requested, AclOperationKind::CreateTokens),
91        AclOperationKind::DescribeTokens => {
92            matches!(requested, AclOperationKind::DescribeTokens)
93        }
94    }
95}
96
97/// Decide whether an API key may run in the current authentication phase.
98#[ensures(state == RequestAuthState::Authenticated ==> result)]
99#[ensures(state == RequestAuthState::Failed ==> !result)]
100#[ensures(state == RequestAuthState::Exchanging ==>
101    result == (api_key@ == 36))]
102#[ensures(state == RequestAuthState::PreHandshake ==>
103    result == (api_key@ == 17 || api_key@ == 18))]
104#[must_use]
105pub fn request_auth_admission(state: RequestAuthState, api_key: i16) -> bool {
106    match state {
107        RequestAuthState::Authenticated => true,
108        RequestAuthState::Failed => false,
109        RequestAuthState::Exchanging => api_key == 36,
110        RequestAuthState::PreHandshake => matches!(api_key, 17 | 18),
111    }
112}
113
114/// Decide a request from whether any matching ACL allowed or denied it.
115///
116/// Kafka's `AclAuthorizer.authorizeAction` order: a super user is always
117/// allowed; otherwise a matching DENY wins over any ALLOW; otherwise a
118/// matching ALLOW allows; otherwise `default_decision` decides. It reflects
119/// `allow.everyone.if.no.acl.found` (default `false`), which allows a request
120/// only when no ACL at all applies to the resource, so it never overrides an
121/// explicit ALLOW or DENY.
122#[ensures(match result {
123    AclDecision::AllowSuperuser => facts.super_user,
124    AclDecision::DenyExplicit => !facts.super_user && facts.saw_deny,
125    AclDecision::AllowAcl => !facts.super_user && !facts.saw_deny && facts.saw_allow,
126    AclDecision::AllowNoAcl => !facts.super_user && !facts.saw_deny && !facts.saw_allow
127        && facts.default_decision == AclDefault::Allow,
128    AclDecision::DenyDefault => !facts.super_user && !facts.saw_deny && !facts.saw_allow
129        && facts.default_decision == AclDefault::Deny,
130})]
131#[must_use]
132pub fn acl_decision(facts: AclFacts) -> AclDecision {
133    if facts.super_user {
134        AclDecision::AllowSuperuser
135    } else if facts.saw_deny {
136        AclDecision::DenyExplicit
137    } else if facts.saw_allow {
138        AclDecision::AllowAcl
139    } else {
140        match facts.default_decision {
141            AclDefault::Allow => AclDecision::AllowNoAcl,
142            AclDefault::Deny => AclDecision::DenyDefault,
143        }
144    }
145}
krabka_verified/authz/acl_decision.rs

krabka_verified/authz/
acl_decision.rs
