A Domain-Specific Language for Filtering in Application-Level Gateways
summary
A compact declarative DSL implements application-level packet filters, automatically synthesizes a validator and filter, and uses static verification via an SMT solver to prove absence of pitfalls like impossible assertions, vacuous checks, division-by-zero, and subverted repairs. The system eliminates ZoneGuard’s extra output validation, runs checks in under a second on realistic rules, reimplements existing ZoneGuard filters with far fewer tokens and lines, and catches conflicting repairs (e.g., clamp to -1 vs 0) before deployment.
AI-written summary · about
chapters (10)
- 0:00Start
- 1:27Example: Remote Desktop Protocol
- 3:59Architecture and Approach
- 4:54A Small Protocol
- 9:45Filter Language Design
- 11:18Pitfalls
- 12:16Pitfall Protection: Lemma Generation
- 12:43Evaluation: Comparing against Advenica's ZoneGuard system
- 13:38Is Our Language a Good Fit for Filter Engineers?
- 14:53Conclusions
related talks
12mAutomated Synthesis of Verified Firewalls
31mPfComp: A Verified Compiler for Packet Filtering Leveraging Binary Decision Diagr...- 12mAutomated Synthesis of Verified Firewalls
15mLiquid Information Flow Control
01h 00mAI Safety through Programming?
36mSpam-fighting Infrastructure
46mApplication Gateway Security What Developers Really Need to Know
04mAutomatically Eliminating Speculative Leaks with Blade