Smart Casual Verification of the Confidential Consortium Framework

• URL: http://arxiv.org/abs/2406.17455v2
• Date: Wed, 16 Oct 2024 12:14:29 GMT
• Title: Smart Casual Verification of the Confidential Consortium Framework
• Authors: Heidi Howard, Markus A. Kuppe, Edward Ashton, Amaury Chamayou, Natacha Crooks,
• Abstract summary: 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. This paper reports our experiences applying smart casual verification to validate the correctness of CCF's novel distributed protocols.
• Score: 2.160395257762205
• License:
• 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

Related papers

• Analogous Alignments: Digital "Formally" meets Analog [0.0]
  This paper focuses on the pragmatic formal verification of a mixed signal Intellectual Property (IP) that has a combination of digital and analog blocks. Digital and Analog Mixed-Signal (AMS) designs, which are fundamentally different in nature, are integrated seamlessly in a formal verification setup.
  arXiv  Detail & Related papers  (2024-09-23T13:38:31Z)
• Collaborative CP-NIZKs: Modular, Composable Proofs for Distributed Secrets [3.3373764108905455]
  Composability allows users to combine different specialized NIZKs. We present the first, general definition for collaborative commit-and-prove NIZK.
  arXiv  Detail & Related papers  (2024-07-27T08:45:34Z)
• Formally Certified Approximate Model Counting [25.20597060311209]
  We present the first certification framework for approximate model counting with formally verified guarantees on the quality of its output approximation. Our approach combines: (i) a static, once-off, formal proof of the algorithm's PAC guarantee in the Isabelle/HOL proof assistant; and (ii) dynamic, per-run, verification of ApproxMC's calls to an external CNF-XOR solver using proof certificates.
  arXiv  Detail & Related papers  (2024-06-17T11:02:04Z)
• A Survey and Comparative Analysis of Security Properties of CAN Authentication Protocols [92.81385447582882]
  The Controller Area Network (CAN) bus leaves in-vehicle communications inherently non-secure. This paper reviews and compares the 15 most prominent authentication protocols for the CAN bus. We evaluate protocols based on essential operational criteria that contribute to ease of implementation.
  arXiv  Detail & Related papers  (2024-01-19T14:52:04Z)
• Towards Auto-Modeling of Formal Verification for NextG Protocols: A Multimodal cross- and self-attention Large Language Model Approach [3.9155346446573502]
  This paper introduces Auto-modeling of Formal Verification with Real-world Prompting for 5G and NextG protocols (AVRE) AVRE is a novel system designed for the formal verification of Next Generation (NextG) communication protocols.
  arXiv  Detail & Related papers  (2023-12-28T20:41:24Z)
• Efficient Conformal Prediction under Data Heterogeneity [79.35418041861327]
  Conformal Prediction (CP) stands out as a robust framework for uncertainty quantification. Existing approaches for tackling non-exchangeability lead to methods that are not computable beyond the simplest examples. This work introduces a new efficient approach to CP that produces provably valid confidence sets for fairly general non-exchangeable data distributions.
  arXiv  Detail & Related papers  (2023-12-25T20:02:51Z)
• A General Framework for Verification and Control of Dynamical Models via Certificate Synthesis [54.959571890098786]
  We provide a framework to encode system specifications and define corresponding certificates. We present an automated approach to formally synthesise controllers and certificates. Our approach contributes to the broad field of safe learning for control, exploiting the flexibility of neural networks.
  arXiv  Detail & Related papers  (2023-09-12T09:37:26Z)
• Provably Secure Commitment-based Protocols over Unauthenticated Channels [0.0]
  We build a theoretic security framework to cover protocols whose characteristics may not always concur with existing models for authenticated exchanges. We propose a number of Commitment-based protocols to establish a shared secret between two parties, and study their resistance over unauthenticated channels. This means analyzing the security robustness of the protocol itself, and its robustness against Man-in-the-Middle attacks.
  arXiv  Detail & Related papers  (2023-07-28T10:35:35Z)
• Federated Conformal Predictors for Distributed Uncertainty Quantification [83.50609351513886]
  Conformal prediction is emerging as a popular paradigm for providing rigorous uncertainty quantification in machine learning. In this paper, we extend conformal prediction to the federated learning setting. We propose a weaker notion of partial exchangeability, better suited to the FL setting, and use it to develop the Federated Conformal Prediction framework.
  arXiv  Detail & Related papers  (2023-05-27T19:57:27Z)
• Joint Differentiable Optimization and Verification for Certified Reinforcement Learning [91.93635157885055]
  In model-based reinforcement learning for safety-critical control systems, it is important to formally certify system properties. We propose a framework that jointly conducts reinforcement learning and formal verification.
  arXiv  Detail & Related papers  (2022-01-28T16:53:56Z)
• CRFL: Certifiably Robust Federated Learning against Backdoor Attacks [59.61565692464579]
  This paper provides the first general framework, Certifiably Robust Federated Learning (CRFL), to train certifiably robust FL models against backdoors. Our method exploits clipping and smoothing on model parameters to control the global model smoothness, which yields a sample-wise robustness certification on backdoors with limited magnitude.
  arXiv  Detail & Related papers  (2021-06-15T16:50:54Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.