Verified iptables firewall analysis and verification

DOI10.1007/s10817-017-9445-1zbMath1451.68173OpenAlexW2781706673WikidataQ90699732 ScholiaQ90699732MaRDI QIDQ1663231

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

Publication date: 21 August 2018

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

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

zbMATH Keywords

formal verificationsemanticsfirewallsIsabellecomputer networksiptablesnetfilter

Mathematics Subject Classification ID

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

Related Items

Verified iptables firewall analysis and verification

Uses Software

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

Cites Work

• Unnamed Item
• Isabelle/HOL. A proof assistant for higher-order logic
• Verified iptables firewall analysis and verification
• A Coalgebraic Decision Procedure for NetKAT
• Applying Data Refinement for Monadic Programs to Hopcroft’s Algorithm
• Concrete Semantics
• A fast compiler for NetKAT
• Code Generation via Higher-Order Rewrite Systems
• Automatic Data Refinement
• NetKAT