如何捕捉形式验证工具中的漏报漏洞

Looking for Missed Alarm Bugs in a Formal Verification Tool

形式验证并非魔法，而是充满挑战的工程工作。我们团队在测试 Alive2 时发现，漏报（missed alarm）比误报更难捕捉。为此，我们尝试了两种方法：一是修改 YARPGen 生成行为不同的函数对，二是利用 Minotaur 在优化过程中产生的大量候选方案进行压力测试。目前看来，Alive2 和 Z3 似乎很少漏报，但这并不意味着完美。我们怀疑在函数属性等特定场景下，仍可能存在未被发现的漏洞。