Verifying correct usage of context-free API protocols
作者： Kostas Ferles , Jon Stephens , Isil Dillig
DOI: 10.1145/3434298
关键词: Language inclusion 、 Programming language 、 Context (language use) 、 Key (cryptography) 、 Grammar 、 Abstraction (linguistics) 、 Serialization 、 Java 、 Counterexample 、 Computer science
摘要: Several real-world libraries (e.g., reentrant locks, GUI frameworks, serialization libraries) require their clients to use the provided API in a manner that conforms context-free specification. Motivated by this observation, paper describes new technique for verifying correct usage of protocols. The key idea underlying our is over-approximate program’s feasible call sequences using grammar (CFG) and then check language inclusion between However, since may fail due imprecision CFG abstraction, we propose novel refinement progressively improve CFG. In particular, method obtains counterexamples from queries uses them introduce non-terminals productions while still over-approximating relevant behavior. We have implemented proposed algorithm tool called CFPChecker evaluate it on 10 popular Java applications at least one with Our evaluation shows able verify correctly produces those do not. also compare against three baselines demonstrate enables verification safety properties are beyond reach existing tools.
acm.org
sigplan.org参考文章(83)
Régis Blanc, Ashutosh Gupta, Laura Kovács, Bernhard Kragl, Tree Interpolation in Vampire international conference on logic programming. ,vol. 8312, pp. 173- 181 ,(2013) , 10.1007/978-3-642-45221-5_13
Aws Albarghouthi, Arie Gurfinkel, Yi Li, Sagar Chaki, Marsha Chechik, UFO: verification with interpolants and abstract interpretation tools and algorithms for construction and analysis of systems. pp. 637- 640 ,(2013) , 10.1007/978-3-642-36742-7_52
Sergey Grebenshchikov, Ashutosh Gupta, Nuno P. Lopes, Corneliu Popeea, Andrey Rybalchenko, HSF(C): a software verifier based on horn clauses tools and algorithms for construction and analysis of systems. pp. 549- 551 ,(2012) , 10.1007/978-3-642-28756-5_46
Antonio Flores-Montoya, Reiner Hähnle, Resource Analysis of Complex Programs with Cost Equations asian symposium on programming languages and systems. pp. 275- 295 ,(2014) , 10.1007/978-3-319-12736-1_15
Arie Gurfinkel, Temesghen Kahsai, Anvesh Komuravelli, Jorge A. Navas, The SeaHorn Verification Framework Computer Aided Verification. pp. 343- 361 ,(2015) , 10.1007/978-3-319-21690-4_20
Robert DeLine, Manuel Fähndrich, Typestates for Objects european conference on object-oriented programming. ,vol. 3086, pp. 465- 490 ,(2004) , 10.1007/978-3-540-24851-4_21
Aditya Thakur, Junghee Lim, Akash Lal, Amanda Burton, Evan Driscoll, Matt Elder, Tycho Andersen, Thomas Reps, Directed proof generation for machine code computer aided verification. pp. 288- 305 ,(2010) , 10.1007/978-3-642-14295-6_27
Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, Grégoire Sutre, Software verification with BLAST international workshop on model checking software. pp. 235- 239 ,(2003) , 10.1007/3-540-44829-2_17
Kevin Bierhoff, Nels E. Beckman, Jonathan Aldrich, Practical API Protocol Checking with Access Permissions european conference on object oriented programming. pp. 195- 219 ,(2009) , 10.1007/978-3-642-03013-0_10
Nels E. Beckman, Jonathan Aldrich, Duri Kim, An empirical study of object protocols in the wild european conference on object-oriented programming. ,vol. 6813, pp. 2- 26 ,(2011) , 10.5555/2032497.2032501