正确使用与上下文无关的API协议（扩展版）
Verifying Correct Usage of Context-Free API Protocols (Extended Version)
摘要：
几个真实世界的库（例如，可重入锁、GUI框架、序列化库）要求它们的客户端以符合上下文无关规范的方式使用所提供的API。受此观察的启发，本文描述了一种用于验证上下文无关API协议的正确使用的新技术。我们的技术的关键思想是过度近似的程序的可行的API调用序列使用一个上下文无关文法（CFG），然后检查这个语法和规范之间的语言包含。然而，由于这种包含检查可能会失败，由于不精确的程序的CFG抽象，我们提出了一种新的细化技术，逐步提高CFG。特别是，我们的方法从CFG包含查询中获得反例，并使用它们来引入新的非终端和生产的语法，同时仍然过度近似程序的相关行为。我们已经实现了所提出的算法，在一个工具，称为CFPUNK和评估它的10个流行的Java应用程序，使用至少一个API与上下文无关的规范。我们的评估表明，CFPPER能够在正确使用API的客户端中验证API的正确使用，并为那些不正确使用API的客户端生成反例。我们还将我们的方法与三个相关的基线进行了比较，并证明CFPstrike可以验证现有工具无法达到的安全属性。
英文摘要：
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 to a context-free specification. Motivated by this observation, this paper describes a new technique for verifying the correct usage of context-free API protocols. The key idea underlying our technique is to over-approximate the program's feasible API call sequences using a context-free grammar (CFG) and then check language inclusion between this grammar and the specification. However, since this inclusion check may fail due to imprecision in the program's CFG abstraction, we propose a novel refinement technique to progressively improve the CFG. In particular, our method obtains counterexamples from CFG inclusion queries and uses them to introduce new non-terminals and productions to the grammar while still over-approximating the program's relevant behavior. We have implemented the proposed algorithm in a tool called CFPChecker and evaluate it on 10 popular Java applications that use at least one API with a context-free specification. Our evaluation shows that CFPChecker is able to verify correct usage of the API in clients that use it correctly and produces counterexamples for those that do not. We also compare our method against three relevant baselines and demonstrate that CFPChecker enables verification of safety properties that are beyond the reach of existing tools.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
