Formal Verification of Cloud Native Components
“The heaviest penalty for declining to rule is to be ruled by someone inferior to yourself.”
― Plato, The Republic
Guardian is an omnibus repository for tooling to formally verify components of a cloud native system. As each component is fleshed out, it might become its own standalone project, or Guardian could become just a Swiss Army Knife of useful verification tools. TBD. Suggestions are welcome!
For any Guardian project the main idea is that Guardian provides a framework for formal expression and verification of the relationship between the intent of a program and program logic such that:
P |= φ [0]
or “P satisfies φ”, where P is a program, ie a computational process, and φ is a logic (a set of properties).
The "formal" activities in scope for Guardian projects in terms of this relation:
- Guardian tooling MUST enable program verification - the task of proving that P |= φ.
- Guardian tooling SHOULD assist with specification - the task of defining (a list of) properties φ to be satisfied by the program.
- Guardian tooling MAY assist with program synthesis, ie the task of finding P given (a list of) φ.
The general framework provided by Guardian consists of finding:
- A metalanguage comprising
- types, or data domains, or universes of discourse for various computational situations.
- and the syntax for specifying parameterized specifications .
- An intepreter for the metalanguage, providing the theorems to be proven from the specification. This gives a "program logic".
- Kubernetes RBAC Policy Verification
- Kubernetes NetworkPolicy Verification
- Kubernetes Admission Control Verfication example
- Certificate (Lifecycle) Management Verification
- Supply Chain Management Verification
- Verification of "Defense in Depth", e.g. CVE Impact Model
- Istio and other Service Mesh policy
- especially where per dataum deny rules are needed, e.g. EMRs[5]