资金费率
资金费率热力图
多空比
大户多空比
币安/欧易/火币大户多空比
Bitfinex杠杆多空比
账号安全
资讯收藏
自选币种
以太坊联合创始人勾勒网络安全未来愿景
以太坊联合创始人维塔利克·布特林近日为区块链及其他领域的网络安全描绘了乐观前景。他指出，在人工智能驱动攻击日益强大的时代，将人工智能与形式化验证技术结合，或将决定性扭转攻防天平，使防御方占据优势。
在5月18日发布的博客文章中，布特林阐释了开发者如何编写代码——甚至可以是EVM字节码或汇编等低级格式代码，进而使用Lean等验证语言通过机器可验证的数学证明来确保证明的正确性。人工智能工具通过同步生成高度优化的代码及相应证明，可显著加速这一过程。在他看来，人类未来只需专注于确保高级规范能真实反映其预期目标。
形式化验证的重要性日益凸显
形式化验证并非全新概念，其起源可追溯至数十年前。该方法将程序特性表述为数学定理，并借助Lean等工具自动验证定理证明。布特林通过斐波那契奇偶性等基础示例阐述概念后，进一步深入探讨了实际场景中的复杂应用。
他认为关键突破在于人工智能能大规模处理繁琐且反直觉的细节证明工作。这种方法尤其适用于密码学与共识系统领域——这些系统的安全需求相对明确，而具体实现却异常复杂。
文中重点提及与以太坊相关的关键领域包括：抗量子签名、STARK证明系统与ZK-EVM、共识算法以及EVM实现方案等。当前已有Arklib等项目正在推进可验证STARK实现，基于Lean的形式化验证工作也在以太坊更广泛的组件中展开。布特林引用开发者对"软件开发终极形态"的论述，指出这种范式能产出高效且可证明正确的代码。
应对AI漏洞挖掘威胁
针对网络安全界日益增长的悲观情绪，布特林在文中作出直接回应。随着AI工具发现零日漏洞的能力不断提升，有人担忧智能合约等不可信系统将难以维系——此类系统中的漏洞可能导致无法挽回的经济损失。
他强调人工智能同样能为防御方提供强大助力。结合形式化方法，AI可对关键的"安全核心"组件进行穷尽式验证，而敏感性较低的"边缘"功能则可在权限受限的沙箱环境中运行。这种分层架构有望构建出有利于防御方的平衡态势。类似理念已开始影响加密钱包的开发实践，通过AI增强自动化能力与安全防护水平。
布特林还引用了相关机构在强化代码防御AI辅助攻击方面的成果，认可"防御方终将获得决定性胜利"的积极判断。
客观认识技术局限
秉持一贯的分析风格，布特林坦诚指出了形式化验证的局限性：它不能保证现实世界的绝对安全。潜在风险包括规范不完整、验证工具或底层硬件存在缺陷，以及已验证核心系统与未验证外围系统间的衔接间隙。
他特别说明："可证明的正确性并不意味着软件符合人类对正确性的普遍理解。"技术目标应是建立冗余机制，最大限度缩小意图与行为间的差距，而非追求绝对完美。
行业反响与未来展望
这一愿景与以太坊路线图中提升安全性与效率的持续努力相契合。布特林近年来也持续关注人工智能带来的社会风险与治理挑战，尤其支持开展长期AI安全与政策研究的机构。
当前业界讨论多聚焦于以太坊安全层面的直接影响，而本文试图从Lean证明实例到AI时代密码朋克精神的深层内涵，全面捕捉布特林提出的哲学思辨与技术精妙之处。
布特林与合作者正持续推动这些技术在以太坊前沿研究中的应用。若取得成功，AI辅助的形式化验证不仅将保障智能合约安全，更可能重塑整个行业构建关键软件的方式，使"去信任化"超越营销术语，成为坚实的技术基石。
