ABSTRACT. At the core of the Ethereum network is the Ethereum Virtual Machine (EVM) which can execute programs written in EVM bytecode. This remarkable feature empowers users to define complex business logic that can be executed programmatically by programs called smart contracts.

Smart contracts are programs and may contain bugs. There are several examples of smart contract vulnerabilities that have been exploited in the past: in 2016, a re-entrance vulnerability in the Decentralised Autonomous Organisation (DAO) smart contract was exploited to steal more than USD50 Million. The total value netted from DeFi hacks in 2023 is estimated to be more than $1.5 billion.

In this talk I will discuss formal verification of smart contracts. The main technique is deductive verification supported by the verification-friendly language Dafny. I will show how we can use deductive verification to reason about smart contracts, from high-level specifications (Dafny), to intermediate representation (Yul) and finally low-level EVM bytecode.

ABSTRACT. There is a trend in blockchains to switch to DAG-based consensus protocols to decrease their energy footprint and improve security. A DAG-based consensus protocol orders transactions for securing blocks, and relies on built-in fault tolerance communications via Byzantine Atomic Broadcasts. The ubiquity and strategic importance of blockchains call for formal proof of their correctness.

We formalize the DAG-based consensus protocol called DAG-Rider in TLA+ and prove the desirable safety properties with the TLA+ proof system. The formalization requires a refinement approach for modelling the consensus. In an abstracted model, we first show the safety of DAG-based consensus on leaders and then further refine the specification to encompass all messages for all processes. The specification consists of 226 number of lines, and the proof system verifies 1922 obligations in approx. 5 minutes.

ABSTRACT. Blockchain systems comprise critical software that handle substantial monetary funds, rendering them excellent candidates for formal verification. One of their core components is the underlying ledger that does all the accounting: keeping track of transactions and their validity, etc.

Unfortunately, previous theoretical studies are typically confined to an idealized setting, while specifications for real implementations are scarce; either the functionality is directly implemented without a proper specification, or at best an informal specification is written on paper.

The present work expands beyond prior meta-theoretical investigations of the EUTxO model to encompass the full scale of the Cardano blockchain: our formal specification describes a hierarchy of modular transitions that covers all the intricacies of a realistic blockchain, such as fully expressive smart contracts and decentralized governance.

It is mechanized in a proof assistant, thus enjoys a higher standard of rigor: type-checking prevents minor oversights that were frequent in previous informal approaches; key meta-theoretical properties can now be formally proven; it is an executable specification against which the implementation in production is being tested for conformance; and it provides firm foundations for smart contract verification.

Apart from a safety net to keep us in check, the formalization also provides a guideline for the ledger design: one informs the other in a symbiotic way, especially in the case of state-of-the-art features like decentralized governance, which is an emerging sub-field of blockchain research that however mandates a more exploratory approach.

All the results presented in this paper have been mechanized in the Agda proof assistant and are publicly available. In fact, this document is itself a literate Agda script and all rendered code has been successfully type-checked.

ABSTRACT. Decentralized Finance (DeFi) has emerged as a contemporary competitive as well as complementary to the traditional centralized finance systems. As of 23rd January 2024, per Defillama approximately USD 55 billion is the total value locked on the DeFi applications on all blockchains put together.

A Byzantine Fault Tolerant (BFT) State Machine Replication (SMR) protocol, popularly known as consensus protocol, is the central component of a blockchain. Possible forks in a consensus protocol imply possible double spending attacks and are catastrophic given high volumes of finance that are transacted on blockchains. Formal verification of the safety of the consensus protocols provide the highest guarantee possible but is considered as complex and challenging. This is reflected by the fact that not many complex consensus protocols are formally verified except for Tendermint.

We focus on Supra's Chained Moonshot consensus protocol. Similar to Tendermint's formal verification, we too model Chained Moonshot using IVy and formally prove that for all network sizes, as long as the number of Byzantine validators is less than the 1/3, the protocol never forks, thus proving that Chained Moonshot is safe and double spending is not possible.

ABSTRACT. A blockchain acts as a universal ledger for digital transactions between two parties that require no moderation from a third party. Such transactions are cheaper, quicker, and more secure with high traceability and transparency, with the decentralised structure of a blockchain network allowing for greater scalability and availability. For these reasons, blockchain is at the forefront of emerging technologies, with a wide variety of industries investing billions into the technology. A blockchains consensus protocol is what allows a blockchain network to be decentralised but can be subject to malicious behaviour and faults in its design and implementation that can lead to catastrophic effects like the DAO hack that resulted in a loss of $60 million. From this it is clear to see that the verifications of these protocols are paramount to ensure the safe use of blockchain. In this research, we formally verify the Proof-of-Work consensus protocol, used by Bitcoin, in Isabelle/HOL by modelling the blockchain as the longest branch in a binary tree and proving that the common prefix property holds with the assumption that the network is majority honest. In this paper, we discuss the validity of our approach, key functions and lemmas we used to complete the proof, advantages and drawbacks of the model, related work and how this research can be taken further.

ABSTRACT. Smart contracts are programs stored on the blockchain. They are usually developed in a high-level programming language, the most popular of which being Solidity. Smart contracts are often used to automate financial transactions and thus, vulnerabilities in smart contracts can result in high financial losses. Therefore, it is important to guarantee their correctness which is best done using verification. To this end, we developed Isabelle/Solidity, a deep embedding of Solidity in Isabelle. In the following, we describe our work on Isabelle/Solidity. We first describe the supported subset of the language and how it is evaluated. Then, we take a brief look at various applications of Isabelle/Solidity. Finally, we discuss ongoing and future work on Isabelle/Solidity.

ABSTRACT. Automated Market Makers (AMMs) are an integral component of the decentralized finance (DeFi) ecosystem, as they allow users to exchange crypto-assets without the need for trusted authorities or external price oracles. Although these protocols are based on relatively simple mechanisms, e.g., to algorithmically determine the exchange rate between crypto-assets, they give rise to complex economic behaviours. This complexity is witnessed by the proliferation of models that study their structural and economic properties. Currently, most of theoretical results obtained on these models are supported by pen-and-paper proofs. This work proposes a formalization of constant-product AMMs in the Lean 4 Theorem Prover. To demonstrate the utility of our model, we provide mechanized proofs of key economic properties like arbitrage, that at the best of our knowledge have only been proved by pen-and-paper before.

ABSTRACT. Formal verification of smart contracts has become a hot topic in academic and industrial research, given the growing value of assets managed by decentralized applications and the consequent incentive for adversaries to tamper with them. Most of the current research on the verification of smart contracts revolves around Solidity, the main high-level language supported by Ethereum and other leading blockchains. Although bug detection tools for Solidity have been mushrooming almost since the introduction of Ethereum, only in the last few years we have seen formal verification tools capable of proving that a given smart contract respects some desirable properties. In the realm of general-purpose programming languages, for this kind of tools there are well-established methodologies for benchmarking their effectiveness and efficiency. Instead, the issue of comparing different verification tools for Solidity is largely unexplored. We address this problem by proposing an open benchmark for Solidity verification tools. We apply our benchmark to compare the effectiveness of two leading tools, SolCMC and Certora.

ABSTRACT. Smart contract upgrades are costly from a verification perspective and can be a meaningful source of vulnerabilities when done incorrectly. Unfortunately, there is no established, formal framework through which one can reason about contracts as they undergo upgrades, though much work has been done to verify standalone smart contracts. Instead, one must repeat the full verification process for each contract upgrade, something which relies heavily on fallible intuition, can lead to unexpected vulnerabilities, and drives up the cost of formally verifying smart contracts. We propose a formal framework for contract upgrades in ConCert, a Coq-based smart contract verification tool. Central to this framework is our notion of a contract morphism, a theoretical tool which we introduce to formally encode structural relationships between smart contracts, and with which we can formally specify and verify an upgraded contract relative to its previous versions. We argue that ours is a natural framework for specifying and verifying contract upgrades, and hope to offer a first step towards rigorous, efficient specification and verification of contract upgrades.

ABSTRACT. Smart contracts are programs which manage resources in blockchain networks in an automated fashion. In this context, liveness properties are often essential: If I transfer money to a contract, will I eventually get it back?

This kind of property can be hard to specify and verify, in particular because application-specific fairness assumptions w.r.t. function invocation and the behavior of other parties are usually necessary for any liveness proof to succeed. In this work, we analyse smart contract liveness properties discussed in the literature. We find that the smart contract paradigm of decentralisation and trustlessness induces a certain, commonly occurring kind of liveness property which is tied to the ability of an agent to induce a state change, e.g., a transfer of resources. We introduce some formal specification concepts which capture this notion of liveness. We also show how this can simplify verification of liveness properties compared to existing approaches.

ABSTRACT. The Aptos Framework is a collection of smart contracts written in the Move language that define standard and common on-chain actions for the Aptos Network. As the security and safety of the Aptos Framework is of utmost importance, it has continuously undergone rigorous testing and comprehensive auditing. To further increase the level of assurance, we have formally verified its security and correctness. This involves identifying critical security requirements for each module, creating formal specifications, and subsequently verifying them using the Move Prover. To the best of our knowledge, this represents one of the first instances of formal verification being applied on such a large scale in a smart contract framework. This paper discusses how this rigorous effort ensures a high level of quality assurance for the Aptos Framework.

ABSTRACT. Blockchain ledgers based on the extended UTxO model support fully expressive smart contracts to specify permissions for performing certain actions, such as spending transaction outputs or minting assets. There have been some attempts to standardize the implementation of stateful programs using this infrastructure, with varying degrees of success. To remedy this, we introduce the framework of structured contracts to formalize what it means for a stateful program to be correctly implemented on the ledger. Using small-step semantics, our approach relates low-level ledger transitions to high-level transitions of the smart contract being specified, thus allowing users to prove that their abstract specification is adequately realized on the blockchain. We argue that the framework is versatile enough to cover a range of examples, in particular proving the equivalence of multiple concrete implementations of the same abstract specification. Building upon prior meta-theoretical results, our results have been mechanized in the Agda proof assistant, paving the way to rigorous verification of smart contracts.