论文标题
分散融资中贷款池的正式分析
Formal Analysis of Lending Pools in Decentralized Finance
论文作者
论文摘要
分散的金融（DEFI）应用程序构成了部署在区块链上的整个金融生态系统。此类应用是基于很难确定财务安全的复杂协议和激励机制。此外，它们的采用速度正在迅速增长，因此损害了越来越高的资产。因此，准确的形式化和对DEFI应用的验证对于评估其安全性至关重要。我们已经开发了一种工具，用于对最广泛的Defi应用程序之一的形式分析：贷款池（LP）。这是通过利用LPS，MAUDE验证环境和Multivesta统计分析仪的现有正式模型来实现的。该工具支持多个分析，包括可及性分析，LTL模型检查和统计模型检查。在本文中，我们展示了该工具如何用于分析LP的几个参数，这些参数是为了评估和预测其行为的基础。特别是，我们使用统计分析来搜索阈值和奖励参数，以最大程度地减少无法恢复贷款的风险。
Decentralised Finance (DeFi) applications constitute an entire financial ecosystem deployed on blockchains. Such applications are based on complex protocols and incentive mechanisms whose financial safety is hard to determine. Besides, their adoption is rapidly growing, hence imperilling an increasingly higher amount of assets. Therefore, accurate formalisation and verification of DeFi applications is essential to assess their safety. We have developed a tool for the formal analysis of one of the most widespread DeFi applications: Lending Pools (LP). This was achieved by leveraging an existing formal model for LPs, the Maude verification environment and the MultiVeStA statistical analyser. The tool supports several analyses including reachability analysis, LTL model checking and statistical model checking. In this paper we show how the tool can be used to analyse several parameters of LPs that are fundamental to assess and predict their behaviour. In particular, we use statistical analysis to search for threshold and reward parameters that minimize the risk of unrecoverable loans.
