Abstract
Designing and maintaining firewall configurations is hard, also for expert system administrators. Indeed, policies are made of a large number of rules and are written in low-level configuration languages that are specific to the firewall system in use. As part of a larger group, we have addressed these issues and have proposed a semantic-based transcompilation pipeline. It is supported by FWS, a tool that analyses a real configuration and ports it from a firewall system to another. To our surprise, we discovered that some configurations expressed in a real firewall system cannot be ported to another system, preserving the semantics. Here we outline the main reasons for the detected differences between the firewall languages, and describe F2F, a tool that checks if a given configuration in a system can be ported to another system, and reports its user on which parts cause problems and why.
The first two authors have been partially supported by project PRA_2018_66 DECLware: Declarative methodologies for designing and deploying applications of the Università di Pisa; the third author by IMT project PAI VeriOSS.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
- 2.
- 3.
- 4.
We use the standard CIDR notation to denote the range of IP addresses.
- 5.
Actually, some translations may occur, typically SNAT, but these are performed by other components of the operating system at run-time.
- 6.
As a matter of fact, it is not ipfw that actually translates address, but it demands this task to other lower level components, possibly to the operating system kernel itself. For the sake of generality, we have only modelled such calls, because the actual translations heavily depend on the specific setting of the system hosting the firewall.
- 7.
References
Adão, P., Bozzato, C., Rossi, G.D., Focardi, R., Luccio, F.L.: Mignis: a semantic based tool for firewall configuration. In: IEEE 27th Computer Security Foundations Symposium, CSF 2014, pp. 351–365 (2014)
Adão, P., Focardi, R., Guttman, J.D., Luccio, F.L.: Localizing firewall security policies. In: Proceedings of the 29th IEEE CSF, Lisbon, Portugal, 27 June–1 July 2016, pp. 194–209 (2016)
Bodei, C., Degano, P., Focardi, R., Galletta, L., Tempesta, M.: Transcompiling firewalls. In: Bauer, L., Küsters, R. (eds.) POST 2018. LNCS, vol. 10804, pp. 303–324. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-89722-6_13
Bodei, C., Degano, P., Focardi, R., Galletta, L., Tempesta, M., Veronese, L.: Language-independent synthesis of firewall policies. In: Proceedings of the 3rd IEEE European Symposium on Security and Privacy (2018)
Ceragioli, L., Degano, P., Galletta, L.: Are All Firewall Systems Equally Powerful? Submitted for publication. https://sysma.imtlucca.it/wp-content/uploads/2019/03/firewall-expressivity.pdf
Ceragioli, L., Galletta, L., Tempesta, M.: From firewalls to functions and back. In: Italian Conference on Cybersecurity ITASEC 2019. CEUR Proceedings, vol. 2315 (2019). http://ceur-ws.org/Vol-2315/paper04.pdf
Cuppens, F., Cuppens-Boulahia, N., Sans, T., Miège, A.: A formal approach to specify and deploy a network security policy. In: Dimitrakos, T., Martinelli, F. (eds.) Formal Aspects in Security and Trust. IIFIP, vol. 173, pp. 203–218. Springer, Boston, MA (2005). https://doi.org/10.1007/0-387-24098-5_15
Diekmann, C., Hupel, L., Michaelis, J., Haslbeck, M.P.L., Carle, G.: Verified iptables firewall analysis and verification. J. Autom. Reason. 61(1–4), 191–242 (2018)
Foley, S.N., Neville, U.: A firewall algebra for openstack. In: 2015 IEEE Conference on Communications and Network Security, CNS 2015, pp. 541–549 (2015)
Martínez, S., Cabot, J., Garcia-Alfaro, J., Cuppens, F., Cuppens-Boulahia, N.: A model-driven approach for the extraction of network access-control policies. In: Proceedings of the MDSec 2012, pp. 5:1–5:6. ACM (2012)
Packet Filter (PF). https://www.openbsd.org/faq/pf/
Russell, R.: Linux 2.4 packet filtering HOWTO (2002). http://www.netfilter.org/ documentation/HOWTO/packet- filtering-HOWTO.html
The IPFW Firewall. https://www.freebsd.org/doc/handbook/firewalls-ipfw.html
The Netfilter Project. https://www.netfilter.org/
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2019 Springer Nature Switzerland AG
About this chapter
Cite this chapter
Ceragioli, L., Degano, P., Galletta, L. (2019). Checking the Expressivity of Firewall Languages. In: Alvim, M., Chatzikokolakis, K., Olarte, C., Valencia, F. (eds) The Art of Modelling Computational Systems: A Journey from Logic and Concurrency to Security and Privacy. Lecture Notes in Computer Science(), vol 11760. Springer, Cham. https://doi.org/10.1007/978-3-030-31175-9_6
Download citation
DOI: https://doi.org/10.1007/978-3-030-31175-9_6
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-31174-2
Online ISBN: 978-3-030-31175-9
eBook Packages: Computer ScienceComputer Science (R0)