Vitalik Buterin 否认人工智能黑客攻击带来的网络安全厄运

以太坊联合创始人维塔利克·布特林 (Vitalik Buterin) 并不认为，改进人工智能最终会让网络安全变得无法取胜。

Buterin 相信，相反的情况最终可能会发生：人工智能可能会为防御者提供构建软件所需的工具，而这些软件一开始就很难被利用。

“人们越来越普遍地认为，人工智能黑客攻击意味着网络安全注定要失败。我不同意，”周三，Buterin 在 X 社交媒体网络上发表了一篇冗长且典型的实质性社交媒体帖子中写道。

这位以太坊联合创始人表示，一旦开发人员开始充分利用形式验证，网络安全自然应该有利于防御者。

Buterin 还将这一信念直接与他自己对加密货币的接触联系起来，并透露他大约 90% 的净资产仍然是加密货币。

他认为，任何继续持有大量加密货币的人都在暗中押注，尽管攻击者的攻击手段日益复杂，但仍然可以构建足够安全的数字系统。

“如果人工智能可以证明纳维-斯托克斯和 FLT，那么人工智能就可以证明‘这个程序是安全的’这一数学定理，”Buterin 写道，指的是纳维-斯托克斯问题和费马大定理。

他的论点基于形式验证，这是一种数学证明软件满足特定属性的方法。

Buterin 在他五月份的文章中广泛探讨了同样的想法，他在文中将人工智能辅助形式验证描述为安全关键软件的巨大变革工具。然而，证明此类软件的安全性可能具有挑战性。

定义问题

Buterin 使用加密消息应用程序 Signal 作为示例来说明为什么这可能很困难。

攻击者可能会尝试伪造消息、阻止消息到达、重放旧消息、危害服务器、操纵用于发现其他用户公钥的进程或利用操作系统中的漏洞。

其他问题可能是由损坏的数据库、恶意库、编译器甚至硬件级信息泄漏引起的。

即使对话内容保持加密状态，攻击者仍然可能知道谁在通信。因此，“安全”实际含义的数学定义本身可能变得极其复杂。

“所以……即使是定义也可能超过一千行代码，需要深入仔细的思考才能弄清楚，”Buterin 写道。

进攻者和防守者

毫无疑问，功能更强大的人工智能系统可以让发现漏洞变得更加容易。

然而，机器推理的同样改进也可以大大降低正式证明软件按照精心构建的安全规范运行的成本。

双方都会有人工智能。