安全专家：形式验证不会终结漏洞研究，AI 转战未验证路径

安全研究员 Julianor 发起线程审视形式验证程度最高的内核 seL4,指出即便完全形式化验证也仍需修洞。他认为形式验证不会终结漏洞研究，而是把猎虫战场转移到假设条件、硬件与运行时模型以及未被验证的路径上，而 AI 已经在未验证路径上找到 bug。背景是 AI 发现漏洞的速度已超过人类修补速度，业界「全面形式化验证」的呼声越来越高。

2026-11-12 ~ 2026-11-13 · 2 条相关