ABSTRACT. Maximal Extractable Value (MEV) refers to a class of recent attacks to public blockchains, where adversaries with the power to reorder, drop or insert transactions in a block can "extract" value from user transactions in the mempool. Empirical research has shown that mainstream DeFi protocols, like e.g. Automated Market Makers and Lending Pools, are massively targeted by MEV attacks. This has detrimental effects on their users, on transaction fees, and on the congestion of blockchain networks. Despite the growing knowledge on MEV attacks to blockchain protocols, an exact definition is still missing. Indeed, formally defining these attacks is an essential prerequisite to the design of provably secure, MEV-free blockchain protocols. In this talk, we propose a formal definition of MEV, based on a general, abstract model of blockchains and smart contracts. We then introduce MEV-freedom, a property enjoyed by contracts resistant to MEV attacks. We validate this notion by rigorously proving that Automated Market Makers and Lending Pools are not MEV-free. We finally discuss how to design MEV-free contracts.

ABSTRACT. We provide three detailed case studies of vulnerabilities in smart contracts, and show how property based testing would have found them: 1. the Dexter1 token exchange; 2. the iToken; 3. the ICO of Brave's BAT token. The last example is, in fact, new, and was missed in the auditing process.

We have implemented this testing in ConCert, a general executable model/specification of smart contract execution in the Coq proof assistant. ConCert contracts can be used to generate verified smart contracts in Tezos' LIGO and rust. We thus show the effectiveness of combining formal verification and property-based testing of smart contracts.

ABSTRACT. Smart contracts on the Ethereum blockchain continue to suffer from well-published errors, leading to a lack of confidence in the whole Ethereum contract platform. A particular example is the very well-known smart contract reentrancy vulnerability, which still continues to be exploited. In this article, we present a method that provided a smart contract which may be vulnerable to such a reentrancy attack, and proceeds to attempt to automatically derive an “attacker” contract which can be used to successfully attack the vulnerable contract. The method uses property-based testing to generate, semi-randomly, large numbers of such potential attacker contracts and then checks whether any of them is a successful attacker.

ABSTRACT. Designing smart contracts in UTXO blockchains is often harder and less intuitive than in account-based ledger models. We present a novel way of structuring such applications, making use of a multi-threaded message-passing architecture built using the state machine paradigm for EUTxO contracts. We study this approach in the broader context of comparing account-based and UTxO ledger functionality. Specifically, we develop a specification for a simple account system, resembling that of account-based ledgers. We then present and compare a number of smart contracts we developed according to this specification: a naive implementation (which maintains all accounts monolithically in one contract), an optimized version using Merkle tries, a direct-transfer multi-threaded implementation, and finally culminating in a multi-threaded version with message-passing.

We argue that the multi-threaded approach allows for maximal parallelism by treating each account as an individual thread. We then assert that restricting state machine communication to message-passing, which are special kinds of UTxO entries, allows for maximal concurrency by making account state updates fully independent of each other, thereby also reducing static analysis complexity. We conjecture that due to its robust concurrency, parallelization, and reduced memory use properties, multi-threaded message-passing architecture would serve as a useful template for a broader class of contracts which includes accounts and extensions thereof.

ABSTRACT. This extended abstract describes ongoing work on a compliance test suite for FA2, a token standard for the Tezos blockchain. By embedding the test suite in the proof assistant Coq, we can prove the completeness of our suite, that is that any FA2-compliant contract must pass the test suite.

ABSTRACT. Proofgold is a peer to peer cryptocurrency making use of formal logic. Users can publish theories and then develop a theory by publishing documents with definitions, conjectures and proofs. The blockchain records the theories and their state of development (e.g., which theorems have been proven and when). Two of the main theories are a form of classical set theory (for formalizing mathematics) and an intuitionistic theory of higher-order abstract syntax (for reasoning about syntax with binders). We give examples definitions and theorems published into the Proofgold blockchain to demonstrate how the Proofgold network can be used to support formalization efforts. We have also significantly modified the open source Proofgold Core client software to create a faster, more stable and more efficient client, Proofgold Lava. Two important changes are the cryptography code and the database code, and we discuss these improvements.

ABSTRACT. Achieving consistency in modern large-scale and fault-tolerant distributed systems often relies on intricate consensus protocols. Ensuring the reliability of implementations of such protocols remains a significant challenge because of the enormous number of exceptional conditions that may arise in production. We propose a methodology and a tool called Netrix for testing such implementations that aims to exploit programmer's knowledge to improve coverage, enables robust bug reproduction, and can be used in regression testing across different versions of an implementation. As a case-study and evaluation, we apply our tool to a popular proof of stake blockchain protocol, Tendermint, which relies on a Byzantine consensus algorithm and to a popular benign consensus algorithm, Raft. We were able to identify deviations of the implementation from the protocol specification and verify corrections on an updated implementation.

ABSTRACT. Ensuring deterministic behaviour in distributed blockchain ledger design matters to end users because it allows for locally predictable fees, smart contract evaluation outcomes, and updates to other ledger-tracked data. In this work we begin by defining an abstract interface of ledgers and its update procedure, which gives us the ability to make formal comparisons of different ledger designs across various properties. We use this model as a basis for formalizing and studying several properties colloquially classified as determinism of ledgers.

We identify a stronger and a weaker definition of determinism, providing simple but illustrative examples. We situate both versions of determinism in the context of the theory of changes, and conjecture what constraints on the derivation of ledger update functions are sufficient and necessary for the two definitions. We additionally discuss substates of a ledger state, which we refer to as threads, and outline how particular threads can remain deterministic while the full ledger may not be.

We discuss how these ideas can be applied to realistic ledgers' designs and architectures, and analyze a nuanced example of non-determinism in an existing UTxO ledger with the tools we have developed.

ABSTRACT. Cardano is a third generation crypto currency developed by IOG whose nodes consist of a network layer, a consensus layer, and a ledger layer. The ledger tracks and validates financial transactions.

The ledger team at IOG has been successful in using a combination of an abstract specification of the ledger, modeled as a small-step operational semantics and written in LaTeX, pen-and-paper proofs, and property based testing using QuickCheck to support the implementation of this critical component of the system. The specification serves as a design document and reference for the team, and also other members of the Cardano ecosystem. However, LaTeX provides no scope or type checking of the model, and there is a tendency for the spec to get out of sync with the rapidly changing implementation. To mitigate both of these problems, and improve on what we already have, we are developing a specification in Agda which is both human and machine readable. This will provide higher assurance and easier maintenance than the current specification via scope and type checking of the current specification. Additionally, we derive a reference implementation from this model via meta-programming, which can be used for conformance testing against the implementation. Last but not least, we can perform machine checked proofs of key properties.

ABSTRACT. Blockchains are maintained by a network of participants, miner nodes, that run algorithms designed to maintain collectively a distributed machine tolerant to Byzantine attacks. From the point of view of users, blockchains provide the illusion of centralized computers that perform trustable verifiable computations, where all computations are deterministic and the results cannot be manipulated or undone. Every blockchain is equipped with a crypto-currency. Programs running on blockchains are called smart-contracts and are written in a special-purpose programming language with deterministic semantics. Each transaction begins with an invocation from an external user to a smart contract. Smart contracts have local storage and can call other contracts, and more importantly, they store, send and receive cryptocurrency. Once installed in a blockchain, the code of the smart-contract cannot be modified. Therefore, it is very important to guarantee that contracts are correct before deployment. However, the resulting ecosystem makes it very difficult to reason about program correctness, since smart-contracts can be executed by malicious users or malicious smart-contracts can be designed to exploit other contracts that call them. Many attacks and bugs are caused by unexpected interactions between multiple contracts, the attacked contract and unknown code that performs the exploit. Moreover, there is a very aggressive competition between different blockchains to expand their user base. Ideas are implemented fast and blockchains compete to offer and adopt new features quickly. In this paper, we propose a formal playground that allows reasoning about multi-contract interactions and is extensible to incorporate new features, study their behaviour and ultimately prove properties before features are incorporated into the real blockchain. We implemented a model of computation that models the execution platform, abstracts the internal code of each individual contract and focuses on contract interactions. Even though our Coq implementation is still a work in progress, we show how many features, existing or proposed, can be used to reason about multi-contract interactions.

ABSTRACT. Game-theoretic approaches provide new ways to model and formally prove security properties of off-chain protocols. For complex protocols, carrying out such formal proofs is a cumbersome and error-prone task. We describe our ongoing efforts for automating the security analysis of off-chain protocols. We encode the game-theoretic protocol model, together with its security properties, as universally quantified formulas, and use SMT solving to enforce these properties.