去中心化金融中借贷池的形式化分析
软件工程
2022-09-19 v2
摘要
去中心化金融（DeFi）应用构成了一个部署在区块链上的完整金融生态系统。此类应用基于复杂的协议与激励机制，其金融安全性难以判定。此外，它们的采用正在快速增长，从而危及越来越大量的资产。因此，对 DeFi 应用进行准确的形式化与验证对于评估其安全性至关重要。我们开发了一款用于形式化分析最广泛使用的 DeFi 应用之一——借贷池（LP）的工具。这是通过利用现有的 LP 形式化模型、Maude 验证环境以及 MultiVeStA 统计分析仪实现的。该工具支持多种分析，包括可达性分析、LTL 模型检测与统计模型检测。在本文中，我们展示了如何使用该工具分析 LP 的若干参数，这些参数对于评估和预测其行为至关重要。特别地，我们使用统计分析来搜索使不可收回贷款风险最小化的阈值与奖励参数。
引用
@article{arxiv.2206.01333,
title = {Formal Analysis of Lending Pools in Decentralized Finance},
author = {Massimo Bartoletti and James Chiang and Tommi Junttila and Alberto Lluch Lafuente and Massimiliano Mirelli and Andrea Vandin},
journal= {arXiv preprint arXiv:2206.01333},
year = {2022}
}