ABSTRACT. The Scilla project has started in late 2017 as a 100-lines-of-code prototype implemented in Coq proof assistant. Learning from the mistakes of Ethereum, which had pioneered the area of blockchain-based applications (aka smart contracts), the aim of Scilla was to provide a smart contract language, which is expressive enough to accommodate most of the reasonable use-cases, while allowing for scalable and tractable formal verification and analysis. As such, Scilla has been positioned as an intermediate-level language, suitable to serve as a compilation target and also as an independent programming framework. Two years later, Scilla is now powering the application layer of Zilliqa, the world's first publicly deployed sharded blockchain system. Since its public launch less than a year ago, dozens of unique smart contracts implemented in Scilla have been deployed, including custom tokens, collectibles, auctions, multiplayer games, name registries, atomic token swaps, and many others. In my talk, I will describe the motivation, design principles, and semantics of Scilla, and outline the main use cases and the tools provided by the developer community. I will also present a framework for lightweight verification of Scilla programs, and showcase it with two automated domain-specific analyses. Finally, I will discuss the pragmatic pitfalls of designing a new smart contract language from scratch, and present the future exciting research directions that are enabled by Scilla's take on smart contract design.

ABSTRACT. Smart contracts are programs that run on a distributed ledger platform. They usually manage resources representing valuable assets. Moreover, their source code is visible to potential attackers, they are distributed, and bugs are hard to fix. Thus, they are susceptible to attacks exploiting programming errors. Their vulnerability makes a rigorous formal analysis of the functional correctness of smart contracts highly desirable. In this short paper, we show that the architecture of smart contract platforms offers a computation model for smart contracts that yields itself naturally to deductive program verification. We discuss different classes of correctness properties of distributed ledger applications, and show that design-by-contract verification tools are suitable to prove these properties. We present experiments where we apply the KeY verification tool to smart contracts in the Hyperledger Fabric framework which are implemented in Java and specified using the Java Modeling Language.

ABSTRACT. In this paper, we use a formal language that performs deductive verification on industrial smart contracts, which are self-executing digital programs. Because smart contracts manipulate cryptocurrency and transaction information, if a bug occurs in such programs, serious consequences can happen, such as a loss of money. The aim of this paper is to show that a language dedicated to deductive verification, called Why3, can be a suitable language to write correct and proven contracts. We first encode existing contracts into the Why3 program; next, we formulate specifications to be proved as the absence of RunTime Error and functional properties, then we verify the behaviour of the program using the Why3 system. Finally, we compile the Why3 contracts to the Ethereum Virtual Machine (EVM). Moreover, our approach estimates the cost of gas, which is a unit that measures the amount of computational effort during a transaction.

ABSTRACT. Smart contracts are programs that constitute the main ingredients of decentralized applications (DApps) running on top of blockchain networks like Ethereum, EOS or Tezos. From a computing point of view, smart contracts are reminiscent to distributed objects used through several entry points by an unknown number of \emph{accounts}. Like any (concurrent) program, smart contracts may have bugs. But contrary to traditional applications, once deployed on a blockchain, dApps can neither be removed nor modified. Unfortunately, but not surprisingly, it has recently been revealed that a large number of smart contractscontain critical security vulnerabilities.

To help dApps programmers, we propose in this paper to model smart contracts into the declarative input language of Cubicle, a model checker for parameterized systems based on SMT. In our approach, smart contract code, as well as the transactional model of the blockchain, are encoded as a state machine on which safety properties of interest are encoded and verified. We show the success of our technique through the simple yet prime example of an auction. This preliminary result is very promising and lays the foundations for a complete and automatized framework for the design and certification of smart contracts.

ABSTRACT. Callbacks in Smart Contracts on blockchain-based distributed ledgers are a potential source of security vulnerabilities: callbacks may lead to reentrancy, which has been previously exploited to steal large sums of money. Unfortunately, analysis tools for Smart Contracts either fail to support callbacks or simply detect and disallow patterns of callbacks that may lead to reentrancy. As a result, many authors of Smart Contracts avoid callbacks altogether, and some Smart Contract programming languages, including Solidity, recommend using primitives that avoid callbacks. Nevertheless, reentrancy remains a threat, due to the utility of and frequent reliance on callbacks in Smart Contracts.

In this paper, we propose the use of _type invariants_, a feature of some languages supporting formal verification, to enable proof of correctness for Smart Contracts, including Smart Contracts that permit or rely on callbacks. Our result improves upon existing research because it neither forbids reentrancy nor relies on informal, meta-arguments to prove correctness of reentrant Smart Contracts. We demonstrate our approach using the SPARK programming language, which supports type invariants and moreover can be compiled to relevant blockchains.

ABSTRACT. RANDAO is a commit-reveal scheme for generating pseudo-random numbers in a decentralized fashion. The scheme is used in emerging blockchain systems as it is widely believed to provide randomness that is unpredictable and hard to manipulate by maliciously behaving nodes. However, RANDAO may still be susceptible to look-ahead attacks, in which an attacker (controlling a subset of nodes in the network) may attempt to pre-compute the outcomes of (possibly many) reveal strategies, and thus may bias the generated random number to his advantage. In this work, we formally evaluate resilience of RANDAO against such attacks. We first develop a probabilistic model in rewriting logic of RANDAO, and then apply statistical model checking and quantitative verification algorithms (using \textsc{Maude} and \textsc{PVeStA}) to analyze two different properties that provide different measures of bias that the attacker could potentially achieve using pre-computed strategies. We show through this analysis that unless the attacker is already controlling a sizable percentage of nodes while aggressively attempting to maximize control of the nodes selected to participate in the process, the expected achievable bias is quite limited.

ABSTRACT. Bitcoin is currently still the most widely used cryptocurrency, judging from its market cap and trade volume. A big part of Bitcoin's appeal is the mining process, which makes sure that new transactions are being validated and processed in a distributed fashion, maintaining a distributed ledger known as the blockchain. Miners receive a fee for every block of transactions that they mine, as an incentive for their computational effort. In the long run, they can expect a reward proportional to the computational power they provide to the network.

However, Eyal and Sirer introduced a strategy for a miner to time the publishing of blocks that will give them a significant edge in profits. This paper models the behaviour of honest and selfish mining pools in UPPAAL, analysing properties of the mining process in the presence of network delay, and taking into account the distributed nature of the process. This shows what effects selfish mining would have on the share of profits, but also on the number of orphaned blocks in the blockchain. This analysis allows us to compares those results to real-world data, to establish if there is evidence for the presence of selfish miners.

ABSTRACT. The Algorand blockchain is a secure and decentralized public ledger based on pure proof of stake rather than proof of work. At its core is a novel consensus protocol with exactly one block certified in each round: that is, the protocol guarantees that the blockchain does not fork. In this paper, we report on our effort to model and formally verify the Algorand consensus protocol in the Coq proof assistant. Similarly to in previous consensus protocol verification efforts, we model the protocol as a state transition system and reason over reachable global states. However, in contrast to previous work, our model explicitly incorporates timing issues (e.g., timeouts and network delays) and adversarial actions, reflecting a more realistic environment faced by a public blockchain. Thus far, we have proved asynchronous safety of the protocol: two different blocks cannot be certified in the same round, even when the adversary has complete control of message delivery in the network. We believe that our model is sufficiently general and other relevant properties of the protocol such as liveness can be proved for the same model.

ABSTRACT. The recent release of Solidity 0.5 introduced a new type to prevent Ether transfers to smart contracts that are not supposed to receive money. Unfortunately, the compiler fails in enforcing the guarantees this type intended to convey, hence the type soundness of Solidity 0.5 is no better than that of Solidity 0.4. In this paper we discuss a paradigmatic example showing that vulnerable Solidity patterns based on potentially unsafe callback expressions are still unchecked. We also point out a solution that strongly relies on formal methods to support a type-safer smart contracts programming discipline, while being retro-compatible with legacy Solidity code.

ABSTRACT. We propose a novel way of embedding functional smart contract languages into the Coq proof assistant using meta-programming techniques. Our framework allows for developing the meta-theory of smart contract languages using the deep embedding and provides a convenient way for reasoning about concrete contracts using the shallow embedding. The proposed approach allows to make a connection between the two embeddings in a form of a soundness theorem. As an instance of our approach we develop an embedding of the Oak smart contract language in Coq and verify several important properties of a crowdfunding contract. The developed techniques are applicable to all functional smart contract languages.

ABSTRACT. Tezos is a blockchain launched in June 2018. It is written in OCaml and supports smart contracts. Michelson is the smart contract language of Tezos and has been designed with formal verification in mind. In this article, we present Mi-Cho-Coq, a Coq library for verifying the functional correctness of Michelson smart contracts. As a study case, we detail the certification of a Multisig contract with the Mi-Cho-Coq framework.

ABSTRACT. We present a novel Coq formalization of smart contract execution in blockchains. Our formalization allows for inter-contract communication and generalizes existing work by allowing modelling of both depth-first execution blockchains (like Ethereum) and breadth-first execution blockchains (like Tezos). We represent smart contracts as simple functions and thus allow writing contracts directly in Coq's functional language Gallina, enabling easier reasoning about functional correctness of concrete contracts than other approaches. In particular we develop a Congress contract in this style. This contract -- a simplified version of the infamous DAO -- is interesting because of its very dynamic communication pattern with other contracts. We give a high-level partial specification of the Congress's behavior, related to reentrancy, and prove that the Congress satisfies it for all possible smart contract execution orders.

ABSTRACT. As smart contracts are growing in size and complexity, it becomes harder and harder to ensure their correctness and security. Due to the lack of isolation mechanisms a single mistake or vulnerability in the code can bring the whole system down, and due to this smart contract upgrades can be especially dangerous. Traditional ways to ensure the security of a smart contract, including DSLs, auditing and static analysis, are used before the code is deployed to the blockchain, and thus offer no protection after the deployment. After each upgrade the whole code need to be verified again, which is a difficult and time-consuming process that is prone to errors. To address these issues a security protocol and framework for smart contracts called Cap9 was developed. It provides developers the ability to perform upgrades in a secure and robust manner, and improves isolation and transparency through the use of a low level capability-based security model. We have used Isabelle/HOL to develop a formal specification of the Cap9 framework and prove its consistency. The paper presents a refinement-based approach that we used to create the specification, as well as discussion of some encountered difficulties during this process.