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.
翻译:分散化金融(DeFi)应用程序构成整个金融生态系统,在供应链上部署。这些应用程序基于复杂的协议和激励机制,其金融安全难以确定。此外,它们的采用正在迅速增长,从而危及越来越多的资产。因此,准确正规化和核查 DeFi 应用程序对于评估其安全至关重要。我们已经开发了一个工具,用于正式分析最广泛的 DeFi 应用程序之一:贷款池(LP),这是利用现有的LP、Maude核查环境和多VeStA统计分析器的正式模型实现的。该工具支持了若干分析,包括可及性分析、LTL模型检查和统计模型检查。在本文中,我们展示了该工具如何用来分析对评估和预测其行为至关重要的LP的若干参数。特别是,我们利用统计分析来寻找尽量减少无法收回贷款风险的门槛和奖励参数。