Monitoring multitenant Kubernetes clusters with TLA+ trace checking
Monitoring and Verification of Multitenant Kubernetes Clusters using TLA+ Trace Checking
Logic in Computer ScienceDistributed, Parallel, and Cluster Computing
Summary
Kubernetes is software that helps run many applications on shared computers. Sometimes, different users can accidentally interfere with each other’s spaces, causing problems. The authors created a tool that checks recorded actions in Kubernetes using a special logic language called TLA+ to spot rule violations as they happen. This approach uses TLA+ not just to design systems beforehand, but to watch live data and find problems in real time.
What this means in practice
- •For kubernetes cluster operators: Detect violations of tenant isolation policies in running Kubernetes clusters using formal trace checking of audit logs.
- •For cloud infrastructure teams: Incorporate formal behavioral monitoring into multitenant cloud environments to improve correctness and security assurance.
Authors
Ioana Silaş, Adrian Crăciun
Abstract
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.