「钢琴测试」思想实验：你敢坐在形式化验证过的代码下吗

moyix · x · 2026-10-28

安全研究者 moyix 转发 samth 引用 John Regehr（Embedded in Academia）2011 年经典博文「The Piano Test for Program Verification」。

思想实验：假设验证者证明某版 OpenSSH 内存安全，并在天花板悬挂一架钢琴，绳索连接 SIGSEGV 处理器——若 fuzzing 工具成功让程序崩溃，刀会切断绳索砸向你。你敢坐在钢琴下吗？Regehr 认为没几个验证研究者敢坐：问题核心在于「verified」一词被验证社区用得极松，语义与实际保障之间差距巨大。这篇老文被重新翻出，回应「形式化验证能否完全取代 fuzzing」的提问。