Vitalik Buterin 认为人工智能可以增强软件安全性以抵御黑客攻击

这位以太坊联合创始人将人工智能辅助的形式验证视为软件开发的“最终形式”，他将 90% 的财富押在它将保护的生态系统上。

Vitalik Buterin 阐述了为什么人工智能实际上可能成为软件世界有史以来最强大的防止黑客攻击的工具，尽管其容易产生幻觉和产生错误代码的倾向已得到充分证明。问题是：人工智能不能单独做到这一点。它需要一个称为形式验证的数学保姆。

在 5 月 18 日发布的博客文章中，Buterin 探讨了如何将人工智能的原始代码生成速度与形式验证的数学严谨性相结合，从而显着提高软件系统的安全性，特别是支撑以太坊基础设施的软件系统的安全性。他还漫不经心地透露，他大约 90% 的净资产都持有 ETH，这让他对保护生态系统的兴趣不再那么学术化，而是更加个人化。

Gloria Stocks 在一个应用程序中，加密货币在另一个应用程序中，钱包无处不在？凯莱金融将您的整个投资组合一目了然。一起看看→

AI 准确性问题及其解决方案

Buterin 的核心论点看似简单。人工智能可以快速生成大量代码，但这种速度伴随着可靠性税。输出往往不如细心的人类开发人员产生的准确。在管理数十亿美元的智能合约中，这是一个生存威胁。

形式验证使用数学证明来证明代码在所有可能的场景中都能正确运行，而不是依赖于测试，后者仅针对特定场景检查程序的行为。

Buterin 特别指出精益定理证明器是该领域的关键工具。精益允许开发人员编写可以机械检查的证明，从而创建传统代码审查根本无法比拟的数学确定性层。

他承认一个普遍的反对意见，即攻击者也可能使用人工智能来更快地发现错误。他的回应是，这种担忧是“暂时的”。经过验证的证据一经确认，就是永久性的。攻击者发现错误是一次性事件。

为什么以太坊比大多数人更关心

后量子密码学是 Buterin 强调的领域之一。随着量子计算机越来越接近能够破解当前的加密方案，以太坊和所有其他区块链将需要抗量子签名，而形式验证提供了一条单独测试无法提供的信心之路。

在您的一天开始之前，新闻会影响资金、市场和世界。日常的。自由的。加入加密货币、金融和政策领域 34,000 多名读者的行列。电子邮件地址 免费订阅 我们尊重您的隐私。随时取消订阅。

零知识证明是另一个。 ZK 技术是以太坊通过 ZK-EVM 和 rollups 进行扩展策略的核心。这些是极其复杂的加密结构，其中一个细微的错误可能会损害整个第 2 层网络的完整性。

Buterin 引用了两个具体的正在进行的项目作为这项工作在实践中的例子。 Arklib 是 STARK 的正式验证实现，STARK 是零知识证明系统的两个主要系列之一。第二个是 evm-asm，是一个 EVM 抽象，旨在使以太坊的虚拟机更适合形式分析。

他更有趣的观察之一是关于信任模型。形式验证不仅仅使代码更安全。它改变了用户需要信任的内容。用户无需逐行审核整个代码库，而是可以验证有关代码功能的高级断言。

Buterin 并没有忽视风险

Buterin 指出了两个重要的限制。首先是规范风险。形式验证证明代码符合其规范，但如果规范本身是错误的，那么证明就毫无价值。

第二是硬件。软件可以被正式验证。运行该软件的物理芯片不能，至少不能达到同样严格的水平。受损的处理器甚至可能破坏经过完美验证的代码。

尽管有这些警告，Buterin 仍将人工智能辅助形式验证描述为软件开发的潜在“最终形式”。形式验证的根源可以追溯到 20 世纪 50 年代和 20 世纪 60 年代，但实际应用仍然有限，主要局限于航空航天、国防和少数其他安全关键行业，在这些行业中，数学证明的成本由失败的成本证明是合理的。

现在正在改变的是经济。人工智能极大地减少了编写代码和证明所需的人力，有可能使形式验证适用于更广泛的软件。