Formally Verifying a Key Management Service

Sammanfattning

This thesis presents a formal model and protocol of a specific cloud-based Key Management Service (KMS) for the purpose of design validation.. The KMS architecture, inspired by industry-leading implementations, employs a layered structure facilitating envelope encryption. The study addresses whether this specific design can be formalized and validated using formal methods and associated tools. An abstract protocol defining the KMS operations was devised, which specified synchronized component classes and assumptions regarding, among other things, cryptography, databases, and scheduling. After exploring different formal approaches, the Spin model checker was chosen to verify the KMS. Four Promela models were created, each exhibiting different protocol operations with two tenants as initiators, allowing observation of concurrent protocol execution. Linear Temporal Logic (LTL) specifications were crafted to validate desired behaviors related to functional requirements. The safety specification focused on secure key management and correct message sequencing, while the liveness specifications for each model confirmed correct handling of all incoming requests. The verification process successfully validated several functional aspects of the KMS, demonstrating the feasibility of using model checking to verify security properties from a functional standpoint. However, it also highlighted the challenges in capturing the full complexity of such a service within model checking constraints. This work provides a foundation for further verification efforts for the KMS, suggesting areas for protocol refinement and more comprehensive modeling of complex KMS aspects like error handling, node failure recovery, and cryptographic operations in distributed settings.