Certifying Findel Derivatives for Blockchain

TL;DR

This paper presents a formal verification framework for blockchain-based financial derivatives written in the Findel DSL, ensuring security and correctness through proof certificates and interactive proofs.

Contribution

It introduces a novel infrastructure for formal verification of Findel derivatives, enabling proof of key properties to prevent vulnerabilities on blockchain.

Findings

Successfully verified properties of common derivatives like forwards, futures, swaps, and options.

Generated proof certificates to increase confidence in derivative correctness.

Identified security vulnerabilities that can be mitigated through formal proofs.

Abstract

Derivatives are a special type of financial contracts used to hedge risks or to speculate on the market fluctuations. In order to avoid ambiguities and misinterpretations, several domain specific languages (DSLs) for specifying such derivatives have been proposed. The recent development of the blockchain technologies enables the automatic execution of financial derivatives. Once deployed on the blockchain, a derivative cannot be modified. Therefore, more caution should be taken in order to avoid undesired situations. In this paper, we address the formal verification of financial derivatives written in a DSL for blockchain, called Findel. We identify a list of properties that, once proved, they exclude several security vulnerabilities (e.g., immutable bugs, money losses). We develop an infrastructure that provides means to interactively formalize and prove such properties. To provide a higher confidence, we also generate proof certificates. We use our infrastructure to certify non-trivial examples that cover the most common types of derivatives (forwards/futures, swaps, options).