Almost correct invariants: synthesizing inductive invariants by fuzzing proofs
Almost correct invariants: synthesizing inductive invariants by fuzzing proofs
复制标题
几乎正确的不变量：通过模糊证明合成归纳不变量
DOI：
--
复制
发表时间：
2022
期刊：
影响因子：
--
通讯作者：
Subhajit Roy
中科院分区：
文献类型：
--
作者：
S. Lahiri;Subhajit Roy
现实生活中的程序包含多个操作，其语义对验证引擎不可用，如第三方库调用，内联汇编和SIMD指令，特殊的编译器提供的原语，以及对不可解释的机器学习模型的查询。即使有了程序验证的特殊成功故事，这种“开放”程序的归纳不变量的合成仍然是一个挑战。目前，这个问题是通过手动“关闭”程序来处理的--通过提供手写的存根来尝试捕获未建模操作的行为;写存根不仅困难和乏味，而且存根经常是不正确的--在整个奋进中提出了严重的问题。在这项工作中，我们提出了几乎正确的不变量作为一个自动化的策略，为这样的“开放”程序合成归纳不变量。我们采用主动学习策略，其中数据驱动的学习者提出候选不变量。在偏离以前的工作，试图验证不变量，我们试图伪造的不变量：我们减少伪造的问题，一组可达性检查的非确定性程序，我们骑在现代模糊的成功，回答这些可达性查询。我们的工具，Achar，自动合成归纳不变量，足以证明目标程序的正确性。我们比较Achar与一个国家的最先进的不变的合成工具，采用定理证明公式建立在程序源。虽然Achar是没有很强的健全性保证，我们的实验表明，即使我们提供几乎没有访问程序源，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：
10.1007/978-3-030-53291-8_9
发表时间：
2020-06-16
期刊：
Computer Aided Verification
影响因子：
--
作者：
Si X;Naik A;Dai H;Naik M;Song L
通讯作者：
Song L
DOI：
10.1109/sp40001.2021.00060
发表时间：
2021-01
期刊：
2021 IEEE Symposium on Security and Privacy (SP)
影响因子：
--
作者：
Subhajit Roy;Justin Hsu;Aws Albarghouthi
通讯作者：
Subhajit Roy;Justin Hsu;Aws Albarghouthi
表示不变量的数据驱动推理
DOI：
10.1145/3385412.3385967
发表时间：
2020
期刊：
ACM SIGPLAN Conference on Programming Language Design and Implementation
影响因子：
--
作者：
Miltner, Anders;Padhi, Saswat;Millstein, Todd;Walker, David
通讯作者：
Walker, David
学习以测试生成器为模的状态前提条件
DOI：
10.1145/3314221.3314641
发表时间：
2019
期刊：
PLDI 2019: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation
影响因子：
--
作者：
Astorga, Angello;Madhusudan, P.;Saha, Shambwaditya;Wang, Shiyu;Xie, Tao
通讯作者：
Xie, Tao