为区块链上的 Findel 衍生品提供认证
计算机科学中的逻辑
2020-05-29 v1
摘要
衍生品是一类用于对冲风险或投机市场波动的特殊金融合约。为避免歧义与误解，已提出多种用于指定此类衍生品的领域特定语言（DSL）。区块链技术的近期发展使得金融衍生品能够自动执行。一旦部署于区块链上，衍生品便不可修改。因此，应更加谨慎以避免不期望的情况。在本文中，我们处理以名为 Findel 的区块链 DSL 编写的金融衍生品的形式化验证。我们确定了一系列性质，一旦证明，便可排除若干安全漏洞（例如，不可变缺陷、资金损失）。我们开发了一个基础设施，提供交互式形式化并证明此类性质的手段。为提供更高置信度，我们还生成了证明证书。我们使用我们的基础设施来认证涵盖最常见衍生品类型（远期/期货、互换、期权）的非平凡示例。
引用
@article{arxiv.2005.13602,
title = {Certifying Findel Derivatives for Blockchain},
author = {Andrei Arusoaie},
journal= {arXiv preprint arXiv:2005.13602},
year = {2020}
}