-
Smart Casual Verification of the Confidential Consortium Framework
Authors:
Heidi Howard,
Markus A. Kuppe,
Edward Ashton,
Amaury Chamayou,
Natacha Crooks
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…
▽ More
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
△ Less
Submitted 16 October, 2024; v1 submitted 25 June, 2024;
originally announced June 2024.
-
Confidential Consortium Framework: Secure Multiparty Applications with Confidentiality, Integrity, and High Availability
Authors:
Heidi Howard,
Fritz Alder,
Edward Ashton,
Amaury Chamayou,
Sylvan Clebsch,
Manuel Costa,
Antoine Delignat-Lavaud,
Cedric Fournet,
Andrew Jeffery,
Matthew Kerner,
Fotios Kounelis,
Markus A. Kuppe,
Julien Maffre,
Mark Russinovich,
Christoph M. Wintersteiger
Abstract:
Confidentiality, integrity protection, and high availability, abbreviated to CIA, are essential properties for trustworthy data systems. The rise of cloud computing and the growing demand for multiparty applications however means that building modern CIA systems is more challenging than ever. In response, we present the Confidential Consortium Framework (CCF), a general-purpose foundation for deve…
▽ More
Confidentiality, integrity protection, and high availability, abbreviated to CIA, are essential properties for trustworthy data systems. The rise of cloud computing and the growing demand for multiparty applications however means that building modern CIA systems is more challenging than ever. In response, we present the Confidential Consortium Framework (CCF), a general-purpose foundation for developing secure stateful CIA applications. CCF combines centralized compute with decentralized trust, supporting deployment on untrusted cloud infrastructure and transparent governance by mutually untrusted parties. CCF leverages hardware-based trusted execution environments for remotely verifiable confidentiality and code integrity. This is coupled with state machine replication backed by an auditable immutable ledger for data integrity and high availability. CCF enables each service to bring its own application logic, custom multiparty governance model, and deployment scenario, decoupling the operators of nodes from the consortium that governs them. CCF is open-source and available now at https://github.com/microsoft/CCF.
△ Less
Submitted 17 October, 2023;
originally announced October 2023.
-
IA-CCF: Individual Accountability for Permissioned Ledgers
Authors:
Alex Shamis,
Peter Pietzuch,
Miguel Castro,
Cédric Fournet,
Edward Ashton,
Amaury Chamayou,
Sylvan Clebsch,
Antoine Delignat-Lavaud,
Matthew Kerner,
Julien Maffre,
Manuel Costa,
Mark Russinovich
Abstract:
Permissioned ledger systems allow a consortium of members that do not trust one another to execute transactions safely on a set of replicas. Such systems typically use Byzantine fault tolerance (BFT) protocols to distribute trust, which only ensures safety when fewer than 1/3 of the replicas misbehave. Providing guarantees beyond this threshold is a challenge: current systems assume that the ledge…
▽ More
Permissioned ledger systems allow a consortium of members that do not trust one another to execute transactions safely on a set of replicas. Such systems typically use Byzantine fault tolerance (BFT) protocols to distribute trust, which only ensures safety when fewer than 1/3 of the replicas misbehave. Providing guarantees beyond this threshold is a challenge: current systems assume that the ledger is corrupt and fail to identify misbehaving replicas or hold the members that operate them accountable -- instead all members share the blame.
We describe IA-CCF, a new permissioned ledger system that provides individual accountability. It can assign blame to the individual members that operate misbehaving replicas regardless of the number of misbehaving replicas or members. IA-CCF achieves this by signing and logging BFT protocol messages in the ledger, and by using Merkle trees to provide clients with succinct, universally-verifiable receipts as evidence of successful transaction execution. Anyone can audit the ledger against a set of receipts to discover inconsistencies and identify replicas that signed contradictory statements. IA-CCF also supports changes to consortium membership and replicas by tracking signing keys using a sub-ledger of governance transactions. IA-CCF provides strong disincentives to misbehavior with low overhead: it executes 47,000 tx/s while providing clients with receipts in two network round trips.
△ Less
Submitted 8 March, 2022; v1 submitted 27 May, 2021;
originally announced May 2021.
-
AMP: Authentication of Media via Provenance
Authors:
Paul England,
Henrique S. Malvar,
Eric Horvitz,
Jack W. Stokes,
Cédric Fournet,
Rebecca Burke-Aguero,
Amaury Chamayou,
Sylvan Clebsch,
Manuel Costa,
John Deutscher,
Shabnam Erfani,
Matt Gaylor,
Andrew Jenks,
Kevin Kane,
Elissa Redmiles,
Alex Shamis,
Isha Sharma,
Sam Wenker,
Anika Zaman
Abstract:
Advances in graphics and machine learning have led to the general availability of easy-to-use tools for modifying and synthesizing media. The proliferation of these tools threatens to cast doubt on the veracity of all media. One approach to thwarting the flow of fake media is to detect modified or synthesized media through machine learning methods. While detection may help in the short term, we be…
▽ More
Advances in graphics and machine learning have led to the general availability of easy-to-use tools for modifying and synthesizing media. The proliferation of these tools threatens to cast doubt on the veracity of all media. One approach to thwarting the flow of fake media is to detect modified or synthesized media through machine learning methods. While detection may help in the short term, we believe that it is destined to fail as the quality of fake media generation continues to improve. Soon, neither humans nor algorithms will be able to reliably distinguish fake versus real content. Thus, pipelines for assuring the source and integrity of media will be required---and increasingly relied upon. We propose AMP, a system that ensures the authentication of media via certifying provenance. AMP creates one or more publisher-signed manifests for a media instance uploaded by a content provider. These manifests are stored in a database allowing fast lookup from applications such as browsers. For reference, the manifests are also registered and signed by a permissioned ledger, implemented using the Confidential Consortium Framework (CCF). CCF employs both software and hardware techniques to ensure the integrity and transparency of all registered manifests. AMP, through its use of CCF, enables a consortium of media providers to govern the service while making all its operations auditable. The authenticity of the media can be communicated to the user via visual elements in the browser, indicating that an AMP manifest has been successfully located and verified.
△ Less
Submitted 20 June, 2020; v1 submitted 22 January, 2020;
originally announced January 2020.
