学术研究：我们智能合约安全研究的发现

在 Veridise，我们将尖端的学术研究与最新的行业经验相结合。

除了我们在审计关键区块链基础设施协议、智能合约和零知识实现方面的丰富经验外，我们团队中的许多成员还有学术研究背景。

在这篇博客文章中，我们希望介绍我们团队成员进行的关于 智能合约 安全性 的学术研究，以及这与我们在 Veridise 所做工作的关系。我们还进行了广泛的 零知识安全 研究，这将在下一篇（第二部分）博客文章中介绍。

我们选择了五篇论文，涵盖以下内容：

• SmartPulse: Automated Checking of Temporal Properties in Smart Contracts
• Synthesis-Powered Optimization of Smart Contracts via Data Type Refactoring
• SolType: Refinement Types for Arithmetic Overflow in Solidity
• Demystifying Loops in Smart Contracts
• Formal Verification of Workflow Policies for Smart Contracts in Azure Blockchain

下面，我们概述了每篇论文，以及当前 Veridise 团队中的作者 —— 点击每个名字以了解更多关于我们的团队成员的信息！

Veridise 学术研究系列: 📚 第一部分：来自我们智能合约安全研究的发现 📚 第二部分：来自我们零知识安全研究的发现（待发布）

SmartPulse: Automated Checking of Temporal Properties in Smart Contracts

Veridise 作者: Jon Stephens, Kostas Ferles, Benjamin Mariano, Işil Dillig.

SmartPulse 论文可以视为启动 Veridise 的基础工作。其检查智能合约活跃性属性的新颖方法引起了区块链安全专家的极大兴趣，促使早期团队建立了 Veridise。

该论文解决了验证智能合约活跃性属性的挑战。检查活跃性属性意味着确保“某件好事”最终会发生（例如，“我最终会收到退款”），而不仅仅是验证安全属性（“X 永远不会发生”）。为了应对这一挑战，作者介绍了 SmartPulse，这是一种可以自动验证智能合约中的安全性和活跃性属性的工具。

SmartPulse 引入了一种新的规范语言 SmartLTL，专门用于表达针对区块链状态的智能合约的时间属性。它还允许自定义攻击模型，支持在各种威胁场景下的全面测试。该工具完全自动化，并能针对易受攻击的合约生成具体的攻击场景。SmartPulse 在总共 1947 个智能合约上进行评估，表明活跃性检查可以按规模进行，并生成与现实攻击相对应的反例。

有趣的是，SmartLTL 规范语言是我们当前用于内部工具（如 OrCa）的 [V] 规范语言 的灵感来源。

Synthesis-Powered Optimization of Smart Contracts via Data Type Refactoring

Veridise 作者: Işil Dillig

本论文解决了通过自动重构数据布局来优化以太坊智能合约的Gas使用问题。这很重要，因为在以太坊上执行智能合约会消耗Gas，而Gas与现实世界货币相关。减少Gas使用使合约更具成本效益。

虽然此前有关于减少Gas使用的工作，但它们主要集中在低级优化上。这是第一篇通过改变数据表示来减少Gas使用的论文，结果显示节省显著。

本研究提出的解决方案引入了一种领域特定语言（DSL），用于指定类型级转换，并使用程序合成自动生成具有优化数据布局的功能等效合约。该方法利用了一种新颖的合成技术，能够在给定转换下找到最有效的Gas代码。工具 Solidare 在现实世界合约中显著减少了Gas消耗。

SolType: Refinement Types for Arithmetic Overflow in Solidity

Veridise 作者: Bryan Tan, Benjamin Mariano, Işil Dillig

本论文旨在防止 Solidity 智能合约中的算术溢出和下溢。该论文引入了 SolType，一个精炼类型系统，使开发者能够注释合约以证明算术操作的安全性。

该系统能够表达整型值之间的复杂关系和数据结构的聚合性质。在名为 Solid 的原型中实现，SolType 包括一个类型推断引擎，能够自动推断有用的类型注释和合约不变式。

在 120 个智能合约上的评估显示，Solid 能够自动消除 86.3% 的冗余 SafeMath 调用，在准确性和效率上优于领先的 Solidity 验证器 Verismart。

Demystifying Loops in Smart Contracts

作者: Benjamin Mariano, Isil Dillig

该论文解决了分析 Solidity 智能合约中循环的挑战，循环的出现频率比以前想象的要高，大约每五个合约中就有一个。作者研究了在以太坊区块链上部署的超过 20,000 个 Solidity 合约。

传统分析工具通常忽视这些循环的复杂性，导致潜在的安全和功能问题。为了解决这一问题，作者引入了一种名为 Consul 的领域特定语言（DSL），旨在总结 Solidity 中常见的循环模式。他们还开发了一个名为 Solis 的程序合成工具链，可以使用 Consul 自动生成循环摘要。

评估显示，Solis 能够总结 56% 分析的循环，其中 81% 的摘要与原始循环完全等价。该研究识别了 Solidity 循环中的关键语义模式，强调了在智能合约验证中需要定制分析工具的重要性。

在 Veridise，我们从 Solis 评估中获得的经验教训指导了我们对 Solidity 智能合约验证和漏洞发现的各种定制分析工具的开发。

Formal Verification of Workflow Policies for Smart Contracts in Azure Blockchain

Veridise 作者: Isil Dillig, Kostas Ferles

这篇论文是最早提出智能合约完全自动形式验证的论文之一，旨在确保 Microsoft 的 Azure Blockchain Workbench 中智能合约的正确性。

给定一个智能合约和一个被定义为有限状态机的属性，所提出的技术可以自动确定智能合约是否满足或违反该属性。

所提议的方法已在一个名为 VeriSol 的工具中实现，并应用于 Azure Blockchain Workbench 中的所有应用合约，发现了以前未知的错误。在修复这些错误后，VeriSol 成功进行了所有合约的全面验证。

该论文在塑造我们内部漏洞检测工具方面发挥了重要作用，强调了定义关键协议属性和验证（无论是手动还是自动）协议是否符合该属性的重要性 —— 这两者对于进行全面、高质量的安全审计至关重要。

结论

总之，这五篇关于智能合约安全的研究论文导致了以下工具、发现，并为我们内部漏洞检测软件的发展作出了贡献，例如：

• SmartPulse，用于检查智能合约的活跃性属性。SmartPulse 验证了 1947 个智能合约并发现了几处漏洞。之后，该工作为我们当前在内部工具（如 OrCa）中使用的 [V] 规范语言 提供了灵感。
• Solidare，优化了现实世界合约并有效减少了Gas使用。
• SolType，在 120 个合约中消除了 86.3% 的冗余 SafeMath 调用。
• Solis，研究了超过 20,000 个 Solidity 智能合约中的循环，并能够使用作者新引入的 DSL 总结 56% 的循环，其中 81% 的摘要与原始循环完全等价。
• VeriSol，发现并修复了 Azure Blockchain Workbench 合约中的错误，随后通过强调定义和验证关键协议属性的关键作用，塑造了我们内部的漏洞检测工具。

我们致力于将学术研究与行业实践相结合，以增强 智能合约安全性 和 零知识安全性。更多研究正在进行中，我们期待着尽快分享。

在我们下一篇博客文章中，我们将介绍我们关于零知识安全的学术研究。

Veridise 学术研究系列: 📚 第一部分：来自我们智能合约安全研究的发现 📚 第二部分：来自我们零知识安全研究的发现（待发布）

作者： Mikko Ikola，Veridise 市场部主管

感谢 Isil Dillig、Bryan Tan、Jon Stephens 审阅该博客文章。

想要了解更多关于 Veridise 的信息？

Twitter | Lens | LinkedIn | Github | 请求审核

• 原文链接： medium.com/veridise/acad...
• 登链社区 AI 助手，为大家转译优秀英文文章，如有翻译不通的地方，还请包涵～