arXiv CSopen access

Monitoring and Verification of Multitenant Kubernetes Clusters using TLA+ Trace Checking

Monitoring and Verification of Multitenant Kubernetes Clusters using TLA+ Trace Checking Ioana Silaş

Adrian Crăciun

Faculty of Informatics West University Timişoara Romania [email protected] [email protected]

In distributed systems, model checking is usually used at design time for specifying an abstract model of the system and then exhaustively checking all possible behaviors. TLA+ is commonly used in this way as a specification language, together with the TLC model checker. In this paper, we present a monitoring tool that, at its core, utilizes TLA+ specifications in a different way. The tool utilizes a TLA+ trace-checking specification to detect violations in behavior inferred from Kubernetes audit logs. Our primary use case focuses on multitenancy violations; however, the pipeline is not limited to that setting. Specifically, it demonstrates how formal reasoning can be incorporated into live Kubernetes environments to improve monitoring and correctness checking.

1

Introduction

Kubernetes (K8s), see [Kub26a], is a widely-used, open-source container orchestration platform. It automates the deployment, scaling, and management of containerized applications and has become the de facto standard for many cloud-native environments. The complexity of K8s introduces challenges in ensuring the correctness and security of live systems. Another layer of complexity is added by multitenancy, which allows multiple teams or applications to share the same cluster to reduce infrastructure costs and improve resource utilization. This setup introduces potential security and stability concerns, since it can lead to interference between different tenants in the cluster, whether malicious or unintentional. To mitigate these risks, it is essential to enforce strict isolation mechanisms across namespaces and resources. Formal methods have traditionally been used to model and verify distributed systems in order to provide strong guarantees of correctness and security. TLA+ , see [Lam02], a formal specification language, has been widely used in the industry by companies such as Intel, see [BL02], Amazon, see [NRZ+ 15], and others. In this paper, we use TLA+ to create a model of a multitenant cluster: we describe predicates, actions, invariants. Then, we extend the role of specifications that reflect the cluster states by using them to monitor live cluster behavior. In this way, we can confirm that the role-based access control (RBAC) implementation fits our abstracted cluster design, which otherwise would be difficult to validate. To achieve this, we create a tool that integrates cluster monitoring with formalism. Rather than just performing exhaustive model checking (as seen in traditional TLA+ applications), our approach verifies that observed system behaviors align with a predefined specification. The goal is to shift the focus from abstract verification to concrete, runtime observation, in order to provide a solution that is both accessible to system administrators and more rigorous than standard monitoring tools. Such tools provide visibility into runtime events but lack formal correctness guarantees.

Mircea Marin, Adrian Crăciun (Eds.): FROM 2026 EPTCS 452, 2026, pp. 51–66, doi:10.4204/EPTCS.452.4

© I. Silaş & A. Crăciun This work is licensed under the Creative Commons Attribution License.

52

Monitoring and Verification of Multitenant Kubernetes Clusters using TLA+ Trace Checking In order to achieve our goal, we take the following steps: • specify expected K8s multitenant cluster behavior using TLA+ , focusing on state transitions and invariants, • extract and normalize execution traces from K8s logs, • check the reconstructed trace against the TLA+ specification using a monitoring pipeline, • evaluate the approach in multitenant scenarios to assess scalability and the pipeline’s ability to detect violations.

What we want to achieve is a combination of formal modeling with practical system observability in order to link specification-level correctness and real-world K8s behavior. The goal is to implement continuous validation of multitenant deployed clusters while preserving the operational semantics of K8s. Our contributions are: TLA+ specifications for multitenant K8s, a monitoring pipeline that can be deployed in clusters. In addition, we have written custom TLA+ operators that interact with a messaging system and its persistence layer. We have also deployed a kubeadm K8s cluster locally on virtual machines and used it to validate the operational flow of the pipeline. The paper is organized as follows: Section 2 presents an overview on K8s multitenancy and the TLA+ specifications at the core of the pipeline. Section 3 describes the architecture and design of the monitoring pipeline. Section 4 details the experimental setup, methodology, and results. Section 5 reviews related work in trace checking and K8s multitenancy. Finally, Section 6 discusses the findings of this paper and directions for future improvements. The implementation of the monitoring pipeline discussed throughout this paper and the experimental results are available in our GitHub repository1 .

Modeling K8s Multitenancy in TLA+

2

We introduce TLA+ and explain the particular way we used it here – trace checking. We then explain how we formalized a particular model of K8 multitenancy, in order to monitor multitenant K8 clusters.

2.1

Formal Instrument: TLA+

TLA+ is a formal language based on set theory, which focuses on model checking (see [Lam02]). It is based on a state machine model: we describe an initial state and specify the possible transitions through which the system can mode from one state to the next. The usual usage of the language follows this trajectory: a specification that describes the essential behavior of an abstracted away algorithm or system is written, then it is model-checked. If modelchecking reports a violation, the counterexample can be used to improve the specification or modify the design before the system implementation. Another case is when the system is already implemented, but writing a specification leads to uncovering hidden assumptions or design flaws that were not obvious from code or testing. In both cases, however, the implementation is not linked directly to the specification, since a highly abstractized version is created and model-checked. This limitation is discussed in [CKLM25], where the authors mention that while TLA+ and similar formal languages provide mechanisms to check an abstracted version of the system, they do not provide means to check the correctness of the actual implementation. As a result, another use of TLA+ , and the 1 https://github.com/zwx13/k8s-runtime-audit/tree/main

I. Silaş & A. Crăciun

53

one we adopt here, is to take the highly abstracted specification and use it to verify traces produced by the implemented system. By trace checking we reuse the initial specification of the system (K8 multitenancy in our case) for the purpose of monitoring deployed multitenant clusters. Note that trace checking does not prove that the implementation or the specification is correct. It solely checks whether recorded executions are compatible with the specification. This depends on what the trace or log specifies, the relation between the specification and implementation. Logging the relevant events at the appropriate level of atomicity can become costly if the implementation is very complex (as seen in [DHS20]). As a result, we should look at trace checking not as a proof of implementation correctness, but rather as a way of reusing TLA+ specifications at the implementation level and identifying differences between the model and actual execution. The TLA+ use in the work presented here can be summarized as follows: (1) The base specification represents the abstract model of the multitenant cluster and the intended multitenant policy. The model was constructed based on the K8 documentation covering multitenancy and Subsection 2.2 provides an overview of this model. The development of the model included the use of the TLC, the model checker of TLA+ to ensure consistency, which is the standard way TLA+ is used. However, the consistency of the model is not the focus of the work presented in this paper and we skip the details. (2) The trace specification reuses the base specification’s predicates and derived sets to classify reconstructed states as allowed or disallowed. The base specification provides the policy semantics, while the trace specification provides the observational replay semantics. This is not refinement or conformance checking, but rather TLA+ -based audit trace checking or runtime policy monitoring. We replay observed events, detect bad states by using predicates, and the replay continues so violations can be accumulated instead of stopping at the first non-conforming transition. This is explained in Subsection 2.3.

2.2

Proposed Multitenancy Model: The Base Specification

There is no single standard model when it comes to K8s multitenancy. We specify a representative soft tenancy model which is built on Namespace isolation between tenants and role-based access control. K8s resources can be either cluster-wide or scoped to a Namespace. Namespaces aid in dividing cluster resources between multiple teams. In soft multitenancy they provide a grouping mechanism for workloads. For example, a team can use one or more Namespaces to deploy their applications, and labels on the Namespaces can identify ownership and tenant information. This is useful in creating the tenant abstraction, since K8s does not have a native Tenant object. Namespaces are created by cluster administrators since they are global objects. Roles define permissions at the Namespace-level, while ClusterRoles define permissions at the cluster level, or reusable permissions that can be used inside a Namespace. In either case, the permissions become effective only when they are bound through RoleBindings or ClusterRoleBindings. The former have Namespace-wide effect, while the latter’s scope is the whole cluster. The TypeOK state predicate defines these RBAC concepts in our model, see Listing 1. Permissions can be granted at the group level with either ClusterRoleBindings or RoleBindings. These bindings can bind only to ClusterRoles, not to Roles. We chose to follow a strict version of the principle of least privilege (see [Kub26c]) and did not include the latter in our model at all. Allowing arbitrary Roles in each Namespace would increase the number of possible permission configurations without adding much value for the representative model. The default K8s ClusterRoles already cover the common access levels needed in this model, while cluster administrators can still create custom ClusterRoles if more specific permissions are required.

54

1 2 3 4 5 6 7 8 9 10 11 12 13

Monitoring and Verification of Multitenant Kubernetes Clusters using TLA+ Trace Checking

TypeOK == /\ nsTenantMap \in [Namespaces -> (Tenants \cup {NoTenant})] /\ DOMAIN roleBindings \in SUBSET (Namespaces \X RBNames) /\ \A key \in DOMAIN roleBindings: roleBindings[key] \in (Groups \X ClusterRoleNames) /\ DOMAIN clusterRoleBindings \in SUBSET CRBNames /\ \A key \in DOMAIN clusterRoleBindings: clusterRoleBindings[key] \in (Groups \X ClusterRoleNames) /\ DefaultClusterRoleNames \in SUBSET DOMAIN clusterRoles /\ DOMAIN clusterRoles \in SUBSET ClusterRoleNames /\ \A key \in DOMAIN clusterRoles: clusterRoles[key] \in Permissions /\ DOMAIN accessAttempts \in SUBSET (Namespaces \X Groups \X Permissions) /\ \A key \in DOMAIN accessAttempts: accessAttempts[key] \in [respectsNSTMapAtReqTime: BOOLEAN, matchingRBorCBR: BOOLEAN]

Listing 1: The base specification - multitenancy concepts and constraints.

1

2 3 4 5 6 7 8 9 10 11

Next == \E admingroup \in Groups, rbName \in RBNames, crbName \in CRBNames, targetgroup \in Groups, ns \in Namespaces, t \in Tenants, p \in Permissions, cr \in (ClusterRoleNames): \/ CreateNamespace(admingroup, ns, t) \/ DeleteNamespace(admingroup, ns) \/ CreateClusterRole(admingroup, cr, p) \/ UpdateClusterRole(admingroup, cr, p) \/ DeleteClusterRole(admingroup, cr) \/ GrantNSAccess(admingroup, ns, rbName, targetgroup, cr) \/ RevokeNSAccess(admingroup, ns, rbName, targetgroup, cr) \/ GrantClusterAccess(admingroup, crbName, targetgroup, cr) \/ RevokeClusterAccess(admingroup, crbName, targetgroup, cr) \/ AttemptAccess(ns, targetgroup, p)

Listing 2: Possible actions - transitions of the system.

The actions (transitions of the multitenant cluster) are described by the Next predicate, as illustrated in Listing 2. These actions describe creation and deletion of namespaces, creation, deletion, updates to cluster roles, granting and revocation of namespace or cluster access, as well as attempted access to resources of particular namespaces. The cluster administrators are the only ones who can create custom ClusterRoles. Besides these, the cluster administrators can use one of the four default ClusterRoles: view, edit, admin, and cluster-admin. When these are bound inside a Namespace with a RoleBinding, even if the permissions are wide, such as those granted by assigning the ClusterRole of cluster-admin, they are Namespace-scoped. When the ClusterRoles are granted through ClusterRoleBindings, they are cluster-scoped. As for the hierarchy inside Namespaces, in each of them there can be a group that is assigned the ClusterRole that grants admin powers. Such a group has permissions to create RoleBindings only, but not ClusterRoleBindings, to give rights to other groups that operate in the same Namespace. However, abiding by the principle of least privilege, no group can grant more powers than they have. As a result, Namespace administrators can only create RoleBindings that bind to view or edit. Cluster administrators can grant whatever ClusterRole they choose to in any Namespace. See Listing 3. The AttemptAccess action, see Listing 4, models the event where a group attempts to access resources in a particular Namespace. The access attempts are monitored and they also note whether they

I. Silaş & A. Crăciun

1 2 3 4 5

55

GrantNSAccess(admingroup, targetNS, rbName, targetG, cr) == /\ cr \in DOMAIN clusterRoles /\ LET clusterPerm == clusterRoles[cr] IN \/ /\ IsClusterAdmin(admingroup) /\ clusterPerm \in {"none", "read", "write", "admin-powers"}

6

\/

/\ IsNSAdmin(admingroup, targetNS) /\ clusterPerm \in {"none", "read", "write"} /\ SameTenant(targetNS, targetG) /\ roleBindings' = <<targetNS, rbName>> :> <<targetG, cr>> @@ roleBindings /\ UNCHANGED << nsTenantMap, clusterRoleBindings, clusterRoles, accessAttempts >>

7 8 9 10 11

Listing 3: Granting namespace access.

were allowed or not, based on the actor group, the relation between this group and the Namespace, and the existence of a matching (Cluster)RoleBinding. The details concerning the rest of the actions are skipped for the purpose of this presentation. The code is available in our repository. 1 2 3 4 5 6 7 8 9 10 11 12 13 14

AttemptAccess(ns, g, p) == /\ nsTenantMap[ns] # NoTenant /\ accessAttempts' = IF <<ns, g, p>> \in DOMAIN accessAttempts THEN [accessAttempts EXCEPT ![<<ns, g, p>>].respectsNSTMapAtReqTime = (SameTenant(ns, g) \/ g \in AdminGroups), ![<<ns, g, p>>].matchingRBorCBR = (MatchRoleBinding(ns, g, p) \/ MatchCRBinding(g, p))] ELSE <<ns, g, p>> :> [respectsNSTMapAtReqTime |-> (SameTenant(ns, g) \/ g \in AdminGroups), matchingRBorCBR |-> (MatchRoleBinding(ns, g, p) \/ MatchCRBinding(g, p)) ] @@ accessAttempts /\ UNCHANGED << nsTenantMap, roleBindings, clusterRoleBindings, clusterRoles >>

Listing 4: Modeling access attempt. The invariants described in the base specification focus on common multitenancy violations: crosstenant bindings, dangling bindings, cross-tenant successful access attempts, RoleBindings to cluster-admin, no ClusterRoleBindings for tenant groups, see Listing 5. Listing 6 illustrates cross tenant access, the rest are available in the repository. 1 2 3 4 5 6

Inv ==

/\ TypeOK /\ BindingsRespectMT /\ NoCrossTenantSuccess /\ NoDanglingBindings /\ NoClusterAdminRB /\ NoTenantCRB

Listing 5: Invariants for the base specification.

56

1

Monitoring and Verification of Multitenant Kubernetes Clusters using TLA+ Trace Checking

NoCrossTenantSuccess ==

2 3 4

\A a \in DOMAIN accessAttempts : LET group == a[2] IN accessAttempts[a].matchingRBorCBR = TRUE => accessAttempts[a].respectsNSTMapAtReqTime = TRUE

Listing 6: Example invariant: groups cannot access ourside their tenant, unless they are cluster admins.

But our objective is to deal with deployed multitenant clusters. Any violation of the invariants from the base specification would lead to a halt to the system. Enters...

2.3

The Trace Specification

The trace specification differs from the base specification in both purpose and input. As we have seen, the base specification models the desired state and allowed transitions of the system. In contrast, the trace specification operates on K8s audit logs directly. Its role is not to generate all possible system behaviors, but to replay observed events and check whether they violate the multitenancy rules we have defined. Model checking is a finite process, so we need to process logs in batches we can reasonably deal with. Each log entry is represented in JSON, but the trace specification needs to access fields such as the request’s verb, resource, Namespace where it took place, user who created the request. In order to achieve this, we convert the logs to a type that TLA+ understands. Moreover, since the trace specification operates on batches of logs, we preserve the intermediary state between batches. This allows the next batch to pick up from the state reached by the previous specification. In addition, detected violations are written separately as alerts so that cluster administrators can investigate them. To achieve this, we created custom operators that bridge the TLA+ specification and outer programs (for more details, see Subsection 3.1). The TLA+ operators retrieve the relevant system logs in a deterministic manner. Since model checking is not a single linear execution, a state or transition can be revisited from different paths. As a result, TLC may evaluate operators multiple times while exploring the state space. The main idea around the operators we implemented is that the log retrieval mechanism is stable and they are idempotent: operators always fetch the same batch of logs for a given state. The initial state initializes the idx variable to 1 (first element in a batch). We then check if there is a saved state to be picked-up from, and if so, we use it as a checkpoint. If there is not, we initialize Init to match the base specification, see Listing 7. In the Next state, we update variables directly. We do not call the matching actions from the base specification because the trace specification should allow actions that the base does not. Specifically, audit logs can contain violations of the desired cluster state reflected by the base specification. These events are real cluster events, so they should be accepted by the trace specification. For the same reason, the trace specification does not use invariants. Instead, it contains alert actions that add data about the violating event in a set, after it is encountered. These alerting operators are based on the base specification invariants. The trace specification records policy violations as alerts while continuing to process the audit logs in the batch. The basis for the alerting mechanism is the difference between the violation set before and after processing an event (e.g. CrossTenantSuccessSet). If the difference is empty, the current event did not introduce a new violation. The trace specification adds an alert with details from the relevant audit event if the difference is not empty. The purpose of this mechanism is to avoid reporting the same previously known violation repeatedly, so that the alert can correspond to the event that actually violates the rules we established in the base specification. This is illustrated in Listing 8.

I. Silaş & A. Crăciun

1 2 3 4 5 6 7 8 9 10 11 12 13 14 15

57

Init == /\ idx = 1 ... IF \/ IsEmpty \/ HasEmptyMappings THEN (* InitBase*) /\ nsTenantMap = [ ns \in Namespaces |-> NoTenant ] /\ roleBindings = [nsrb \in {} |-> {}] /\ clusterRoleBindings = "cluster-admin":> <<"kubeadm:cluster-admins","cluster-admin">> /\ clusterRoles = DefaultClusterRolePermMap ELSE (* InitFromCheckoint*) /\ nsTenantMap = IF HasEmptyNSTenantMap THEN [ ns \in Namespaces |-> NoTenant ] ELSE AllocIn.nsTenant /\ clusterRoles = AllocIn.clusterRoles /\ roleBindings = AllocIn.roleBindings /\ clusterRoleBindings = AllocIn.clusterRoleBindings

Listing 7: Initial state of the trace specification.

1 2 3

CrossTenantSuccessSet == {a \in DOMAIN accessAttempts : /\ accessAttempts[a].matchingRBorCBR /\ ~(accessAttempts[a].respectsNSTMapAtReqTime)}

4 5 6 7 8 9 10 11

12

AlertIfCrossTenantAction == LET crossTenantAction == Model!CrossTenantSuccessSet' \ Model!CrossTenantSuccessSet IN IF crossTenantAction = {} THEN /\ TRUE /\ UNCHANGED << crossTenantAlerts >> ELSE /\ crossTenantAlerts' = crossTenantAlerts \cup { << LogEvents[idx]["auditID"], LogEvents[idx]["tlaType"] >> } /\ PrintT("!!! Cross Tenant Access Identified !!!")

Listing 8: Alert processing example.

As for the allowed behavior, the AlertIfBadState action and Next action are combined into one. Processing a log entry can affect both the variables that represent the modeled cluster state and those that store detected alerts. The two actions are complementary: Next updates the cluster-state variables according to the information from the currently processed audit event, while AlertIfBadState evaluates the resulting state and updates just the alert sets: it does not modify the cluster-state variables. We combine the two actions using conjunction since they operate on disjoint groups of variables. 1 2 3 4 5 6

AlertIfBadState == /\ AlertIfCrossTenantAction /\ AlertIfDanglingRoleBindings /\ AlertIfDanglingClusterRoleBindings /\ AlertIfClusterRoleBindingForTenant /\ AlertIfRoleBindingToClusterAdmin

1 2

NextPrintSerialize == PrintInitOnce \/ (Next /\ AlertIfBadState ) \/ SerializeAtEnd

3 4 5

TraceBehavior == Init /\ [][NextPrintSerialize]_vars

Listing 9: Alerts, transitions in the trace specification.

58

3

Monitoring and Verification of Multitenant Kubernetes Clusters using TLA+ Trace Checking

Pipeline Architectural Details

The monitoring pipeline is designed as a K8s-native tool, so administrators can deploy it directly inside their clusters. Deployment is managed through Helm (see [Hel26]), which provides a package-like mechanism for installing and configuring K8s resources. The framework is organized as a pipeline of independent components which include a Python webhook, stream creating scripts, filtering scripts, and a Java-based TLC runner. These components are decoupled, so each stage can be updated or replaced independently, without disrupting the whole monitoring flow. The flow of the pipeline is illustrated in Figure 1 and goes as follows. The K8s API server continuously produces audit logs for cluster activity. By default, these logs are generated by the API server, but they are not automatically forwarded to an external processing component. For this reason, we configured a webhook endpoint where audit events are received.

K8s Cluster Native K8s Components Audit Log Mechanism

K8s API Server

HTTPS POST

TLA+ Monitoring Pipeline Webhook

Trace Runner

Alerts Stream

TLC (TLA+ Model-Checker)

Ingest

MT Stream

Filter

Audit Stream

Storage Stream

Figure 1: Architecture of the integrated monitoring pipeline within the K8s cluster. After receiving the audit events, the webhook forwards them to an Audit stream in NATS Jetstream (see [NAT26]), which is used as a high-performance messaging system. From there, the logs are consumed and further filtered to reduce noise and keep only those events that are relevant to the multitenancy model. Then we have another stream that acts as storage for cleaned and classified logs. We call this stream the Multitenancy stream. Before logs are sent to this stream, we classify them to match the abstracted permissions in the TLA+ specifications. After this classification, the logs are prepared for analysis and consumption by the TLC runner as input for trace checking. The pipeline depends on an ordering guaranty regarding the audit events. This assumption has two parts. First, K8s audit logs are treated as a chronological record of API-server activity (see [Kub26b]).

I. Silaş & A. Crăciun

59

Second, once these events are received by the webhook, they are published to a single NATS JetStream stream. JetStream streams store messages with sequence numbers, and TLC consumes messages from the Multitenancy stream in order. The trace checked by TLC corresponds to the order in which the relevant audit events are stored in the final stream. Batches of audit logs are processed by sequential TLC invocations, with a one-second interval between runs; TLC operates continuously as part of the monitoring pipeline. When the pipeline is first deployed, a Kubernetes job performs an initial catch-up with the current cluster state and stores the resulting state in NATS JetStream. Subsequent batches of audit logs are then processed using the TLA+ trace specification, starting from the previously stored state. After each TLC run, two outcomes are possible. If a specification violation is detected, the relevant audit logs are published to the Alerts stream so that the violation can be inspected and appropriate clean-up actions can be performed. The final model state is also persisted. If no violation is detected, no alert is emitted, but the final state is still stored persistently in NATS JetStream. This stored state acts as a checkpoint for the next TLC invocation: it allows each new batch of logs to be checked relative to the state produced by the previous batch.

3.1

Custom NATS Jetstream TLA+ Operators

As mentioned in Sunbsection 2.3, the TLA+ trace specification interacts with an external system to fetch batches of audit logs, save state between runs, and output alerts that can then be inspected by cluster administrators. This is achieved with the help of custom operators implemented in Java, that are then called inside the trace specification. NatsConsume: This is the log-fetching operator. The idea is that the fetching mechanism must remain stable: the operator must always fetch the same batch of logs for a given state, instead of advancing through the log stream during a revisiting of states. This is achieved with the help of a flag that is set to True once successful retrieval of the batch is finished. If the operator is called again during the same TLC process, it fetches the same batch instead of advancing and acking the next set of messages that might have arrived in the meanwhile. NatsLoadCachedState: This operator is used inside the initial state of the trace specification to retrieve the current state saved in the Storage stream in NATS JetStream. The pipeline could be deployed inside the cluster at any point: we created a mechanism that when the Storage stream is created, an entry with the current relevant cluster objects is added to it. Moreover, at the end of a TLC process, the state is saved in the same Storage stream, overwriting the previous entry. Its purpose is to ensure that the loaded cluster state from storage accurately reflects the environment. NatsPutCachedState: This is the counterpart to the previous operator. When a TLC process finishes executing, the resulting state is saved inside the Storage stream, so it can then be loaded when the next process runs. Both operators are idempotent, similar to the NatsConsume: if the NatsLoadCachedState operator’s flag indicates that the state was already fetched once during the same process, it returns the same state, instead of trying to load it again. As for the NatsPutCachedState operator, if it gets called again during model-checking, it returns True instead of re-publishing. NatsPublishAlert: Finally, this operator publishes alerts to the Alerts stream. These alerts are based on the mechanism showcased in 2.3. Similar to the NatsPutCachedState operator, after alerts have been published once during a TLC process, the operator returns True instead of publishing them again.

60

4

Monitoring and Verification of Multitenant Kubernetes Clusters using TLA+ Trace Checking

Experimental Evaluation

The evaluation focuses on two aspects. The first part determines whether audit events produced by a live K8s cluster are successfully processed by the monitoring pipeline and converted into alerts when they violate the TLA+ multitenancy model. We evaluate this using controlled, separate scenarios, where each script targets a specific policy violation. The second part of the experiment involves generating workloads of different sizes (10, 50, 100, 1000) for different number of tenants (2, 5, 10) to showcase the pipeline’s scalability.

4.1

Environment Configuration and Methodology

The experiment was conducted on a local kubeadm K8s cluster running on three libvirt virtual machines: one control-plane node and two worker nodes. The deployment of the monitoring tool includes all parts described in the previous section: the webhook receiver, the event filtering component, the NATS messaging layer, and the TLC-based trace checker. Validation Experiments We evaluated 5 different scenarios that corresponds to the actions in the multitenancy TLA+ model. For each scenario, the expected result is one or more alerts in the NATS Alerts stream. Each alert references the audit ID and the type of event that triggered it. When the expected alert is produced, the experiment validates the complete monitoring path: the API server emits an audit event, the webhook receives it, the event is filtered and converted, the trace checker processes it, and the violation is reported. Before each scenario, the required tenant resources are created from scratch. After each scenario finishes, the created resources are removed. The results in the repository show that the monitoring pipeline was able to detect each of the evaluated RBAC-related multitenancy violations. 1 2 3 4 5 6 7 8 9 10

apiVersion: rbac.authorization.k8s.io/v1 kind: ClusterRole metadata: name: dev rules: - apiGroups: [""] resources: ["pods", "configmaps", "secrets"] verbs: ["get", "list", "create", "update", "patch", "delete"]

1 2 3 4 5 6 7 8 9 10 11 12 13

apiVersion: rbac.authorization.k8s.io/v1 kind: RoleBinding metadata: name: tenant-b-binding namespace: tenant-b subjects: - kind: Group name: tenant-a # should be tenant-b apiGroup: rbac.authorization.k8s.io roleRef: kind: ClusterRole name: dev apiGroup: rbac.authorization.k8s.io

Listing 10: Simplified cross-tenant access violation example. Listing 10 showcases the K8s events created by the 01-cross-tenant-access.sh script. A ClusterRole, dev, grants access to Pods, ConfigMaps and Secrets. The RoleBinding in Namespace tenant-b wrongly binds the tenant-a group instead of tenant-b. As a result of the misconfiguartion, tenant-a-user’s access request is incorrectly authorized and they can successfully access resources in tenant-b. The monitoring pipeline detects the resulting cross-

I. Silaş & A. Crăciun

61

tenant access and emits the following alert: [["54e2c017-14f6-4ee5-a4bf-202e9d249362","access.attempt "]].

The first element of the alert is the K8s auditID, which uniquely identifies the corresponding audit event. An administrator can then retrieve the complete audit record for further investigation. An excerpt of the matching audit event is shown in Listing 11. 1 2

{

3 4 5 6 7 8 9 10 11 12 13 14 15 16 17

18 19

}

"auditID": "54e2c017-14f6-4ee5-a4bf-202e9d249362", "verb": "list", "user": { "username": "tenant-a-user", "groups": ["tenant-a"] }, "objectRef": { "resource": "pods", "namespace": "tenant-b" }, "responseStatus": { "code": 200 }, "annotations": { "authorization.k8s.io/reason": "RBAC: allowed by RoleBinding \"tenant-b-binding/tenant-b\" of ClusterRole \"dev\" to Group \"tenant-a\"" }

Listing 11: Audit log extract

Scalability Experiment Input generation duration

Prepare isolated run

Start experiment timer and per-batch TLC timing

Generate N workload actions

Wait for AUDIT and AUDIT_MT consumer drain

Wait for active TLC batch completion

Stop timing collection and experiment timer

Total experiment duration

Figure 2: Execution flow for an experiment run. For this experiment, the goal is to measure the scalability of the monitoring pipeline. Figure 2 describes the steps followed during each run. Each run is isolated, and multiple timers are used to measure both the overall experiment duration and the processing time of individual TLC batches. We measured the following metrics: • Input generation time (Tgen ) represents the wall-clock time required to generate the configured number of workload actions. • Experiment total time (Texp ) is the complete end-to-end duration. • TLC duration (TTLC ) is the accumulated duration of the TLC invocations.

62

Monitoring and Verification of Multitenant Kubernetes Clusters using TLA+ Trace Checking • TLC time spent on messages, the (Tnonfetch ) divided by no. of messages: Tnonfetch/msg =

TTLC,non-fetch . msgs

• TLC non-fetch time (Tnonfetch ) is the TLC invocation duration minus measured NATS fetch time. • TLC real-time factor ratio between TLC non-fetch time and input-generation time, RTLC =

TTLC,non-fetch . Tgeneration

Values below 1 indicate that the measured TLC processing cost is shorter than the workloadgeneration interval, while values above 1 indicate that TLC requires more processing time than the workload takes to generate. • End-to-end factor is the ratio between total experiment duration and input-generation time, RE2E =

Texperiment . Tgeneration

This ratio suggests whether the pipeline could fall behind the workload generation in time. • TLC messages and batches – the mean number of audit messages processed by TLC and the mean number of TLC batches required. The workload size is the number of Kubernetes activities generated during an experiment. The amount of messages eventually handled by TLC may range from this value and vary among runs and tenant configurations, as only audit events relevant to the multitenancy architecture are transmitted for verification. • Standard deviation is the run-to-run variability around the reported mean for each configuration. In order to adapt its processing behavior to the monitored cluster, the monitoring pipeline provides a number of adjustable options. In the evaluated configuration, TLC requests batches of up to 50 messages, with a pull-request expiration time of 4.5 seconds. The consumer waits 4.5 seconds for a batch to be filled, or it is processed right away if 50 messages become available before the expiry period; if not, the messages gathered during that time are processed as a smaller batch. These settings may be modified based on the event rate and latency needs of a specific cluster.

4.2

Results

Tables 1 and 2 describe the results of the scalability experiment. Both tables include the number of tenants, actions, and runs. The first table focuses on TLC processing characteristics: the number of processed messages, batching behavior, total processing time, non-fetch time, and non-fetch processing time per message. The second table focuses on workload generation and the overall timing of the experiment. It presents Tgen , Texp , and the ratios used to assess the real-time behavior of the monitoring pipeline.

4.3

Discussion

The end-to-end factor (RE2E ) gets lower as the action count increases, which suggests that the overhead of the pipeline becomes less significant under larger workloads. For smaller batches, the 4.5-second pull expiration is highly influential because batches are often only partially filled. In larger workloads, batches become fuller and the processing cost per message generally decreases. Similarly, the TLC real-time factor (RTLC ) lowers as the workload becomes more increased.

I. Silaş & A. Crăciun

63

Tenants Actions Runs Msgs. Batches Msgs./batch TTLC (ms) Tnonfetch (ms) Tnonfetch/msg (ms) 2 10 30 15.77 1.27 12.45 7076.0 ± 2495.5 1290.3 ± 445.3 89.8 ± 58.2 2 50 20 56.10 2.05 27.37 9738.3 ± 3153.4 2180.2 ± 622.3 38.7 ± 9.8 2 100 10 107.10 3.00 35.70 13574.6 ± 2416.1 3280.1 ± 699.4 30.4 ± 4.5 2 1000 10 1071.20 22.30 48.04 71149.9 ± 5019.3 26206.3 ± 1062.2 24.5 ± 0.8 5 10 30 13.57 1.30 10.44 7330.9 ± 2574.2 1386.1 ± 456.5 103.2 ± 26.5 5 50 20 41.50 1.15 36.09 6495.7 ± 2140.3 1320.4 ± 384.8 32.3 ± 9.5 5 100 10 82.50 2.40 34.38 13218.9 ± 2896.7 2730.5 ± 500.4 33.1 ± 5.5 5 1000 10 775.90 16.50 47.02 66235.1 ± 2674.3 20069.7 ± 684.8 25.9 ± 0.8 10 10 30 12.00 1.00 12.00 7292.3 ± 166.6 2724.2 ± 166.8 233.4 ± 42.1 10 50 20 36.60 1.05 34.86 7795.6 ± 1167.5 3080.8 ± 638.2 85.5 ± 15.8 10 100 10 68.70 2.00 34.35 14229.4 ± 594.3 6122.2 ± 511.8 89.3 ± 5.8 10 1000 10 689.60 14.30 48.22 71025.4 ± 1377.4 48484.2 ± 1430.4 70.3 ± 1.7

Table 1: TLC processing characteristics across tenant configurations.

Tenants 2 2 2 2 5 5 5 5 10 10 10 10

Actions 10 50 100 1000 10 50 100 1000 10 50 100 1000

Runs Tgen (ms) RTLC 30 1046.5 ± 188.6 1.263 ± 0.473 20 4364.0 ± 1129.4 0.520 ± 0.172 10 8998.2 ± 1159.0 0.366 ± 0.077 10 86005.1 ± 4406.9 0.305 ± 0.020 30 1627.3 ± 213.9 0.867 ± 0.310 20 4345.2 ± 315.2 0.305 ± 0.093 10 8758.8 ± 906.9 0.312 ± 0.045 10 75264.7 ± 2627.3 0.267 ± 0.007 30 2747.5 ± 162.0 0.994 ± 0.076 20 5755.0 ± 709.9 0.541 ± 0.119 10 9454.0 ± 800.9 0.651 ± 0.069 10 78971.8 ± 895.5 0.614 ± 0.017

RE2E 7.375 ± 1.516 2.609 ± 0.645 1.763 ± 0.186 1.073 ± 0.018 4.751 ± 0.677 1.788 ± 0.180 1.621 ± 0.159 1.100 ± 0.013 4.134 ± 0.281 2.110 ± 0.286 2.064 ± 0.136 1.124 ± 0.019

Texp (ms) 7579.1 ± 1251.4 11017.2 ± 2338.0 15744.8 ± 1621.1 92302.5 ± 4752.9 7636.1 ± 728.4 7724.9 ± 468.4 14085.9 ± 747.3 82783.7 ± 3301.1 11364.0 ± 1032.9 12024.9 ± 1370.1 19420.0 ± 576.6 88718.8 ± 1433.3

Table 2: End-to-end scalability and real-time processing characteristics across tenant configurations. The Tnonfetch/msg entries suggest that processing an individual audit event becomes more expensive as the modeled cluster state grows. We can observe this in the results for the ten-tenant configuration. A possible explanation is that larger modeled domains and state structures increase the cost of TLC’s internal state processing.

5

Related Work

This section presents related work in the fields of K8s multitenancy and trace checking. For the former, we present open-souce tools that propose different solutions to the problem. For the latter, we present peer-reviewed papers and one open-source project.

5.1

K8s Multitenancy

Kyverno is a K8s-native policy engine that is used as an admission controller (see [Kyv26]). It connects to the K8s API Server using an admission webhook. OPA Gatekeeper (see [Ope26]) is another K8s policy engine used to enforce policies at admission-time. It is similar to Kyverno in the sense that both

64

Monitoring and Verification of Multitenant Kubernetes Clusters using TLA+ Trace Checking

tools can evaluate requests sent to the K8s API server before resources are persisted. Kyverno and OPA Gatekeeper can prevent or report resources that violate K8s policies, but they do not provide a formal model of the expected multitenant state or reason over audit-log traces in the same way as our proposed tool. The monitoring pipeline is not a replacement for admission controllers: they evaluate resources against policies, while the proposed tool checks audit-log events against a formal multitenancy model. Falco is a cloud native security tool focused on threat detection (see [Fal26]). Unlike Kyverno and OPA Gatekeeper, which are mainly used to evaluate K8s resources at admission time, Falco observes runtime events and raises alerts in case it detects suspicious behavior. In multitenant environments, Falco can complement preventive isolation mechanisms by detecting suspicious cross-tenant behavior. Both the pipeline and Falco consume event streams and produce alerts, but the goals are different: Falco detects suspicious behavior using predefined or custom security rules, while the proposed pipeline checks K8s audit events against a formal multitenancy model. Capsule is a K8s multitenancy framework that introduces a higher level Tenant abstraction (for more details: [Pro26]). A Tenant is a cluster-scoped resource that groups one or more Namespaces under the same administrative boundary. Rather than validating resources or detecting suspicious runtime actions, Capsule changes how namespace-based multitenancy is represented in a cluster. Capsule has a different scope from the monitoring pipeline: our tool does not introduce a new abstraction in K8s, rather it utilizes existing cluster information to detect multitenancy violations.

5.2

Trace Checking

Howard et al. [HGG+ 11] present a case study that suggests the feasibility of replaying execution traces against formal specifications and highlights challenges related to trace processing. Their approach is primarily offline, as traces are gathered and analyzed after execution. On the other hand, our system is designed for continuous cluster monitoring rather than a retrospective analysis tool. Kuppe et al.[CKLM25] present a trace validation framework that links distributed Java program executions to high-level TLA+ specifications through code instrumentation. The authors create a tracespecific TLA+ wrapper around the base protocol spec and use TLC to measure the impact of trace detail on TLC’s state-space search cost. Our tool allows TLA+ -aided monitoring to be integrated directly into the operational lifecycle of an active cluster. However, we do not allow incomplete traces: every state must be explicitly mentioned in the cluster logs. This is not generally a problem for K8s audit logs, since they represent a history of the cluster state. Howard et al. [HKA+ 24] show how TLA+ can be applied to large-scale production systems using bounded model checking, simulation, and offline trace validation. Their work validates a framework by matching instrumented execution traces against low-level consensus and high-level consistency specifications. The validation is mainly performed offline in controlled test environments, rather than used as an online runtime monitor. Rahman et al. [DHS20] present an industrial case study of applying TLA+ and TLC for model-based trace checking in MongoDB. Their study highlights challenges in tracing highly concurrent systems: hierarchical locking, state visibility, and the difficulty of obtaining consistent snapshots of internal state without altering system behavior. In contrast to this approach, our work relies exclusively on K8s audit logs, which provide a complete and externally visible record of control-plane actions, and does not require changes in application code. Ding et al. [DWLP25] propose a runtime verification tool written in Go called Ellsberg, which emits alerts when a distributed protocol’s implementation outputs messages inconsistent with a protocol specification. The workflow starts from a TLA+ specification, from which users should derive a specification

I. Silaş & A. Crăciun

65

that Ellsberg can use. In their work, they modified the systems’ network APIs to forward protocol messages to the tool. In contrast, our pipeline directly uses TLC and TLA+ specifications to check observed behavior inferred from a cluster’s audit logs. The Open Network Operating System (ONOS) TLA+ Monitor [ONO26b] is a public conformance monitoring tool associated with the µONOS platform. Unlike most related work presented in this section, it is not presented as a peer-reviewed paper, but through public documentation and source code. The official ONOS documentation describes conformance monitoring as a mechanism for checking whether µONOS services abide by formal specifications in near real time. For more details, see [ONO26a]. The ONOS monitor showcases a practical use of TLA+ outside offline model checking, since formal specifications are used to validate executions of a running system. The ONOS monitor focuses on a SDN platform, while our pipeline targets K8s clusters. For the trace processing, the ONOS monitor uses uses a sliding window batching strategy. In our implementation we use explicit batching and checkpointing over the audit-event stream.

6

Conclusions and Future Work

In this paper, we have shown that a formal state-machine-based specification can be used as the basis for runtime monitoring in a K8s cluster. The main idea was to link a TLA+ multitenancy model to events produced by a live cluster in order to check observed system activity against the rules expressed in the specification. We packaged the pipeline as a K8s-native deployment, configured a K8s cluster, deployed the pipeline, and evaluated it through a set of experimental scenarios. The experiment showed that the selected multitenancy violations can be detected from audit events in a live cluster and verified the whole path: from API server audit logging, to webhook ingestion, filtering, trace checking, and alert generation. Overall, this work demonstrates that TLA+ can be used not only as a design-time specification language, but also as the basis for a monitoring pipeline connected to real system traces. Using the same language for both modeling the desired state and catching events that violate this state increases the usefulness of the specifications, especially in cases where the implementation can easily drift from the intended design. However, our work also presents limitations: it depends on access to K8s audit logging and audit webhook configuration. This may not be an issue in self-managed clusters where administrators can modify the API server configuration, but it is not directly applicable to managed K8s environments where audit webhook configuration is not exposed to the users. Moreover, the multitenancy specification is not universally reusable since it requires individual adaptation. For future work, we plan to extend the model to cover additional multitenancy-related concerns, such as resource consumption and NetworkPolicies. Supporting these aspects would also require the pipeline to ingest additional sources of runtime information, such as pod- and container-level logs.

References [BL02]

Brannon Batson & Leslie Lamport (2002): High-Level Specifications: Lessons from Industry. 2852, pp. 242–261, doi:10.1007/978-3-540-39656-7_10.

[CKLM25] Horatiu Cirstea, Markus A. Kuppe, Benjamin Loillier & Stephan Merz (2025): Validating Traces of Distributed Programs Against TLA+ Specifications. In Alexandre Madeira & Alexander Knapp, editors: Software Engineering and Formal Methods, Springer Nature Switzerland, Cham, p. 126–143, doi:10.1007/978-3-031-77382-2_8. Available at https://link.springer.com/chapter/10. 1007/978-3-031-77382-2_8.

66

Monitoring and Verification of Multitenant Kubernetes Clusters using TLA+ Trace Checking

[DHS20]

A. Jesse Jiryu Davis, Max Hirschhorn & Judah Schvimer (2020): Extreme modelling in practice. Proc. VLDB Endow. 13(9), p. 1346–1358, doi:10.14778/3397230.3397233. Available at http:// vldb.org/pvldb/vol13/p1346-davis.pdf.

[DWLP25] Ding Ding, Zhanghan Wang, Jinyang Li & Aurojit Panda (2025): Runtime Protocol Refinement Checking for Distributed Protocol Implementations. In: 22nd USENIX Symposium on Networked Systems Design and Implementation (NSDI 25), USENIX Association, Philadelphia, PA, pp. 1305–1326, doi:10.5555/3767955.3768025. Available at https://www.usenix.org/conference/nsdi25/ presentation/ding. [Fal26]

Falco Authors (2026): Falco Documentation. https://falco.org/docs/. Accessed: 2026-04-26.

[Hel26]

Helm Authors (2026): Helm Documentation. https://helm.sh/docs/. Accessed: 2026-06-15.

[HGG+ 11]

Yvonne Howard, Stefan Gruner, A. Gravell, Carla Ferreira & Juan Augusto Wrede (2011): ModelBased Trace-Checking. CoRR abs/1111.2825, doi:10.48550/arXiv.1111.2825. Available at https: //arxiv.org/abs/1111.2825.

[HKA+ 24] Heidi Howard, Markus A. Kuppe, Edward Ashton, Amaury Chamayou & Natacha Crooks (2024): Smart Casual Verification of the Confidential Consortium Framework, doi:https://doi.org/10.48550/arXiv.2406.17455. arXiv:2406.17455. [Kub26a]

Kubernetes Authors (2026): Kubernetes Documentation. https://kubernetes.io/. Accessed: 2026-04-25.

[Kub26b]

Kubernetes Authors (2026): Kubernetes Documentation: Auditing. https://kubernetes.io/ docs/tasks/debug/debug-cluster/audit/. Accessed: 2026-04-25.

[Kub26c]

Kubernetes Authors (2026): Kubernetes Documentation: RBAC Good Practices. https:// kubernetes.io/docs/concepts/security/rbac-good-practices/. Accessed: 2026-05-27.

[Kyv26]

Kyverno Authors (2026): Kyverno Documentation: Introduction. https://kyverno.io/docs/ introduction/. Accessed: 2026-04-26.

[Lam02]

Leslie Lamport (2002): Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley. Available at https://lamport.azurewebsites.net/tla/ book-02-08-08.pdf.

[NAT26]

NATS Maintainers (2026): NATS Documentation: nats-concepts/jetstream. Accessed: 2026-06-13.

JetStream.

https://docs.nats.io/

[NRZ+ 15] Chris Newcombe, Tim Rath, Fan Zhang, Bogdan Munteanu, Marc Brooker & Michael Deardeuff (2015): How Amazon Web Services uses formal methods. Communications of the ACM, doi:10.1145/2699417. Available at https://www.amazon.science/publications/ how-amazon-web-services-uses-formal-methods. [ONO26a] ONOS Project (2026): ONOS Documentation: Open Network Operating System. https://docs. onosproject.org/. Accessed: 2026-06-23. [ONO26b] ONOS Project (2026): TLA+ Monitor. https://github.com/onosproject/tlaplus-monitor. Accessed: 2026-04-25. [Ope26]

Open Policy Agent Contributors (2026): Gatekeeper Documentation: Introduction. https:// open-policy-agent.github.io/gatekeeper/website/docs/. Accessed: 2026-04-26.

[Pro26]

Project Capsule Authors (2026): Capsule Documentation: Overview. https://projectcapsule. dev/docs/overview/. Accessed: 2026-06-13.