Verifying Correct Usage of Context-Free API Protocols
summary
CFPChecker verifies context-free grammar API protocols by over-approximating program API sequences with a CFG, checking language inclusion, and running counterexample-guided refinement that uses SMTInterpol for interpolants and z3 for feasibility while building PCFAs from Soot bytecode. Implementation runs on 10 Java applications (12 API–client pairs), initially finds 3 real bugs and after fixes verifies all clients, with average runtime under 10 minutes and median about 1 minute.
AI-written summary · about
chapters (19)
- 0:00Intro
- 0:12MOTIVATION
- 1:04CONTEXT-FREE API PROTOCOLS
- 2:12TYPESTATE ANALYSIS
- 2:41THIS WORK Generalizes prior work on verifying correct API usage!
- 2:57SPECIFICATION LANGUAGE
- 4:32ANATOMY OF CFP CHECKER
- 6:17MOTIVATING EXAMPLE
- 7:05PROG. INSTRUMENTATION
- 9:13ABSTRACTION REFINEMENT LOOP
- 10:03PROGRAM ABSTRACTION
- 11:31INCLUSION CHECK
- 11:54COUNTEREXAMPLE FEASIBILITY
- 13:00ELIMINATING COUNTEREXAMPLE
- 14:34REFINEMENT - NEW CFG
- 15:34NEW ABSTRACTION
- 16:09IMPLEMENTATION
- 16:36EVALUATION
- 16:50CFPCHECKER PERFORMANCE
related talks
30mAPISan: Sanitizing API Usages through Semantic Cross-Checking
58mAutomating Relational Verification of Infinite-State Programs
52mStructure aware fuzzing
21mParDiff: Practical Static Differential Analysis of Network Protocol Parsers
18mSmart Casual Verification of the Confidential Consortium Framework
45mFuzz Testing Web APIs: Overview of Existing Tools
30mC to checked C by 3c
06mFormal Verification with the Certora Prover