资金费率
资金费率热力图
多空比
大户多空比
币安/欧易/火币大户多空比
Bitfinex杠杆多空比
账号安全
资讯收藏
自选币种
以太坊联合创始人：形式化验证将成抵御AI攻击的关键防线
以太坊联合创始人维塔利克·布特林近日指出，数学验证的软件正成为保护以太坊乃至整个加密货币行业免受人工智能辅助网络攻击与软件漏洞威胁的重要工具。
在最新发表的博客文章中，布特林主张AI辅助的“形式化验证”技术能够帮助保护区块链网络、智能合约及加密系统，防范可能导致用户承受不可逆财务损失的软件缺陷。他写道：“如果方法得当，这种技术既能输出极高效率的代码，又能实现比传统编程方式更可靠的安全性。”他特别提到开发者平井洋一将其称为“软件开发的终极形态”。
形式化验证是通过数学方法检验软件行为正确性的技术，其渊源可追溯至二十世纪五六十年代的基础研究。布特林认为，近期人工智能的进展正在使这项技术更适用于软件工程与安全研究领域。他指出：“如果实现端到端的形式化验证，你不仅能在理论上证明协议设计的安全性，还能在实践中验证用户实际运行的特定代码段的安全性。从用户视角看，这极大提升了无需信任的安全性：要完全信任代码，你无需逐行检查全部代码，只需核验已被证明的声明即可。”
这番论述发表之际，恰逢研究机构与政府部门警告先进AI模型正在快速提升发现和利用软件漏洞的能力。此前某公司曾限制其网络安全专用模型的访问权限，因为测试显示该系统能自主识别并利用软件缺陷，其能力远超以往公开的AI模型。
代码漏洞的灾难性影响
“计算机代码中的漏洞令人心惊。”布特林在文章中强调。未发现的漏洞对加密项目可能造成毁灭性打击，攻击者往往能利用软件缺陷永久窃取用户资金且几乎无法追回。例如今年四月，某组织通过污染内部服务接口，从某基础设施项目窃取了价值2.92亿美元的代币。据估算，国家背景的黑客迄今已窃取价值超60亿美元的加密货币。
验证技术的双重价值
布特林表示，形式化验证还能通过证明优化后的底层代码与可读性更高的参考实现相一致，从而增强人们对AI生成软件的信任度。“其核心价值在于验证过程真正实现了端到端的覆盖，”他写道，“最棘手的漏洞往往是那些存在于两个独立子系统边界处的交互性问题。”
技术局限与未来展望
尽管认可AI在保护加密网络代码方面的潜力，布特林也提醒形式化验证无法完全消除安全风险。“形式化验证并非万能灵药，但它特别适用于目标远比实现方式简单的场景，”他分析道，“这在以太坊下一阶段迭代中需要部署的某些高难度技术中尤为明显：抗量子签名、STARK证明系统、共识算法以及ZK-EVM等。”
对于日益先进的网络攻击是否终将使开源软件或去中心化系统无法保障安全的观点，布特林持反对态度：“这将是网络安全的黯淡未来，尤其对关注互联网去中心化与自由的人们而言更是如此。密码朋克的核心理念本就建立在‘互联网中防御方具有优势’这一基础上。”
他提出，未来系统很可能依赖通过形式化验证和受限安全环境保护的高度安全“核心”基础设施。“对于安全核心部分，我们不会让存在缺陷的代码肆意扩散，”布特林总结道，“我们将积极行动保持安全核心的小型化，并推动其进一步精简。”
