Verification Modulo Versions: Towards Usable Verification
Verification Modulo Versions: Towards Usable Verification
复制标题
DOI：
10.1145/2666356.2594326
复制
发表时间：
2014-06-01
影响因子：
--
通讯作者：
Blackshear, Sam
中科院分区：
文献类型：
--
作者：
Logozzo, Francesco;Lahiri, Shuvendu K.;Blackshear, Sam
我们引入了验证模块版本(VMV)，这是一种新的静态分析技术，用于减少静态验证器报告的告警数量，同时提供良好的语义保证。首先，VMV从基础程序P中提取语义环境条件。环境条件可以是充分条件(表示P的安全性)，也可以是必要条件(由P的安全性表示)。然后，VMV用所推断的条件测量程序的新版本P‘。我们证明了我们可以使用(I)充分条件来识别P‘W.r.t的抽象回归。证明P‘W.r.T.的相对正确性的必要条件。P.我们表明，环境条件的提取可以在抽象级别(历史、状态或调用条件)的层次上执行，每个后续级别需要对P‘和P之间的句法变化进行不那么复杂的匹配。调用条件特别有用，因为它们只需要跨程序版本的入口点和被调用者名称的句法匹配。我们已经在一个广泛使用的静态分析和验证工具中实现了VMV。我们在两个大型代码库上报告了我们的经验，并展示了警报的大幅减少，同时还提供了相对的正确性保证。
We introduce Verification Modulo Versions (VMV), a new static analysis technique for reducing the number of alarms reported by static verifiers while providing sound semantic guarantees. First, VMV extracts semantic environment conditions from a base program P. Environmental conditions can either be sufficient conditions (implying the safety of P) or necessary conditions (implied by the safety of P). Then, VMV instruments a new version of the program, P', with the inferred conditions. We prove that we can use (i) sufficient conditions to identify abstract regressions of P' w.r.t. P; and (ii) necessary conditions to prove the relative correctness of P' w.r.t. P. We show that the extraction of environmental conditions can be performed at a hierarchy of abstraction levels (history, state, or call conditions) with each subsequent level requiring a less sophisticated matching of the syntactic changes between P' and P. Call conditions are particularly useful because they only require the syntactic matching of entry points and callee names across program versions. We have implemented VMV in a widely used static analysis and verification tool. We report our experience on two large code bases and demonstrate a substantial reduction in alarms while additionally providing relative correctness guarantees.