PaperlayerView exact revision on arXiv

Source-linked AI summary

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

Ioana Silaş, Adrian Crăciun

arXiv:2609.34881v1cs.LOcs.DC

TL;DR

Multitenant Kubernetes clusters can face security and stability concerns from tenant interference, while traditional TLA+ use focuses on abstract models. This paper applies TLA+ trace checking to live audit-event behavior and reports that selected multitenancy violations can be detected in a live cluster.

  • Problem

    Multitenant Kubernetes clusters can face security and stability concerns when tenants interfere, making strict isolation important.

    Source: §1 · p. 1

  • Method

    The pipeline reuses a TLA+ cluster model’s predicates and derived sets to classify reconstructed states from Kubernetes audit-log traces as allowed or disallowed.

    Source: §2.1 · p. 3, §2.3 · p. 6

  • Results

    The evaluated scenarios showed that selected multitenancy violations can be detected from live-cluster audit events through alert generation.

    Source: §6 · p. 15

  • Takeaways & Limitations

    The work demonstrates that a formal state-machine specification can serve as the basis for runtime monitoring in a Kubernetes cluster.

    Source: §6 · p. 15

    The approach depends on access to Kubernetes audit logging and webhook configuration, which is not exposed to users in some managed environments.

    Source: §6 · p. 15

Abstract

from arXiv · show

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

The paper aims to connect formal modeling with practical observability to validate multitenant Kubernetes clusters continuously. It uses TLA+ specifications in a monitoring pipeline to check observed cluster behavior against specified rules.

1 Introduction

  • Multitenancy can introduce security and stability concerns through interference between tenants, motivating strict isolation across namespaces and resources.The paper frames this as a challenge in live Kubernetes systems.Source: §1 · p. 1
  • The paper models a multitenant cluster in TLA+ using predicates, actions, and invariants to check whether RBAC fits the abstracted cluster design.Source: §1 · p. 1
  • The approach shifts TLA+ from exhaustive model checking toward checking whether observed runtime behavior aligns with a predefined specification.The stated goal is to combine specification-level correctness with real-world Kubernetes behavior.Source: §1 · pp. 1–2
  • The workflow specifies expected behavior, extracts and normalizes execution traces from Kubernetes logs, then checks reconstructed traces against the specification.Source: §1 · p. 2
  • The contributions include TLA+ specifications and a deployable monitoring pipeline, with custom operators that interact with a messaging system and persistence layer.The authors also deployed a local kubeadm cluster on virtual machines to validate the pipeline’s operational flow.Source: §1 · p. 2

2 Modeling K8s Multitenancy in TLA+

The paper reuses a TLA+ model of multitenant Kubernetes policy to check deployed-cluster audit traces rather than only exhaustively checking abstract behaviors. The model captures namespace isolation and RBAC, while the trace specification replays observed events and records violations without treating them as proof of implementation correctness.

2.1 Formal Instrument: TLA+

  • Trace checking reuses a multitenant-cluster specification to replay deployed-cluster executions, detecting differences between the model and actual behavior without proving either implementation or specification correct.The result depends on which events are logged and their level of atomicity.Source: §2.1 · pp. 2–3

2.2 Proposed Multitenancy Model: The Base Specification

  • The base specification encodes namespace and cluster resources, bindings, permissions, and access attempts as states and transitions for the multitenant cluster.Its actions cover namespace and ClusterRole lifecycle changes, access grants and revocations, and attempted resource access.Source: §2.1 · p. 3, §2.2 · p. 4

2.1 Formal Instrument: TLA+

  • The base specification supplies policy semantics, while the trace specification supplies observational replay semantics and continues after violations so they can accumulate.This is audit trace checking or runtime policy monitoring, not refinement or conformance checking.Source: §2.1 · p. 3

2.2 Proposed Multitenancy Model: The Base Specification

  • The representative soft-tenancy model uses Namespace isolation and role-based access control, with Roles and ClusterRoles taking effect through namespace-wide RoleBindings or cluster-wide ClusterRoleBindings.The model excludes arbitrary Roles and binds permissions only to ClusterRoles, following a strict least-privilege choice.Source: §2.2 · p. 3
  • The base model’s invariants target cross-tenant bindings, dangling bindings, cross-tenant successful access, RoleBindings to cluster-admin, and tenant ClusterRoleBindings.A cross-tenant access success is disallowed unless the acting group is a cluster administrator.Source: §2.2 · pp. 5–6

2.3 The Trace Specification

  • The trace specification consumes Kubernetes audit logs and replays observed events against multitenancy rules instead of generating all possible system behaviors.It accepts real events even when they violate the desired state, then records violations as alerts while continuing through the batch.Source: §2.3 · p. 6
  • Audit logs are converted into TLA+-understood inputs and processed in finite batches, with intermediary state preserved so the next batch resumes from the preceding state.The specification processes event fields such as verb, resource, namespace, and user.Source: §2.3 · p. 6
  • Alerts are generated when processing an event adds a new violation to a violation set, avoiding repeated reports of previously known violations.The alert can therefore correspond to the event that actually introduces the violation.Source: §2.3 · p. 6

3 Pipeline Architectural Details

The monitoring pipeline runs inside Kubernetes and moves audit events through filtering, classification, and TLC trace checking. Custom NATS JetStream operators fetch logs, preserve state between runs, and publish alerts while making repeated calls stable within a TLC process.

3 Pipeline Architectural Details

  • The K8s-native pipeline is deployable in-cluster and uses decoupled components that can be updated or replaced independently.Its stages include a Python webhook, stream-creation and filtering scripts, and a Java-based TLC runner.Source: §3 · p. 8
  • Audit events pass from the API server to a webhook, then through NATS JetStream filtering and classification before the Multitenancy stream supplies TLC trace-checking input.Classification maps logs to the abstracted permissions in the TLA+ specification.Source: §3 · p. 8, Figure 1 · p. 8
  • The trace assumes audit events retain chronological order through webhook publication to a single JetStream stream and ordered consumption from the Multitenancy stream.TLC checks the order in which relevant events are stored in the final stream.Source: §3 · pp. 8–9
  • Sequential TLC runs process log batches continuously, saving each final state as a checkpoint for the next batch and publishing relevant logs to Alerts when violations are detected.The initial deployment catches up with current cluster state before subsequent batches use the trace specification.Source: §3 · p. 9

3.1 Custom NATS Jetstream TLA+ Operators

  • NatsConsume returns the same log batch when TLC revisits a state, rather than advancing the stream during that process.The operator uses a flag after successful retrieval to keep repeated fetches stable.Source: §3.1 · p. 9
  • State-loading, state-saving, and alert-publishing operators avoid duplicate effects when called repeatedly during a TLC process.The cached state is loaded from and saved to the Storage stream; alerts are published to the Alerts stream.Source: §3.1 · p. 9

4 Experimental Evaluation

The evaluation tests whether controlled RBAC multitenancy violations produce alerts and measures pipeline processing across workloads and tenant configurations. The discussion reports improving real-time factors with larger workloads, alongside higher per-event processing cost as modeled state grows.

Scalability Experiment

  • Workloads vary from 10 to 1,000 activities across 2, 5, or 10 tenants, while TLC batches up to 50 messages with a 4.5-second pull expiration.The batch size and expiration can be adjusted for a cluster’s event rate and latency needs.Source: §4 · p. 10, Scalability Experiment · p. 12

4.1 Environment Configuration and Methodology

  • The evaluation ran the webhook, event filtering, NATS messaging, and TLC trace checker on a local kubeadm cluster with one control-plane and two worker virtual machines.Source: §4.1 · p. 10

Validation Experiments

  • The pipeline detected each of the evaluated RBAC-related multitenancy violations.Each scenario expected alerts in the NATS stream, and the reported alert referenced the audit ID and triggering event type.Source: Validation Experiments · p. 10
  • A RoleBinding in tenant-b bound the tenant-a group, enabling tenant-a-user access to tenant-b resources and triggering a cross-tenant alert.Source: Validation Experiments · pp. 10–11

Scalability Experiment

  • The scalability runs measure workload-generation, end-to-end, and TLC durations, plus real-time ratios intended to indicate whether processing could fall behind generation.Source: Scalability Experiment · pp. 11–12

4.3 Discussion

  • Per-event TLC processing becomes more expensive as modeled cluster state grows, with the discussion pointing to the ten-tenant configuration.The authors offer larger modeled domains and state structures as a possible explanation.Source: Table 1 · p. 13, §4.3 · p. 13
  • As action counts increase, both the end-to-end factor and TLC real-time factor decrease; the reported tables cover end-to-end and TLC processing characteristics.Source: §4.3 · p. 12, §4.2 · p. 12, Table 2 · p. 13

5 Related Work

The related work contrasts the pipeline with Kubernetes multitenancy tools and runtime monitors, then with trace-checking approaches using formal specifications. The paper distinguishes its approach by checking cluster audit-log traces against a formal multitenancy model.

5.1 K8s Multitenancy

  • Kyverno and OPA Gatekeeper evaluate resources at admission time, while this pipeline checks audit events against a formal multitenancy model.Source: §5.1 · pp. 13–14
  • Falco detects suspicious behavior with security rules, whereas the pipeline checks Kubernetes audit events against a formal multitenancy model.Source: §5.1 · p. 14
  • Capsule groups namespaces under a cluster-scoped Tenant abstraction; the pipeline instead uses existing cluster information to detect violations.Source: §5.1 · p. 14

5.2 Trace Checking

  • Howard et al. describe primarily offline trace replay, unlike this pipeline’s continuous cluster monitoring.Source: §5.2 · p. 14
  • Kuppe et al. connect instrumented Java executions to TLA+ specifications, while this pipeline integrates TLA+-aided monitoring into an active cluster.The pipeline requires every state to be explicit in cluster logs; the paper says this is generally not a problem for Kubernetes audit logs.Source: §5.2 · p. 14
  • Howard et al. [HKA+24] validate production-system traces mainly offline in controlled test environments, rather than as an online runtime monitor.Source: §5.2 · p. 14
  • Rahman et al. discuss tracing challenges in MongoDB; this work relies on Kubernetes audit logs and requires no application-code changes.Source: §5.2 · p. 14
  • Ellsberg derives a trace-checking specification from TLA+ and uses modified network APIs; this pipeline checks behavior inferred directly from cluster audit logs.Source: §5.2 · pp. 14–15

6 Conclusions and Future Work

The paper demonstrates that a TLA+ multitenancy model can check live Kubernetes activity against specified rules and detect selected violations from audit events. Its pipeline depends on audit-log access, while future extensions would cover additional multitenancy concerns.

6 Conclusions and Future Work

  • Selected multitenancy violations were detected from live-cluster audit events, with the evaluated path spanning audit logging, webhook ingestion, filtering, trace checking, and alert generation.The work demonstrates runtime monitoring based on a formal state-machine specification in a Kubernetes cluster.Source: §6 · p. 15
  • The approach depends on Kubernetes audit logging and webhook configuration, and the multitenancy specification requires adaptation rather than being universally reusable.Managed Kubernetes environments without user-exposed audit webhook configuration are not directly applicable; self-managed clusters may allow administrators to modify API-server configuration.Source: §6 · p. 15
  • Future work would extend the model to resource consumption and NetworkPolicies, requiring additional runtime sources such as pod- and container-level logs.Source: §6 · p. 15
Loading 2609.34881v1…