Decentralized finance (DeFi) has become one of the most successful applications of blockchain and smart contracts. The DeFi ecosystem enables a wide range of crypto-financial activities, while the underlying smart contracts often contain bugs, with many vulnerabilities arising from the unforeseen consequences of composing DeFi protocols together. In this paper, we propose a formal process-algebraic technique that models DeFi protocols in a compositional manner to allow for efficient property verification. We also conduct a case study to demonstrate the proposed approach in analyzing the composition of two interacting DeFi protocols, namely, Curve and Compound. Finally, we discuss how the proposed modeling and verification approach can be used to analyze financial and security properties of interest.

翻译：分散化金融(DeFi)已成为最成功的连锁和智能合同应用之一。DeFi生态系统使各种加密金融活动得以进行,而基础智能合同往往含有错误,许多脆弱性产生于共同制定DeFi协议的意外后果。在本文件中,我们提出一种正式的流程代数技术,以组成方式模式来模拟DeFi协议,以便有效地进行财产核查。我们还进行了一项案例研究,以证明在分析两个相互作用的 DeFi协议(即Curve和Complus)的组成方面拟议采用的方法。最后,我们讨论了如何利用拟议的建模和核查方法来分析具有利益的财务和安全性质。