Verified iptables firewall analysis and verification

DOI10.1007/S10817-017-9445-1MaRDI QIDQ1663231zbMATH OpenOpenAlexWikidataFDO

Authors Cornelius Diekmann, Lars Hupel, Julius Michaelis, Georg Carle, Maximilian P. L. Haslbeck

Publication date 21 August 2018

Published in Journal of Automated Reasoning (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/s10817-017-9445-1

zbMATH Keywords

semanticsfirewallsformal verificationIsabellecomputer networksiptablesnetfilter

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Network design and communication in computer systems (68M10) Computer security (68M25) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• Validating firewalls using flow logics
• scientific article; zbMATH DE number 2080705
• scientific article; zbMATH DE number 2084352
• scientific article; zbMATH DE number 1983212
• Firewall policy verification and troubleshooting

Cites work

• scientific article; zbMATH DE number 3073037 (Why is no real title available?)
• A coalgebraic decision procedure for NetKAT
• A fast compiler for NetKAT
• Applying data refinement for monadic programs to Hopcroft's algorithm
• Automatic Data Refinement
• Code generation via higher-order rewrite systems
• Concrete semantics. With Isabelle/HOL
• Isabelle/HOL. A proof assistant for higher-order logic
• Netkat, semantic foundations for networks
• Verified iptables firewall analysis and verification

Cited in

(2)

• Firewall policy verification and troubleshooting
• Verified iptables firewall analysis and verification

Describes a project that uses

Uses Software

• Isabelle
• Isabelle/HOL
• TikZ
• FIREMAN
• Firmato
• Autoref
• NetCore
• NetKAT
• Archive Formal Proofs
• Firewall Builder
• Simple Firewall
• IP Addresses
• UPF Firewall
• Iptables Semantics
• margrave
• LOFT
• ConfigChecker
• Routing
• pgf
• GitHub
• iptables
• nftables

This page was built for publication: Verified iptables firewall analysis and verification

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1663231)