论文标题
证明区块链的Findel衍生物
Certifying Findel Derivatives for Blockchain
论文作者
论文摘要
衍生品是用于对冲风险或推测市场波动的一种特殊类型的金融合同。为了避免歧义和误解，已经提出了用于指定此类衍生物的几种特定域（DSL）。区块链技术的最新发展使金融导数的自动执行。部署在区块链上后，无法修改衍生物。因此，应采取更多谨慎，以避免不希望的情况。 在本文中，我们介绍了用DSL为区块链编写的金融衍生工具的正式验证，称为Findel。我们确定了一份属性列表，一旦证明，它们都排除了几个安全漏洞（例如，不可变的错误，货币损失）。我们开发了一种基础架构，该基础架构提供了交互式形式化和证明此类属性的手段。为了提供更高的信心，我们还生成了证明证书。我们使用基础架构来证明涵盖最常见类型的衍生品（正向/期货，掉期，选项）的非平凡示例。
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).
