关于CBDC的操作韧性：形式验证在离线支付中的威胁与前景
On the Operational Resilience of CBDC: Threats and Prospects of Formal Validation for Offline Payments
AI总结：
本文探讨CBDC离线支付系统的形式验证方法，通过构建威胁模型和形式化方法，提出提升操作韧性的策略。
摘要：
信息和通信技术如今已广泛应用于人类活动，包括经济和金融领域。现代计算机在信息处理、存储、检索和传输方面已达到极高水平。然而，理论计算机科学的一些结果表明，一般情况下无法认证软件质量。除了安全关键系统外，这主要涉及由受限系统处理的信息，社会经济影响有限。在新兴的互联网技术时代，如中央银行数字货币（CBDC）等交换代币资产和数字货币的技术，即使是微小的bug也可能引发金融崩溃。尽管上述不可能结果在绝对意义上无法克服，但存在形式化方法可以在适当条件下为软件系统模型提供正确性断言。我们倡导利用这些方法来验证CBDC软件基础设施的操作韧性，通过构建离线支付问题、组织其威胁景观，并概述形式化方法方法，通过最小的证明概念示例，我们认为这些方法应成为CBDC设计和部署的基础。
英文摘要：
Information and communication technologies are by now employed in most human activities, including economics and finance. Modern computers have reached an extraordinary power in terms of information processing, storage, retrieval, and transmission. However, several results of theoretical computer science imply the impossibility of certifying software quality in general. With the exception of safety-critical systems, this has primarily concerned information processed by confined systems, with limited socio-economic consequences. In the emerging era of technologies for exchanging tokenized assets and digital money over the Internet, such as in particular central bank digital currency (CBDC), even a minor bug could trigger a financial collapse. Although the aforementioned impossibility results cannot be overcome in an absolute sense, there exist formal methods that can provide correctness assertions for software system models under suitable conditions. We advocate their use to validate the operational resilience of software infrastructures for CBDC by framing the offline payment problem, organizing its threat landscape, and outlining a formal methods methodology, illustrated by a minimal proof of concept, that we argue should underpin CBDC design and deployment.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
