Cryptographically Verified Design and Implementation of a Distributed Key Manager

We present DKM, a distributed key management system with a cryptographically verified code base. DKM implements a new data protection API. It manages keys and policies on behalf of groups of users that share data. To ensure long-term protection, DKM supports cryptographic agility: algorithms, keys, and policies can evolve for protecting fresh data while preserving access to old data. DKM is written in C# and currently used by several large data center applications. To verify our design and implementation, we also write a lightweight reference implementation of DKM in F#. This code closes the gap between formal cryptographic models and production code: Formally, the F# code is a very precise model of DKM: we automatically verify its security against active adversaries, using a refinement type-checker coupled with an SMT solver and new symbolic libraries for cryptographic agility. Concretely, the F# code closely mirrors our production code, and we automatically test that the corresponding C# and F# fragments can be swapped without affecting the runtime behavior of DKM. To the best of our knowledge, this is the largest cryptographically-verified implementation to date. We also describe several problems we uncovered and fixed as part of this joint design, implementation, and verification process.