【作者】 王钊；

【导师】 黄鑫； 赵梁斌；

【作者基本信息】 太原理工大学 ， 软件工程（专业学位）， 2024， 硕士

【摘要】 区块链技术作为一种革命性的数字和信息处理技术,在全球范围内得到了迅速的发展和广泛的应用。特别是在数据存储、交易处理、供应链管理等方面,区块链技术凭借其去中心化、不可篡改、透明性高等特点,为数据交换和信息安全提供了新的解决方案。随着区块链应用场景的不断扩展,如何保证链上与链下数据之间的有效、安全交互,构建一种安全有效的区块链数据馈送机制成为了一个重要的研究议题。区块链预言机技术应运而生,作为连接区块链与外部世界数据的桥梁,使得区块链能够访问和处理外部数据源的信息。预言机在金融、保险、物流等多个区块链应用领域发挥着至关重要的作用,它不仅能够提高区块链应用的灵活性和实用性,同时也扩展了区块链技术的应用范围。然而,随着预言机应用的增多和类型的多样化,如何确保预言机提供的数据可认证性、完整性和安全性,成为了区块链技术发展中的一个关键挑战。尽管形式化证明方法提供了一种精确定义和验证复杂协议所需安全保障的理论工具,但在区块链预言机系统的安全性证明中,由于系统的动态性、多样性及环境的不断变化,使得形式化模型的建立和验证过程面临极大挑战。当前形式化方法主要针对静态或较为简单的系统设计,难以适应预言机系统高度动态和不确定的环境要求。此外,考虑到区块链预言机系统中的跨链通信和数据验证,现有的形式化工具和语言可能需要进一步的扩展和改进。针对上述背景和挑战,本文提出了一套区块链预言机的模块化安全分析框架和形式化证明方法。本研究首先利用线索演算与协议可组合语法语义系统,创新性地提出了基于协议可组合方式的区块链预言机形式化建模架构,有效应对预言机系统的复杂性和动态性。通过对广泛使用的Town Crier系统进行深入分析,本文不仅揭示了其安全通信架构的关键特点,将通信阶段分为多个模块,还对每个模块进行了详尽的安全性形式化证明,验证了系统设计的机密性、完整性等安全性质。特别地,本文通过顺序组合的方式证明了Town Crier系统的数据完整性和可认证性,展示了通过将多个模块的安全性质组合起来加强系统安全性的可行性。此外,本研究还探讨了针对PCL逻辑证明过程的自动化验证方法,进一步提升了证明过程的效率和可信度。综上所述,本文的工作不仅为区块链预言机系统的安全性提供了新的建模思路支持和证明途径,也为未来区块链技术的安全性研究和应用开发探索了一种可能性。更多还原

【Abstract】 Blockchain technology,as a revolutionary digital and information processing technology,has witnessed rapid development and extensive application globally.Particularly in data stor-age,transaction processing,and supply chain management,blockchain technology,with its de-centralization,immutability,and high transparency,has offered new solutions for data exchange and information security.As the application scenarios of blockchain continue to expand,en-suring effective and secure interaction between on-chain and off-chain data and constructing a reliable blockchain data feed mechanism has emerged as a significant research topic.The advent of blockchain Oracle technology serves as a pivotal bridge connecting block-chain with external world data,enabling blockchain to access and process information from external data sources.Oracles play a crucial role in various blockchain application domains such as finance,insurance,and logistics,enhancing the flexibility and practicality of blockchain applications and broadening the scope of blockchain technology.However,with the increasing use and diversity of Oracle applications,ensuring the authenticity,integrity,and security of data provided by Oracles poses a key challenge in the development of blockchain technology.Although formal proof methods offer theoretical tools for precisely defining and verifying the security guarantees required by complex protocols,the dynamic nature,diversity,and ever-changing environment of blockchain Oracle systems pose significant challenges in establishing and validating formal models.Current formal methods,mainly tailored for static or simpler system designs,struggle to meet the high dynamism and uncertain environmental requirements of Oracle systems.Moreover,considering cross-chain communication and data verification in blockchain Oracle systems,existing formal tools and languages may require further extension and improvement.In light of the aforementioned background and challenges,this paper proposes a modular security analysis framework and formal proof method for blockchain Oracles.This research innovatively employs thread calculus and the syntax and semantics of protocol composition to propose a formal modeling architecture for blockchain Oracles based on protocol composition,effectively addressing the complexity and dynamism of Oracle systems.Through an in-depth analysis of the widely-used Town Crier system,this paper not only reveals the key features of its secure communication architecture by dividing the communication phase into multiple modules but also provides a detailed formal proof of the security properties,such as confidentiality and integrity,of each module.Specifically,this paper demonstrates the feasibility of enhancing system security by sequentially combining the security properties of multiple modules,proving the data integrity and authenticity of the Town Crier system.Additionally,this research explores automated verification methods for PCL logic-proof processes,further enhancing the efficiency and credibility of the proof process.In summary,this work not only supports the security of blockchain Oracle systems with new modeling ideas and proof methods but also explores the possibility of future security re-search and application development in blockchain technology.更多还原