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.

Publication Downloads

Distributed Key-Manager Verification

December 2, 2010

This package contains the F# and F7 source files to aid in the verification of a distributed key-management system. This new component implements a data-protection API for groups of clients. To enable long-term data protection, it supports cryptographic agility so cryptography algorithms and policies can evolve for protecting fresh data while preserving access to old data. To verify the security of our design and production code, written in C#, we write a reference implementation in F#. Formally, we verify our F# code against a logical cryptographic model using F7, a refinement type checker coupled with a model checker. Experimentally, we test that the corresponding C# and F# code fragments are interchangeable.