Tolga Acar, Cedric Fournet, and Dan Shumow
15 April 2014
We present DKM, a distributed key management system with a cryptographically veriﬁed 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 reﬁnement 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-veriﬁed implementation to date. We also describe several problems we uncovered and ﬁxed as part of this joint design, implementation, and veriﬁcation process.
|Publisher||Microsoft Technical Report|
Tolga Acar, Mira Belenkiy, Mihir Bellare, and David Cash. Cryptographic Agility and its Relation to Circular Encryption, Springer Verlag, May 2010.