POPL 2021 (series) / CoqPL 2021 (series) / The Seventh International Workshop on Coq for Programming Languages /
Automated Synthesis of Verified Firewalls
Tue 19 Jan 2021 17:15 - 17:30 at CoqPL - Contributed Talks
We demonstrate correct-by-construction firewalls—stateful packet filters for TCP/IP packets—using the Fiat synthesis library [3]. We present a general DSL for specifying their behavior independent of algorithmic implementation. We outline the design of a verified compiler in Coq, detail a few verified efficiency optimizations, and show how the compiler can easily be extended to support custom optimizations for user-defined policies.
| Abstract (coqpl21-final7.pdf) | 344KiB |
Tue 19 Jan Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
Tue 19 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
| 16:00 - 16:15 Talk | A Limited Case for Reification by Type Inference CoqPL Jason GrossMIT CSAIL Media Attached File Attached | ||
| 16:15 - 16:30 Talk | Towards a Coq Specification for Generalized Algebraic Datatypes in OCaml CoqPL File Attached | ||
| 16:30 - 16:45 Talk | Record Updates in Coq CoqPL Tej ChajedMassachusetts Institute of Technology, USA Media Attached File Attached | ||
| 16:45 - 17:00 Break | Break CoqPL | ||
| 17:00 - 17:15 Talk | The B+-tree Index as a Verified Software Unit CoqPL Anastasiya Kravchuk-KirilyukHarvard University, Andrew AppelPrinceton, Lennart BeringerPrinceton University File Attached | ||
| 17:15 - 17:30 Talk | Automated Synthesis of Verified Firewalls CoqPL Shardul ChiplunkarMassachusetts Institute of Technology, Clément Pit-ClaudelMassachusetts Institute of Technology, USA, Adam ChlipalaMassachusetts Institute of Technology File Attached | ||