Formal Model Guided Conformance Testing for Blockchains

• URL: http://arxiv.org/abs/2501.08550v2
• Date: Sat, 18 Jan 2025 19:54:08 GMT
• Title: Formal Model Guided Conformance Testing for Blockchains
• Authors: Filip Drobnjakovic, Amir Kashapov, Matija Kupresanin, Bernhard Scholz, Pavle Subotic,
• Abstract summary: We present a framework that performs protocol conformance testing using a formal model of the protocol. Our framework consists of two complementary components that use the components as trace generators and checkers.
• Score: 1.4838910416636741
• License:
• Abstract: Modern blockchains increasingly consist of multiple clients that implement a single blockchain protocol. If there is a semantic mismatch between the protocol implementations, the blockchain can permanently split and introduce new attack vectors. Current ad-hoc test suites for client implementations are not sufficient to ensure a high degree of protocol conformance. As an alternative, we present a framework that performs protocol conformance testing using a formal model of the protocol and an implementation running inside a deterministic blockchain simulator. Our framework consists of two complementary workflows that use the components as trace generators and checkers. Our insight is that both workflows are needed to detect all types of violations. We have applied and demonstrated the utility of our framework on an industrial strength consensus protocol.

Related papers

• Atomic Transfer Graphs: Secure-by-design Protocols for Heterogeneous Blockchain Ecosystems [7.312229214872541]
  We propose a framework for generating secure-by-design protocols that realize common security and functionality goals. The resulting protocols build upon Timelock Contracts (CTLCs), a novel minimal smart contract functionality. Our framework is the first to provide generic and provably secure protocols for all these use cases while matching or improving the performance of existing use-case-specific protocols.
  arXiv  Detail & Related papers  (2025-01-29T17:25:53Z)
• Commit0: Library Generation from Scratch [77.38414688148006]
  Commit0 is a benchmark that challenges AI agents to write libraries from scratch. Agents are provided with a specification document outlining the library's API as well as a suite of interactive unit tests. Commit0 also offers an interactive environment where models receive static analysis and execution feedback on the code they generate.
  arXiv  Detail & Related papers  (2024-12-02T18:11:30Z)
• BlockFound: Customized blockchain foundation model for anomaly detection [47.04595143348698]
  BlockFound is a customized foundation model for anomaly blockchain transaction detection. We introduce a series of customized designs to model the unique data structure of blockchain transactions. BlockFound is the only method that successfully detects anomalous transactions on Solana with high accuracy.
  arXiv  Detail & Related papers  (2024-10-05T05:11:34Z)
• The Latency Price of Threshold Cryptosystem in Blockchains [52.359230560289745]
  We study the interplay between threshold cryptography and a class of blockchains that use Byzantine-fault tolerant (BFT) consensus protocols. Existing approaches for threshold cryptosystems introduce a latency overhead of at least one message delay for running the threshold cryptographic protocol. We propose a mechanism to eliminate this overhead for blockchain-native threshold cryptosystems with tight thresholds.
  arXiv  Detail & Related papers  (2024-07-16T20:53:04Z)
• Sequencer Level Security [2.756899615600916]
  We introduce the Sequencer Level Security (SLS) protocol, an enhancement to sequencing protocols of rollups. We describe the mechanics of the protocol for both the transactions submitted to the rollup mempool, as well as transactions originating from Layer one. We implement a prototype of the SLS protocol, Zircuit, which is built on top of Geth and the OP stack.
  arXiv  Detail & Related papers  (2024-05-03T02:47:40Z)
• Atomicity and Abstraction for Cross-Blockchain Interactions [2.041399528183464]
  Current methods for multi-chain atomic transactions are limited in scope to cryptocurrency swaps. We first define a uniform, high-level interface for communication between chains. We then formulate a protocol that guarantees atomicity for general transactions whose operations may span several chains.
  arXiv  Detail & Related papers  (2024-03-12T02:13:29Z)
• 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)
• BlockEmulator: An Emulator Enabling to Test Blockchain Sharding Protocols [18.755112831811836]
  BlockEmulator is an experimental platform for emulating blockchain sharding mechanisms. It adopts a lightweight blockchain architecture so developers can only focus on implementing their new protocols or mechanisms. We have made BlockEmulator open-source in Github.
  arXiv  Detail & Related papers  (2023-11-06T23:45:11Z)
• Blockchain Large Language Models [65.7726590159576]
  This paper presents a dynamic, real-time approach to detecting anomalous blockchain transactions. The proposed tool, BlockGPT, generates tracing representations of blockchain activity and trains from scratch a large language model to act as a real-time Intrusion Detection System.
  arXiv  Detail & Related papers  (2023-04-25T11:56:18Z)
• Talaria: A Framework for Simulation of Permissioned Blockchains for Logistics and Beyond [19.988195564240577]
  Talaria is a novel permissioned blockchain simulator. It supports numerous protocols and use cases, most notably in supply chain management. Talaria is designed with both practical Byzantine Fault Tolerance (pBFT) and simplified version of Proof-of-Authority consensus protocols.
  arXiv  Detail & Related papers  (2021-03-03T08:43:30Z)
• Quantum Multi-Solution Bernoulli Search with Applications to Bitcoin's Post-Quantum Security [67.06003361150228]
  A proof of work (PoW) is an important cryptographic construct enabling a party to convince others that they invested some effort in solving a computational task. In this work, we examine the hardness of finding such chain of PoWs against quantum strategies. We prove that the chain of PoWs problem reduces to a problem we call multi-solution Bernoulli search, for which we establish its quantum query complexity.
  arXiv  Detail & Related papers  (2020-12-30T18:03:56Z)

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.