Smart Casual Verification of the Confidential Consortium Framework

TL;DR

This paper presents a hybrid verification approach called smart casual verification, combining formal methods and automated testing, applied to validate the correctness of the Confidential Consortium Framework's distributed protocols within its CI pipeline.

Contribution

It introduces a practical, integrated verification method for complex distributed systems, enabling continuous correctness validation during development.

Findings

Identified six subtle bugs in CCF's design and implementation.

Successfully integrated formal verification into CCF's CI pipeline.

Validated the correctness of CCF's distributed consensus and client consistency model.

Abstract

The Confidential Consortium Framework (CCF) is an open-source platform for developing trustworthy and reliable cloud applications. CCF powers Microsoft's Azure Confidential Ledger service and as such it is vital to build confidence in the correctness of CCF's design and implementation. This paper reports our experiences applying smart casual verification to validate the correctness of CCF's novel distributed protocols, focusing on its unique distributed consensus protocol and its custom client consistency model. We use the term smart casual verification to describe our hybrid approach, which combines the rigor of formal specification and model checking with the pragmatism of automated testing, in our case binding the formal specification in TLA+ to the C++ implementation. While traditional formal methods approaches require substantial buy-in and are often one-off efforts by domain experts, we have integrated our smart casual verification approach into CCF's CI pipeline, allowing contributors to continuously validate CCF as it evolves. We describe the challenges we faced in applying smart casual verification to a complex existing codebase and how we overcame them to find six subtle bugs in the design and implementation before they could impact production