一句话：提出 Achar，用主动学习提出候选不变式，并以模糊测试反证之，从而为含不可解释操作的开放程序合成归纳不变式。
现实程序常包含验证引擎无法理解语义的操作，如第三方库调用、内联汇编、SIMD 指令、编译器原语乃至不可解释的机器学习模型查询。针对这类“开放”程序，归纳不变式的合成长期依赖人工编写桩函数，既困难又容易出错。本文提出“几乎正确的不变式”这一自动化策略：采用主动学习，由数据驱动的学习器提出候选不变式，但与传统“验证不变式”的思路不同，作者转而尝试证伪候选不变式，将证伪问题归约为非确定性程序上的一组可达性检查，并借助现代模糊测试器高效求解这些查询。工具 Achar 能自动合成足以证明目标程序正确性的归纳不变式。实验表明，即使几乎不接触程序源码，Achar 也优于能完整访问源码的最先进不变式生成工具；对于调用外部库、内联汇编以及查询卷积神经网络等现有引擎无法处理的程序，Achar 也能在合理时间内成功推断所需不变式。
Real-life programs contain multiple operations whose semantics are unavailable to verification engines, like third-party library calls, inline assembly and SIMD instructions, special compiler-provided primitives, and queries to uninterpretable machine learning models. Even with the exceptional success story of program verification, synthesis of inductive invariants for such "open" programs has remained a challenge. Currently, this problem is handled by manually "closing" the program---by providing hand-written stubs that attempt to capture the behavior of the unmodelled operations; writing stubs is not only difficult and tedious, but the stubs are often incorrect---raising serious questions on the whole endeavor. In this work, we propose Almost Correct Invariants as an automated strategy for synthesizing inductive invariants for such "open" programs. We adopt an active learning strategy where a data-driven learner proposes candidate invariants. In deviation from prior work that attempt to verify invariants, we attempt to falsify the invariants: we reduce the falsification problem to a set of reachability checks on non-deterministic programs; we ride on the success of modern fuzzers to answer these reachability queries. Our tool, Achar, automatically synthesizes inductive invariants that are sufficient to prove the correctness of the target programs. We compare Achar with a state-of-the-art invariant synthesis tool that employs theorem proving on formulae built over the program source. Though Achar is without strong soundness guarantees, our experiments show that even when we provide almost no access to the program source, Achar outperforms the state-of-the-art invariant generator that has complete access to the source. We also evaluate Achar on programs that current invariant synthesis engines cannot handle---programs that invoke external library calls, inline assembly, and queries to convolution neural networks; Achar successfully infers the necessary inductive invariants within a reasonable time.
DOI 原文 ·
@inproceedings{paperbot7434,
title = {Almost correct invariants: synthesizing inductive invariants by fuzzing proofs},
author = {Sumit Lahiri and Subhajit Roy},
booktitle = {ISSTA},
year = {2022},
doi = {10.1145/3533767.3534381}
}