ABSTRACT. Merkle trees are ubiquitous in blockchains and other distributed ledger technologies (DLTs). They guarantee that the involved systems are referring to the same binary tree, even if each of them knows only a subtree. Inclusion proofs allow knowledgeable systems to share subtrees with other systems and the latter can verify the subtrees’ authenticity. Often, blockchains and DLTs use data structures more complicated than binary trees; authenticated data structures generalize Merkle trees to such structures.

We show how to formally define and reason about authenticated data structures, their inclusion proofs, and operations thereon as datatypes in Isabelle/HOL. Our approach is modular and allows us to construct complicated trees from reusable building blocks, which we call Merkle functors. Merkle functors include sums, products, and function spaces and are closed under composition and least fixpoints. As a practical application, we model the hierarchical transactions of Canton, a practical interoperability protocol for distributed ledgers, as authenticated data structures. This is a first step towards formalizing the Canton protocol and verifying its integrity and security guarantees.

ABSTRACT. We present the first formal model of Bitcoin's transaction and blockchain data structures including the formalization of the blockchain validation procedures. Our formal model, though still a simplified representation of an actual Bitcoin blockchain, includes regular and coinbase transactions, segregated witnesses, relative and absolute locktime, the Bitcoin Script language expressions together with a denotational semantics, transaction fees and block rewards. We formally specify the details of consistency and validity checks performed when adding new blocks to the blockchain. We assume perfect cryptography and use the symbolic approach for modeling hash functions and digital signatures.

To demonstrate the utility of the model, we formally state and prove several essential properties of a consistent blockchain --- transactions are unique, each coin can be spent at most once and the new value is only created through block rewards.The model and the proofs are largely independent of Bitcoin specific details and easily generalize to any cryptocurrency blockchain based on the Unspent Transaction Output (UTXO) paradigm.

We mechanize all the results using the Coq proof assistant.

The model and the proofs are largely independent of Bitcoin specific details and easily generalize to any cryptocurrency blockchain based on the Unspent Transaction Output (UTXO) paradigm.

We mechanize all the results using the Coq proof assistant.

ABSTRACT. We try to verify properties of the bitcoin-s library, a Scala implementation of parts of the Bitcoin protocol. We use the Stainless verifier which supports programs in a fragment of Scala called Pure Scala. Since bitcoin-s is not written in this fragment, we extract the relevant code from it and perform a series of equivalent transformations until we arrive at code that we successfully verify. In that process we find and fix two bugs in bitcoin-s.

ABSTRACT. The Stellar Network relies on the Stellar Consensus Protocol (SCP) to repeatedly agree on the next block to add to its blockchain. At a high level, SCP is a quorum-based Byzantine Fault-Tolerant consensus protocol similar to the protocols used in permissioned blockchains such as Tendermint and HotStuff. However, SCP works in a permissionless model in which a quorum-system emerges from the participant's self-declared trust in each other.

SCP poses unique formal-verification challenges due to it's reliance on an underlying trust structure with particular connectivity properties. In this paper, we describe the formal verification technique that we deploy to verify SCP's safety and liveness properties for an arbitrary but fixed configuration (i.e. participants do not join or leave the system dynamically).

We model this parameterized, infinite-state system in first-order logic and we verify its safety properties, using Ivy, by providing suitable inductive invariants that are checked fully automatically. A liveness to safety reduction implemented in Ivy allows us to verify liveness using inductive invariants too. Finally, we verify the soundness of the first-order model of Stellar's quorum system with respect to a more straightforward higher-order model in Isabelle/HOL.

ABSTRACT. Blockchain synchronization is one of the core protocols of Tendermint blockchains. In this short paper, we discuss our recent efforts in formal specification of the protocol and its implementation, as well as some initial model checking results. We demonstrate that the protocol quality and understanding can be improved by writing specifications and model checking them.

ABSTRACT. The main incentives of blockchain technology are distribution and distributed change, consistency, and consensus. Beyond just being a distributed ledger for digital currency, smart contracts add transaction protocols to blockchains to execute terms of a contract in a blockchain network. Inter-blockchain (IBC) protocols define and control exchanges between different blockchains. The Isabelle Infrastructure framework serves security and privacy for IoT architectures by formal specification and stepwise attack analysis and refinement. A major case study of this framework is a distributed health care scenario for data consistency for GDPR compliance. This application led to the development of an abstract system specification of blockchains for IoT infrastructures. In this paper, we first give a summary of the concept of IBC. We then introduce an instantiation of the Isabelle Infrastructure framework to model blockchains. Based on this we exend this model to instantiate different blockchains and formalise IBC protocols. We prove the concept by defining the generic property of global consistency and prove it in Isabelle.

ABSTRACT. Smart contract verification is becoming increasingly important. The ConCert smart contract verification framework in Coq allows for proving properties of functional smart contracts and formalises a contract execution model. We take the next steps in the ConCert development. We extend ConCert with the extraction functionality for obtaining certified code in a functional smart contract language from the Coq implementation of a smart contract. The extraction is exemplified by several simple use cases, including an example of a contract that uses dependent types, thus showing that our extraction is able to handle non-trivial transformations. We implement anonymous voting based on the Open Vote Network protocol in ConCert. This provides a smart contract for boardroom voting with maximum voter privacy such that each vote is kept private except under collusion of all other parties. The contract itself orchestrates the computation of the final tally and is proven functionally correct, meaning that it cannot compute a wrong tally. With ConCert's executable specification our contracts are furthermore fully testable from within Coq. This enables us to integrate property-based testing into ConCert using QuickChick. We show that this is successful by testing complex contracts such as the congress contract (the essence of TheDAO) and the Tezos FA2 token standard.

ABSTRACT. Bitcoin contracting protocols regulate the transfer of bitcoins amongst participants in a trustless manner. A safe and secure contract design should feature collaborative execution traces, but also allow the verifying actor to reach a safe terminal state despite any potentially adversarial actions by the counter-party. Trace-Net is a proposed Petri Net formalism extended with a stateful actor knowledge model. A Trace-Net model is lifted from raw Bitcoin contract transactions, enabling the contract to be verified at the raw Bitcoin transaction level: Verification can therefore be performed at at run-time, and does not require manually generated contract specifications. This extended abstract summarizes the recently published Bitcoin contract verification method named Trace-Net, which is sufficiently expressive for the verification of complex contracts including off-chain state channels and contracts featuring cryptographic sub-protocols unobservable on the blockchain.

ABSTRACT. Bilinear pairings are integral for deploying privacy-preserving cryptocurrencies, as they represent a fundamental building block for the zero-knowledge proofs required for security. Due to many optimizations implementations of these can be hard to verify in a post hoc way. Recently, an alternative path for implementing cryptographic libraries was demonstrated as viable in the Fiat-Crypto framework. By combining correct-by-design optimized low-level code with automatically generated and formally verified high-level code, it became possible to develop libraries which are both efficient and formally verified. The approach was illustrated through the implementation of field arithmetic for several standardized elliptic curves using an extensible code generation framework, capable of producing code competitive in performance with popular hand-optimized multi-precision libraries. The verification steps are conducted using the Coq proof assistant. Using these techniques, we generate a verified and efficient C-implementation of a constant-time field inversion algorithm, a key building-block of bilinear pairings.

ABSTRACT. We present Albert, an intermediate smart-contract language for Tezos. Contracts stored in the Tezos blockchain are written in a low-level stack-based language called Michelson. Albert is a higher-level language: Michelson stacks are abstracted as linearly typed records. In this Extended Abstract, we also briefly describe its compiler to Michelson. This compiler is written in Coq, and targets Mi-Cho-Coq, a formal specification of Michelson implemented in Coq.

ABSTRACT. This paper introduces WhylSon, a deductive verification tool for smart contracts written in Michelson, the low-level language of the Tezos blockchain. WhylSon accepts a formally specified Michelson contract and automatically translates it to an equivalent program written in WhyML, the programming and specification language of the Why3 framework. Smart contract instructions are mapped into a corresponding WhyML shallow-embedding of the their axiomatic semantics, which we also developed in the context of this work. One major advantage of this approach is that it allows an out-of-the-box integration with the Why3 framework, namely its VCGen and the backend support for several automated theorem provers. We discuss the use of WhylSon to automatically prove the correctness of diverse smart contracts, and detail on the case study of proving correct a multisig Tezos smart contract.