More Web Proxy on the site http://driver.im/

research-article

PfComp: A Verified Compiler for Packet Filtering Leveraging Binary Decision Diagrams

Authors:

Clément Chavanon,

Frédéric Besson,

Tristan NinetAuthors Info & Claims

CPP 2024: Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs

Pages 89 - 102

https://doi.org/10.1145/3636501.3636954

Published: 09 January 2024 Publication History

Abstract

We present PfComp, a verified compiler for stateless firewall policies. The policy is first compiled into an intermediate representation taking the form of a binary decision diagram that is optimised in terms of decision nodes. The decision diagram is then compiled into a program. The compiler is proved correct using the Coq proof assistant and extracted into OCaml code. Our preliminary experiments show promising results. The compiler generates code for relatively large firewall policies and the generated code outperforms a sequential evaluation of the policy rules.

References

[1]

2019. Internet Firewall Data. UCI Machine Learning Repository.

[2]

2023. nftables sets. https://wiki.nftables.org/wiki-nftables/index.php/Sets

[3]

NetFilter authors. 2023. NetFilter. https://www.netfilter.org/

[4]

Andrew Begel, Steven McCanne, and Susan L. Graham. 1999. BPF+: Exploiting Global Data-Flow Optimization in a Generalized Packet Filter Architecture. In SIGCOMM. ACM, 123–134.

[5]

Beate Bollig and Ingo Wegener. 1996. Improving the Variable Ordering of OBDDs Is NP-Complete. IEEE Trans. Computers, 45, 9 (1996), 993–1002.

Digital Library

[6]

Thomas Braibant, Jacques-Henri Jourdan, and David Monniaux. 2014. Implementing and Reasoning About Hash-consed Data Structures in Coq. J. Autom. Reason., 53, 3 (2014), 271–304.

Digital Library

[7]

Randal E. Bryant. 1986. Graph-Based Algorithms for Boolean Function Manipulation. IEEE Trans. Computers, 35, 8 (1986), 677–691.

Digital Library

[8]

Mikkel Christiansen and Emmanuel Fleury. 2004. An MTIDD Based Firewall. Telecommun. Syst., 27, 2-4 (2004), 297–319.

Digital Library

[9]

Olivier Coudert and Jean Christophe Madre. 1990. A Unified Framework for the Formal Verification of Sequential Circuits. In ICCAD. IEEE Computer Society, 126–129.

[10]

Jean-Christophe Filliâtre and Sylvain Conchon. 2006. Type-safe modular hash-consing. In ML. ACM, 12–19.

[11]

Mathieu Giorgino and Martin Strecker. 2012. Correctness of Pointer Manipulating Algorithms Illustrated by a Verified BDD Construction. In FM (LNCS, Vol. 7436). Springer, 202–216.

[12]

Scott Hazelhurst, Adi Attar, and Raymond Sinnappan. 2000. Algorithms for Improving the Dependability of ll ll and Filter Rule Lists. In DSN. IEEE Computer Society, 576–585.

[13]

Sava Krstic and John Matthews. 2002. Verifying BDD Algorithms through Monadic Interpretation. In VMCAI (LNCS, Vol. 2294). Springer, 182–195.

[14]

Xavier Leroy. 2009. Formal verification of a realistic compiler. Commun. ACM, 52, 7 (2009), 107–115. https://doi.org/10.1145/1538788.1538814

Digital Library

[15]

Steven McCanne and Van Jacobson. 1993. The BSD Packet Filter: A New Architecture for User-level Packet Capture. In USENIX Winter. USENIX Association, 259–270.

[16]

Frank Mueller and David B. Whalley. 1992. Avoiding Unconditional Jumps by Code Replication. In PLDI. ACM, 322–330.

[17]

Veronika Ortner and Norbert Schirmer. 2005. Verification of BDD Normalization. In TPHOLs (LNCS, Vol. 3603). Springer, 261–277.

Digital Library

[18]

Steffen Smolka, Spiridon Aristides Eliopoulos, Nate Foster, and Arjun Guha. 2015. A fast compiler for NetKAT. In ICFP. ACM, 328–341.

[19]

Fabio Somenzi. 1999. Binary decision diagrams. In Calculational system design (NATO Science Series F: Computer and systems sciences, Vol. 173). IOS Press, 303–366.

[20]

Fabio Somenzi. 2016. CUDD: CU Decision Diagram Package 3.0.0. online. https://framagit.org/nberth/mlcuddidl/-/archive/3.0.7/mlcuddidl-3.0.7.tar.gz

[21]

Kumar Neeraj Verma, Jean Goubault-Larrecq, Sanjiva Prasad, and S. Arun-Kumar. 2000. Reflecting BDDs in Coq. In ASIAN (LNCS, Vol. 1961). Springer, 162–181.

[22]

Xi Wang, David Lazar, Nickolai Zeldovich, Adam Chlipala, and Zachary Tatlock. 2014. Jitk: A Trustworthy In-Kernel Interpreter Infrastructure. In OSDI. USENIX Association, 33–47.

[23]

Mark N. Wegman and F. Kenneth Zadeck. 1991. Constant Propagation with Conditional Branches. ACM Trans. Program. Lang. Syst., 13, 2 (1991), 181–210.

Digital Library

Cited By

Zhang JLiang X(2024)ADLBiLSTM: A Semantic Generation Algorithm for Multi-Grammar Network Access Control PoliciesApplied Sciences10.3390/app1411455514:11(4555)Online publication date: 25-May-2024
https://doi.org/10.3390/app14114555
Monniaux D(2024)Pragmatics of formally verified yet efficient static analysis, in particular, for formally verified compilersInternational Journal on Software Tools for Technology Transfer (STTT)10.1007/s10009-024-00760-326:4(463-477)Online publication date: 1-Aug-2024
https://dl.acm.org/doi/10.1007/s10009-024-00760-3

Index Terms

PfComp: A Verified Compiler for Packet Filtering Leveraging Binary Decision Diagrams

Index terms have been assigned to the content through auto-classification.

Recommendations

Formally Verified Native Code Generation in an Effectful JIT: Turning the CompCert Backend into a Formally Verified JIT Compiler

Modern Just-in-Time compilers (or JITs) typically interleave several mechanisms to execute a program. For faster startup times and to observe the initial behavior of an execution, interpretation can be initially used. But after a while, JITs dynamically ...
Formally verified speculation and deoptimization in a JIT compiler

Just-in-time compilers for dynamic languages routinely generate code under assumptions that may be invalidated at run-time, this allows for specialization of program code to the common case in order to avoid unnecessary overheads due to uncommon cases. ...
A formally verified compiler for Lustre
PLDI '17

The correct compilation of block diagram languages like Lustre, Scade, and a discrete subset of Simulink is important since they are used to program critical embedded control software. We describe the specification and verification in an Interactive ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

CPP 2024: Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs

January 2024

290 pages

ISBN:9798400704888

DOI:10.1145/3636501

General Chairs:
Amin Timany
Aarhus University, Denmark
,
Dmitriy Traytel
University of Copenhagen, Denmark
,
Program Chairs:
Brigitte Pientka
McGill University, Canada
,
Sandrine Blazy
University of Rennes, France

Copyright © 2024 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].

Sponsors

SIGPLAN: ACM Special Interest Group on Programming Languages

In-Cooperation

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 09 January 2024

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

CPP '24

Sponsor:

SIGPLAN

CPP '24: 13th ACM SIGPLAN International Conference on Certified Programs and Proofs

January 15 - 16, 2024

London, UK

Acceptance Rates

Overall Acceptance Rate 18 of 26 submissions, 69%

Upcoming Conference

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

2
Total Citations
View Citations
102
Total Downloads

Downloads (Last 12 months)58
Downloads (Last 6 weeks)4

Reflects downloads up to 01 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

Zhang JLiang X(2024)ADLBiLSTM: A Semantic Generation Algorithm for Multi-Grammar Network Access Control PoliciesApplied Sciences10.3390/app1411455514:11(4555)Online publication date: 25-May-2024
https://doi.org/10.3390/app14114555
Monniaux D(2024)Pragmatics of formally verified yet efficient static analysis, in particular, for formally verified compilersInternational Journal on Software Tools for Technology Transfer (STTT)10.1007/s10009-024-00760-326:4(463-477)Online publication date: 1-Aug-2024
https://dl.acm.org/doi/10.1007/s10009-024-00760-3

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Figures

Tables

Media

View Table of Conten