×

Verified iptables firewall analysis and verification. (English) Zbl 1451.68173

Summary: This article summarizes our efforts around the formally verified static analysis of iptables rulesets using Isabelle/HOL. We build our work around a formal semantics of the behavior of iptables firewalls. This semantics is tailored to the specifics of the filter table and supports arbitrary match expressions, even new ones that may be added in the future. Around that, we organize a set of simplification procedures and their correctness proofs: we include procedures that can unfold calls to user-defined chains, simplify match expressions, and construct approximations removing unknown or unwanted match expressions. For analysis purposes, we describe a simplified model of firewalls that only supports a single list of rules with limited expressiveness. We provide and verify procedures that translate from the complex iptables language into this simple model. Based on that, we implement the verified generation of IP space partitions and minimal service matrices. An evaluation of our work on a large set of real-world firewall rulesets shows that our framework provides interesting results in many situations, and can both help and out-compete other static analysis frameworks found in related work.

MSC:

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

References:

[1] Al-Shaer, E., Alsaleh, M.: ConfigChecker: a tool for comprehensive security configuration analytics. In: Configuration Analytics and Automation (SAFECONFIG), pp. 1-2. IEEE (2011). https://doi.org/10.1109/SafeConfig.2011.6111667
[2] Al-Shaer, E., Hamed, H.: Discovery of policy anomalies in distributed firewalls. In: Annual Joint Conference of the IEEE Computer and Communications Societies (INFOCOM), vol. 4, pp. 2605-2616 (2004). https://doi.org/10.1109/INFCOM.2004.1354680
[3] Analyzed firewall rulesets (raw data). https://github.com/diekmann/net-network. Accompanying material
[4] Anderson, C.J., Foster, N., Guha, A., Jeannin, J.B., Kozen, D., Schlesinger, C., Walker, D.: NetKAT: semantic foundations for networks. In: 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’14, pp. 113-126. ACM, San Diego (2014). https://doi.org/10.1145/2535838.2535862 · Zbl 1284.68100
[5] Baker, F., Savola, P.: Ingress filtering for multihomed networks. RFC 3704 (Best Current Practice) (2004)
[6] Bartal, Y., Mayer, A., Nissim, K., Wool, A.: Firmato: a novel firewall management toolkit. In: IEEE Symposium on Security and Privacy, pp. 17-31. IEEE (1999). https://doi.org/10.1109/SECPRI.1999.766714
[7] Bianchi, G; Bonola, M; Capone, A; Cascone, C, Openstate: programming platform-independent stateful openflow applications inside the switch, ACM SIGCOMM Comput. Commun. Rev., 44, 44-51, (2014) · doi:10.1145/2602204.2602211
[8] Brucker, A.D., Brügger, L., Kearney, P., Wolff, B.: Verified firewall policy transformations for test case generation. In: 3rd International Conference on Software Testing, Verification and Validation, pp. 345-354. IEEE (2010). https://doi.org/10.1109/ICST.2010.50
[9] Brucker, A.D., Brügger, L., Wolff, B.: Model-based firewall conformance testing. In: Suzuki, K., Higashino, T., Ulrich, A., Hasegawa, T. (eds.) Testing of Software and Communicating Systems, pp. 103-118. Springer (2008)
[10] Brucker, A.D., Brügger, L., Wolff, B.: Formal firewall conformance testing: an application of test and proof techniques. Softw. Test. Verif. Reliab. (STVR) 25(1), 34-71 (2015). https://doi.org/10.1002/stvr.1544, https://www.brucker.ch/bibliography/abstract/brucker.ea-formal-fw-testing-2014
[11] Brucker, A.D., Brügger, L., Wolff, B.: Formal network models and their application to firewall policies. Archive of Formal Proofs (2017). http://isa-afp.org/entries/UPF_Firewall.shtml. Formal proof development
[12] Byma, S., Tarafdar, N., Xu, T., Bannazadeh, H., Leon-Garcia, A., Chow, P.: Expanding OpenFlow capabilities with virtualized reconfigurable hardware. In: ACM/SIGDA International Symposium on Field-Programmable Gate Arrays, FPGA ’15, pp. 94-97. ACM, Monterey (2015). https://doi.org/10.1145/2684746.2689086
[13] Capretta, V., Stepien, B., Felty, A., Matwin, S.: Formal correctness of conflict detection for firewalls. In: Workshop on Formal Methods in Security Engineering, pp. 22-30. ACM (2007). https://doi.org/10.1145/1314436.1314440
[14] Cisco IOS firewall—configuring IP access lists. Document ID: 23602 (2007). http://www.cisco.com/c/en/us/support/docs/security/ios-firewall/23602-confaccesslists.html
[15] Cotton, M., Vegoda, L., Bonica, R., Haberman, B.: Special-purpose IP address registries. RFC 6890 (Best Current Practice) (2013)
[16] CrazyCat: iptables multiport and negation. Server Fault Question (2016). http://serverfault.com/questions/793631/iptables-multiport-and-negation/
[17] Deering, S., Hinden, R.: Internet protocol, version 6 (IPv6) specification. RFC 2460 (Draft Standard) (1998). Updated by RFCs 5095, 5722, 5871, 6437, 6564, 6935, 6946, 7045, 7112
[18] Diekmann, C.: Naming network interfaces. In: PoC||GTFO: Pastor Laphroaig Races the Runtime Relinker and Other True Tales of Cleverness and Craft, vol. 16, no. 08, pp. 45-46 (2017)
[19] Diekmann, C., Hupel, L.: Iptables semantics. Archive of Formal Proofs (2016). http://isa-afp.org/entries/Iptables_Semantics.shtml. Formal proof development
[20] Diekmann, C., Hupel, L., Carle, G.: Directed security policies: a stateful network implementation. In: Electronic Proceedings in Theoretical Computer Science on Engineering Safety and Security Systems (ESSS), vol. 150, pp. 20-34. Open Publishing Association, Singapore (2014). https://doi.org/10.4204/EPTCS.150.3
[21] Diekmann, C., Korsten, A., Carle, G.: Demonstrating topoS: theorem-prover-based synthesis of secure network configurations. In: 11th International Conference on Network and Service Management (CNSM), pp. 366-371. Barcelona (2015). https://doi.org/10.1109/CNSM.2015.7367384
[22] Diekmann, C., Michaelis, J., Haslbeck, M.: Simple firewall. Archive of Formal Proofs (2016). http://isa-afp.org/entries/Simple_Firewall.shtml. Formal proof development · Zbl 1451.68173
[23] Diekmann, C., Michaelis, J., Haslbeck, M., Carle, G.: Verified iptables firewall analysis. In: IFIP Networking 2016. Vienna (2016) · Zbl 1451.68173
[24] Diekmann, C., Michaelis, J., Hupel, L.: IP addresses. Archive of Formal Proofs (2016). http://isa-afp.org/entries/IP_Addresses.shtml. Formal proof development
[25] Diekmann, C., Posselt, S.A., Niedermayer, H., Kinkelin, H., Hanka, O., Carle, G.: Verifying security policies using host attributes. In: Formal Techniques for Distributed Objects, Components, and Systems: 34th IFIP WG 6.1 International Conference, FORTE, pp. 133-148. Springer, Berlin (2014). https://doi.org/10.1007/978-3-662-43613-4_9
[26] Diekmann, C., Schwaighofer, L., Carle, G.: Certifying spoofing-protection of firewalls. In: 11th International Conference on Network and Service Management (CNSM), pp. 168-172. Barcelona (2015). https://doi.org/10.1109/CNSM.2015.7367354
[27] diekmann/Iptables_Semantics: Issue #113—Port numbers belong to a specific protocol. github (2016). https://github.com/diekmann/Iptables_Semantics/issues/113
[28] Eastep, T.M.: iptables made ease—shorewall (2014). http://shorewall.net/
[29] Engelhardt, J.: Towards the perfect ruleset (2011). http://inai.de/documents/Perfect_Ruleset.pdf
[30] Foster, N., Kozen, D., Milano, M., Silva, A., Thompson, L.: A coalgebraic decision procedure for NetKAT. In: 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’15, pp. 343-355. ACM, Mumbai (2015). https://doi.org/10.1145/2676726.2677011 · Zbl 1346.68132
[31] Fuller, V., Li, T.: Classless inter-domain routing (CIDR): the internet address assignment and aggregation plan. RFC 4632 (Best Current Practice) (2006)
[32] Gartenmeister, M.: Iptables vs. Cisco PIX (2005). http://lists.netfilter.org/pipermail/netfilter/2005-April/059714.html
[33] Guha, A., Reitblatt, M., Foster, N.: Machine-verified network controllers. In: 34th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI ’13, pp. 483-494. ACM, Seattle (2013). https://doi.org/10.1145/2462156.2462178
[34] Haftmann, F., Bulwahn, L.: Code generation from Isabelle/HOL theories (2016)
[35] Haftmann, F., Nipkow, T.: Code generation via higher-order rewrite systems. In: Blume, M., Kobayashi, N., Vidal, G. (eds.) Functional and Logic Programming, pp. 103-117. Springer (2010) · Zbl 1284.68131
[36] Hamed, H; Al-Shaer, E, Taxonomy of conflicts in network security policies, IEEE Commun. Mag., 44, 134-141, (2006) · doi:10.1109/MCOM.2006.1607877
[37] Hewlett Packard: IP firewall configuration guide (2005). ftp://ftp.hp.com/pub/networking/software/ProCurve-SR-IP-Firewall-Config-Guide.pdf
[38] IPTables Example Config. http://networking.ringofsaturn.com/Unix/iptables.php. Retrieved Sept 2014
[39] Jeffrey, A., Samak, T.: Model checking firewall policy configurations. In: Policies for Distributed Systems and Networks, pp. 60-67. IEEE (2009). https://doi.org/10.1109/POLICY.2009.32
[40] Kawamura, S., Kawashima, M.: A recommendation for IPv6 address text representation. RFC 5952 (Proposed Standard) (2010)
[41] Kazemian, P., Varghese, G., McKeown, N.: Header space analysis: static checking for networks. In: 9th USENIX Symposium on Networked Systems Design and Implementation (NSDI), NSDI’12, pp. 113-126. USENIX Association, San Jose (2012)
[42] Kleene, S.C.: Introduction to Metamathematics. Bibliotheca Mathematica. North-Holland, Amsterdam (1952) · Zbl 0047.00703
[43] Lammich, P.: Automatic Data Refinement, pp. 84-99. Springer, Berlin (2013). https://doi.org/10.1007/978-3-642-39634-2_9 · Zbl 1317.68216 · doi:10.1007/978-3-642-39634-2_9
[44] Lammich, P., Tuerk, T.: Applying Data Refinement for Monadic Programs to Hopcroft’s Algorithm, pp. 166-182. Springer, Berlin (2012). https://doi.org/10.1007/978-3-642-32347-8_12 · Zbl 1360.68757 · doi:10.1007/978-3-642-32347-8_12
[45] Leblond, E.: Why you will love nftables (2014). https://home.regit.org/2014/01/why-you-will-love-nftables/
[46] Linux Kernel Sources: Linux/include/linux/netfilter/x_tables.h. Kernel 4.6. http://lxr.free-electrons.com/source/include/linux/netfilter/x_tables.h?v=4.6#L343
[47] Mansmann, F., Göbel, T., Cheswick, W.: Visual analysis of complex firewall configurations. In: 9th International Symposium on Visualization for Cyber Security, VizSec ’12, pp. 1-8. ACM (2012). https://doi.org/10.1145/2379690.2379691
[48] Marmorstein, R.M., Kearns, P.: A tool for automated iptables firewall analysis. In: USENIX Annual Technical Conference, FREENIX Track, pp. 71-81. USENIX Association (2005)
[49] Marmorstein, R.M., Kearns, P., et al.: Firewall analysis with policy-based host classification. In: 20th USENIX Large Installation System Administration Conference (LISA), vol. 6. USENIX Association, Washington (2006)
[50] Michaelis, J., Diekmann, C.: LOFT—verified migration of Linux firewalls to SDN. Archive of Formal Proofs (2016). http://isa-afp.org/entries/LOFT.shtml. Formal proof development
[51] Michaelis, J., Diekmann, C.: Routing. Archive of Formal Proofs (2016). http://isa-afp.org/entries/Routing.shtml. Formal proof development
[52] Monsanto, C., Foster, N., Harrison, R., Walker, D.: A compiler and run-time system for network programming languages. In: 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’12, pp. 217-230. ACM (2012)
[53] Moy, E., Gildea, S., Dickey, T.: XTerm control sequences (2016). http://invisible-island.net/xterm/ctlseqs/ctlseqs.html
[54] Nelson, T., Barratt, C., Dougherty, D.J., Fisler, K., Krishnamurthi, S.: The Margrave tool for firewall analysis. In: 24th USENIX Large Installation System Administration Conference (LISA). USENIX Association, San Jose (2010)
[55] Nelson, T., Ferguson, A.D., Krishnamurthi, S.: Static Differential Program Analysis for Software-Defined Networks, pp. 395-413. Springer, Berlin (2015). https://doi.org/10.1007/978-3-319-19249-9_25 · doi:10.1007/978-3-319-19249-9_25
[56] Nelson, T., Ferguson, A.D., Scheer, M.J., Krishnamurthi, S.: Tierless programming and reasoning for software-defined networks. In: 11th USENIX Symposium on Networked Systems Design and Implementation (NSDI), NSDI’14, pp. 519-531. USENIX Association, Seattle (2014)
[57] Nelson, T., Ferguson, A.D., Yu, D., Fonseca, R., Krishnamurthi, S.: Exodus: toward automatic migration of enterprise network configurations to SDNs. In: 1st ACM SIGCOMM Symposium on Software Defined Networking Research, no. 13 in SOSR ’15, pp. 13:1-13:7. ACM, Santa Clara (2015). https://doi.org/10.1145/2774993.2774997
[58] Nelson, T., Guha, A., Dougherty, D.J., Fisler, K., Krishnamurthi, S.: A balance of power: expressive, analyzable controller programming. In: Second ACM SIGCOMM Workshop on Hot Topics in Software Defined Networking, HotSDN ’13, pp. 79-84. ACM, Hong Kong (2013). https://doi.org/10.1145/2491185.2491201
[59] NetCitadel, Inc.: FirewallBuilder. http://www.fwbuilder.org. Ver. 5.1
[60] netfilter coreteam: libxtables/xtables.c. https://git.netfilter.org/iptables/tree/libxtables/xtables.c?h=v1.6.0#n518
[61] Nicira, Inc.: Nicira extensions. openvswitch/ovs repository (2016). https://github.com/openvswitch/ovs/blob/master/include/openflow/nicira-ext.h. Revision fb8f22c186b89cd36059c37908f940a1aa5e1569
[62] Nipkow, T., Klein, G.: Concrete Semantics. Springer, Berlin (2014). https://doi.org/10.1007/978-3-319-10542-0 · Zbl 1410.68004 · doi:10.1007/978-3-319-10542-0
[63] Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL: a proof assistant for higher-order logic. In: LNCS, vol. 2283. Springer (2002, last updated 2016). http://isabelle.in.tum.de/ · Zbl 0994.68131
[64] Nygren, A., Pfaff, B., Lantz, B., Heller, B., Barker, C., Beckmann, C., Cohn, D., Malek, D., Talayco, D., Erickson, D., McDysan, D., Ward, D., Crabbe, E., Schneider, F., Gibb, G., Appenzeller, G., Tourrilhes, J., Tonsing, J., Pettit, J., Yap, K., Poutievski, L., Dunbar, L., Vicisano, L., Casado, M., Takahashi, M., Kobayashi, M., Orr, M., Yadav, N., McKeown, N., dHeureuse, N., Balland, P., Madabushi, R., Ramanathan, R., Price, R., Sherwood, R., Das, S., Gandham, S., Curtis, S., Natarajan, S., Mizrahi, T., Yabe, T., Ding, W., Yiakoumis, Y., Moses, Y., Kis, Z.L.: OpenFlow switch specification v1.5.1 (2015). https://www.opennetworking.org/images/stories/downloads/sdn-resources/onf-specifications/openflow/openflow-switch-v1.5.1.pdf.ONFTS-025
[65] Petrucci, L., Bonelli, N., Bonola, M., Procissi, G., Cascone, C., Sanvito, D., Pontarelli, S., Bianchi, G., Bifulco, R.: Towards a stateful forwarding abstraction to implement scalable network functions in software and hardware. ArXiv e-prints (2016)
[66] PF: the OpenBSD packet filter. http://www.openbsd.org/faq/pf/
[67] Pfaff, B., Heller, B., Talayco, D., Erickson, D., Gibb, G., Appenzeller, G., Tourrilhes, J., Pettit, J., Yap, K., Casado, M., Kobayashi, M., McKeown, N., Balland, P., Price, R., Sherwood, R., Yiakoumis, Y.: OpenFlow switch specification v1.0.0 (2009). http://archive.openflow.org/documents/openflow-spec-v1.0.0.pdf
[68] Postel, J.: Internet protocol. RFC 791 (INTERNET STANDARD) (1981). Updated by RFCs 1349, 2474, 6864
[69] Pozo, S., Ceballos, R., Gasca, R.M.: CSP-based firewall rule set diagnosis using security policies. In: 2nd International Conference on Availability, Reliability and Security (ARES), pp. 723-729. IEEE, Los Alamitos (2007). https://doi.org/10.1109/ARES.2007.63
[70] Pozo, S; Ceballos, R; Gasca, RM, Model-based development of firewall rule sets: diagnosing model inconsistencies, Inf. Softw. Technol., 51, 894-915, (2009) · doi:10.1016/j.infsof.2008.05.001
[71] Renard, B.: cisco-acl-to-iptables (2013). http://git.zionetrix.net/?a=summary&p=cisco-acl-to-iptables. Retrieved Sept 2014
[72] Reynolds, J.: Assigned numbers: RFC 1700 is replaced by an on-line database. RFC 3232 (Informational) (2002)
[73] Reynolds, J., Postel, J.: Assigned numbers. RFC 1700 (Historic) (1994). Obsoleted by RFC 3232
[74] Sherry, J; Hasan, S; Scott, C; Krishnamurthy, A; Ratnasamy, S; Sekar, V, Making middleboxes someone elses problem: network processing as a cloud service, ACM SIGCOMM Comput. Commun. Rev., 42, 13-24, (2012) · doi:10.1145/2377677.2377680
[75] Sluizer, S., Postel, J.: Mail transfer protocol. RFC 780 (1981). Obsoleted by RFC 788
[76] Smolka, S., Eliopoulos, S.A., Foster, N., Guha, A.: A fast compiler for NetKAT. In: International Conference on Functional Programming (ICFP), pp. 328-341. ACM (2015). https://doi.org/10.1145/2784731.2784761 · Zbl 1360.68352
[77] Tantau, T., Feuersaenger, C.: The TikZ and pgf packages (2016). Pgfversion 3.0.1a
[78] The netfilter.org project: netfilter/iptables project. http://www.netfilter.org/
[79] The netfilter.org project: netfilter/nftables project. http://www.netfilter.org/
[80] Tongaonkar, A., Inamdar, N., Sekar, R.: Inferring higher level policies from firewall rules. In: 21st USENIX Large Installation System Administration Conference (LISA), vol. 7, pp. 1-10. USENIX Association, Dallas (2007)
[81] Verizon Business RISK Team, United States Secret Service: 2010 Data Breach Investigations Report (2010). http://www.verizonenterprise.com/resources/reports/rp_2010-DBIR-combined-reports_en_xg.pdf
[82] Wool, A, A quantitative study of firewall configuration errors, IEEE Comput., 37, 62-67, (2004) · doi:10.1109/MC.2004.2
[83] Wool, A, The use and usability of direction-based filtering in firewalls, Comput. Secur., 23, 459-468, (2004) · doi:10.1016/j.cose.2004.02.003
[84] Wool, A, Trends in firewall configuration errors: measuring the holes in swiss cheese, IEEE Internet Comput., 14, 58-65, (2010) · doi:10.1109/MIC.2010.29
[85] Yuan, L., Chen, H., Mai, J., Chuah, C.N., Su, Z., Mohapatra, P.: FIREMAN: a toolkit for firewall modeling and analysis. In: IEEE Symposium on Security and Privacy, pp. 199-213 (2006)
[86] Zhang, B., Al-Shaer, E., Jagadeesan, R., Riely, J., Pitcher, C.: Specifications of a high-level conflict-free firewall policy language for multi-domain networks. In: 12th ACM Symposium on Access Control Models and Technologies, SACMAT’07, pp. 185-194. ACM (2007). https://doi.org/10.1145/1266840.1266871
[87] Zhang, S., Mahmoud, A., Malik, S., Narain, S.: Verification and synthesis of firewalls using SAT and QBF. In: Network Protocols (ICNP), pp. 1-6 (2012). https://doi.org/10.1109/ICNP.2012.6459944
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.