SMT-based verification of program changes through summary repair
Tóm tắt
This article provides an innovative approach for verification by model checking of programs that undergo continuous changes. To tackle the problem of repeating the entire model checking for each new version of the program, our approach verifies programs incrementally. It reuses computational history of the previous program version, namely function summaries. In particular, the summaries are over-approximations of the bounded program behaviors. Whenever reusing of summaries is not possible straight away, our algorithm repairs the summaries to maximize the chance of reusability of them for subsequent runs. We base our approach on satisfiability modulo theories (SMT) to take full advantage of lightweight modeling approach and at the same time the ability to provide concise function summarization. Our approach leverages pre-computed function summaries in SMT to localize the checks of changed functions. Furthermore, to exploit the trade-off between precision and performance, our approach relies on the use of an SMT solver, not only for underlying reasoning, but also for program modeling and the adjustment of its precision. On the benchmark suite of primarily Linux device drivers versions, we demonstrate that our algorithm achieves an order of magnitude speedup compared to prior approaches.
Tài liệu tham khảo
Clarke EM, Emerson EA (1981) Design and synthesis of synchronization skeletons using branching-time temporal logic. In: Workshop on logics of programs, pp 52–71. Springer, Heidelberg
Queille J, Sifakis J (1982) Specification and verification of concurrent systems in CESAR. In: 5th International symposium on programming, pp 337–351
Biere A, Cimatti A, Clarke EM, Zhu Y (1999) Symbolic model checking without BDDs. In: TACAS 1999, vol 1579, pp 193–207. Springer, Heidelberg
Fedyukovich G, Sery O, Sharygina N (2013) eVolCheck: Incremental upgrade checker for C. In: TACAS 2013, vol 7795, pp 292–307. Springer, Heidelberg
Barrett C, Sebastiani R, Seshia S, Tinelli C (2009) Satisfiability modulo theories, vol 185, 1st edn., pp 825–885
de Moura LM, Bjørner N (2009) Satisfiability modulo theories: An appetizer. In: SBMF 2009. LNCS, vol 5902, pp 23–36. Springer, Heidelberg
Craig W (1957) Three uses of the herbrand–Gentzen theorem in relating model theory and proof theory. J Symb Log 22(3):269–285
Sery O, Fedyukovich G, Sharygina N (2011) Interpolation-based function summaries in bounded model checking. In: HVC 2011, vol 7261, pp 160–175. Springer, Heidelberg
Asadi S, Blicha M, Fedyukovich G, Hyvärinen AEJ, Even-Mendoza K, Sharygina N, Chockler H (2018) Function summarization modulo theories. In: LPAR-22, vol 57, pp 56–75. EasyChair, England & Wales
Rollini SF, Alt L, Fedyukovich G, Hyvärinen A, Sharygina N (2013) PeRIPLO: A framework for producing effective interpolants in SAT-based software verification. In: LPAR 2013, vol 8312, pp 683–693. Springer, Heidelberg
Alt L, Asadi S, Chockler H, Even-Mendoza K, Fedyukovich G, Hyvärinen A, Sharygina N (2017) HiFrog: SMT-based function summarization for software verification. In: TACAS 2017, vol 10206, pp 207–213. Springer, Heidelberg
Sery O, Fedyukovich G, Sharygina N (2012) Incremental upgrade checking by means of interpolation-based function summaries. In: FMCAD 2012, pp 114–121. IEEE, New York
Fedyukovich G, Sery O, Sharygina N (2017) Flexible SAT-based framework for incremental bounded upgrade checking. STTT 19(5):517–534
Asadi S, Blicha M, Hyvärinen A, Fedyukovich G, Sharygina N (2020) Incremental verification by SMT-based summary repair. In: FMCAD 2020. IEEE, New York
Silva T, Porto C, da S Alves EH, Cordeiro LC, Rocha H (2021) Verifying security vulnerabilities in large software systems using multi-core k-induction. CoRR arXiv:abs/2102.02368
Kroening D, Tautschnig M (1976) CBMC—C bounded model checker. In: TACAS 2014, vol 42, pp 389–391. Springer, Heidelberg
Clarke E, Kroening D, Lerda F (2004) A tool for checking ANSI-C programs. In: TACAS 2004, vol 2988, pp 168–176. Springer, Berlin, Heidelberg
McMillan KL (2003) Interpolation and SAT-based model checking. In: CAV 2003, pp 1–13
Henzinger T, Jhala R, Majumdar R, McMillan KL (2004) Abstractions from Proofs. In: POPL
Asadi S, Blicha M, Hyvärinen A, Fedyukovich G, Sharygina N (2020) Farkas-based tree interpolation. In: SAS 2020. Springer, Heidelberg
Blanc R, Gupta A, Kovács L, Kragl B (2013) Tree interpolation in Vampire. In: LPAR 2013, vol 8312, pp 173–181. Springer, Berlin
Komuravelli A, Gurfinkel A, Chaki S, Clarke EM (2013) Automatic abstraction in SMT-based unbounded software model checking. In: CAV 2013. LNCS, vol 8044, pp 846–862. Springer, Berlin
Fedyukovich G, Bodík R (2018) Accelerating Syntax-Guided Invariant Synthesis. In: TACAS, 2018, vol 10805, pp 251–269. Springer, Heidelberg
Flanagan C, Leino KRM (2001) Houdini, an annotation assistant for esc/java. In: FME 2001, vol 2021, pp 500–517. Springer, Heidelberg
Schrijver A (1999) Theory of linear and integer programming. Wiley-Interscience series in discrete mathematics and optimization. Wiley, Sons, London
McMillan KL (2005) An interpolating theorem prover. Theor Comput Sci 345(1):101–121
Blicha M, Hyvärinen A, Kofron J, Sharygina N (2019) Decomposing Farkas interpolants. In: TACAS 2019, vol 11427, pp 3–20. Springer, Heidelberg
Alt L, Hyvärinen A, Asadi S, Sharygina N (2017) Duality-based interpolation for quantifier-free equalities and uninterpreted functions. In: FMCAD 2017, pp 39–46. FMCAD Inc, Austin, Texas
Pudlák P (1997) Lower bounds for resolution and cutting plane proofs and monotone computations. J Symb Log 62(3):981–998
Christ J, Hoenicke J (2016) Proof tree preserving tree interpolation. J Autom Reasoning 57(1):67–95
Gurfinkel A, Rollini SF, Sharygina N (2013) Interpolation properties and SAT-based model checking. In: ATVA 2013, pp 255–271
Hyvärinen A, Marescotti M, Alt L, Sharygina N (2016) OpenSMT2: An SMT solver for multi-core and cloud computing. In: SAT 2016, vol 9710, pp 547–553. Springer, Heidelberg
Alt L, Fedyukovich G, Hyvärinen A, Sharygina N (2016) A proof-sensitive approach for small propositional interpolants. In: VSTTE 2015, vol 9593, pp 1–18. Springer, Berlin, Heidelberg
Beyer D, Löwe S, Novikov E, Stahlbauer A, Wendler P (2013) Precision reuse for efficient regression verification. In: ESEC/FSE 2013, pp 389–399. ACM, New York
Conway CL, Namjoshi KS, Dams D, Edwards SA (2005) Incremental algorithms for inter-procedural analysis of safety properties. In: CAV 2005, vol 3576, pp 449–461. Springer, Heidelberg
Trostanetski A, Grumberg O, Kroening D (2017) Modular demand-driven analysis of semantic difference for program versions. In: SAS 2017, vol 10422, pp 405–427. Springer, Cham
He F, Yu Q, Cai L (2018) When regression verification meets CEGAR. CoRR arXiv:abs/1806.04829
Rothenberg B, Dietsch D, Heizmann M (2018) Incremental verification using trace abstraction. In: Static analysis—25th international symposium, SAS 2018, pp 364–382
Beyer D, Jakobs M, Lemberger T (2020) Difference verification with conditions. In: SEFM 2020, vol 12310, pp 133–154. Springer, Cham
Lauterburg S, Sobeih A, Marinov D, Viswanathan M (2008) Incremental state-space exploration for programs with dynamically allocated data. In: ICSE 2008, pp 291–300. ACM, New York
Visser W, Geldenhuys J, Dwyer MB (2012) Green: reducing, reusing and recycling constraints in program analysis. In: SIGSOFT/FSE 2012, p 58. ACM, New York
Fedyukovich G, Gurfinkel A, Sharygina N (2014) Incremental verification of compiler optimizations. In: NFM 2014, pp 300–306
Fedyukovich G, Gurfinkel A, Sharygina N (2016) Property directed equivalence via abstract simulation. In: Proc. CAV 2016, vol 9780, Part II, pp 433–453. Springer, Cham
Hardin RH, Kurshan RP, McMillan KL, Reeds JA, Sloane NJA (1996) Efficient regression verification. In: Proc. WODES’96, pp 147–150. IEEE, Proc
Godlin B, Strichman O (2009) Regression verification. In: The 46th design automation conference, DAC, pp 466–471. ACM, New York
Lahiri SK, McMillan KL, Sharma R, Hawblitzel C (2013) Differential assertion checking. In: ESEC/FSE 2013, pp 345–355. ACM, New York
Pick L, Fedyukovich G, Gupta A (2018) Exploiting synchrony and symmetry in relational verification. In: CAV 2018, Part I, vol 10981, pp 164–182. Springer, Cham
Shemer R, Gurfinkel A, Shoham S, Vizel Y (2019) Property directed self composition. In: CAV 2019, vol 11561, pp 161–179. Springer, Heidelberg
Mordvinov D, Fedyukovich G (2019) Property directed inference of relational invariants. In: FMCAD 2019, pp 152–160. IEEE, San Jose
Felsing D, Grebing S, Klebanov V, Rümmer P, Ulbrich M (2014) Automating regression verification. In: ASE 2014, pp 349–360. ACM, New York
Yang G, Khurshid S, Person S, Rungta N (2014) Property differencing for incremental checking. In: ICSE 2014, pp 1059–1070. ACM, New York
Lahiri SK, Hawblitzel C, Kawaguchi M, Rebêlo H (2012) SYMDIFF: A language-agnostic semantic diff tool for imperative programs. In: CAV 2012, vol 7358, pp 712–717. Springer, Heidelberg
Godefroid P, Lahiri SK, Rubio-González C (2011) Statically validating must summaries for incremental compositional dynamic test generation. In: SAS 2011, vol 6887, pp 112–128. Springer, Heidelberg
McMillan KL (2010) Lazy annotation for program testing and verification. In: CAV 2010. LNCS, vol 6174, pp 104–118. Springer, Heidelberg (2010)
Albarghouthi A, Gurfinkel A, Chechik M (2012) Whale: An interpolation-based algorithm for inter-procedural verification. In: VMCAI 2012. LNCS, vol 7148, pp 39–55. Springer, Heidelberg (2012)