{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T07:25:18Z","timestamp":1740122718260,"version":"3.37.3"},"reference-count":43,"publisher":"Springer Science and Business Media LLC","issue":"1-3","license":[{"start":{"date-parts":[[2020,9,30]],"date-time":"2020-09-30T00:00:00Z","timestamp":1601424000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2020,9,30]],"date-time":"2020-09-30T00:00:00Z","timestamp":1601424000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"funder":[{"name":"National Science Foundation","award":["CCF-1302327","CCF-1553168"],"award-info":[{"award-number":["CCF-1302327","CCF-1553168"]}]},{"name":"National Science Foundation","award":["CCF-1715387"],"award-info":[{"award-number":["CCF-1715387"]}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2020,12]]},"DOI":"10.1007\/s10703-020-00346-0","type":"journal-article","created":{"date-parts":[[2020,9,30]],"date-time":"2020-09-30T12:03:31Z","timestamp":1601467411000},"page":"127-153","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Automated repair by example for firewalls"],"prefix":"10.1007","volume":"56","author":[{"given":"William T.","family":"Hallahan","sequence":"first","affiliation":[]},{"given":"Ennan","family":"Zhai","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3267-0776","authenticated-orcid":false,"given":"Ruzica","family":"Piskac","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2020,9,30]]},"reference":[{"key":"346_CR1","unstructured":"Mayer AJ, Wool A, Ziskind E (2000) Fang: a firewall analysis engine. In: IEEE symposium on security and privacy (IEEE S&P)"},{"key":"346_CR2","unstructured":"Torlak E, Jackson D (2007) Kodkod: a relational model finder. In: 13th international conference on tools and algorithms for the construction and analysis of systems (TACAS)"},{"key":"346_CR3","unstructured":"Lopes NP, Bj\u00f8rner N, Godefroid P, Jayaraman K, Varghese G (2015) Checking beliefs in dynamic networks. In: 12th USENIX symposium on networked system design and implementation (NSDI)"},{"key":"346_CR4","unstructured":"Nelson T, Barratt C, Dougherty DJ, Fisler K, Krishnamurthi S (2010) The Margrave tool for firewall analysis. In: 24th large installation system administration conference (LISA)"},{"key":"346_CR5","unstructured":"Wool A (2001) Architecting the Lumeta firewall analyzer. In: USENIX security symposium"},{"key":"346_CR6","unstructured":"Zhang S, Mahmoud A, Malik S, Narain S (2012) Verification and synthesis of firewalls using SAT and QBF. In: 20th IEEE international conference on network protocols (ICNP)"},{"issue":"2","key":"346_CR7","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1145\/357073.357079","volume":"1","author":"G Nelson","year":"1979","unstructured":"Nelson G, Oppen DC (1979) Simplification by cooperating decision procedures. ACM Trans Program Lang Syst 1(2):245\u2013257. https:\/\/doi.org\/10.1145\/357073.357079","journal-title":"ACM Trans Program Lang Syst"},{"key":"346_CR8","unstructured":"iptables. http:\/\/ipset.netfilter.org\/iptables.man.html"},{"key":"346_CR9","doi-asserted-by":"crossref","unstructured":"Hallahan WT, Zhai E, Piskac R (2017) Automated repair by example for firewalls. In: 2017 formal methods in computer aided design (FMCAD). IEEE, pp 220\u2013229","DOI":"10.23919\/FMCAD.2017.8102263"},{"key":"346_CR10","volume-title":"Watch what I do: programming by demonstration","author":"A Cypher","year":"1993","unstructured":"Cypher A, Halbert D (1993) Watch what I do: programming by demonstration. MIT Press, Cambridge"},{"key":"346_CR11","volume-title":"Your wish is my command: programming by example","author":"H Lieberman","year":"2001","unstructured":"Lieberman H (2001) Your wish is my command: programming by example. Morgan Kaufmann, Burlington"},{"key":"346_CR12","unstructured":"Juniper: traffic policier overview. http:\/\/www.juniper.net\/documentation\/en_US\/junos12.3\/topics\/concept\/policer-overview.html"},{"key":"346_CR13","unstructured":"Cisco: policing and shaping overview. http:\/\/www.cisco.com\/c\/en\/us\/td\/docs\/ios\/12_2\/qos\/configuration\/guide\/fqos_c\/qcfpolsh.html"},{"key":"346_CR14","first-page":"197","volume-title":"ACLA: a framework for access control list (ACL) analysis and optimization","author":"J Qian","year":"2001","unstructured":"Qian J, Hinrichsa S, Nahrstedt K (2001) ACLA: a framework for access control list (ACL) analysis and optimization. Springer, New York, pp 197\u2013211"},{"key":"346_CR15","unstructured":"iptables Linux User\u2019s Manual (2015)"},{"key":"346_CR16","volume-title":"Computer networks","author":"A Tanenbaum","year":"2002","unstructured":"Tanenbaum A (2002) Computer networks, 4th edn. Prentice Hall, Upper Saddle River","edition":"4"},{"key":"346_CR17","unstructured":"Cannot block IP address. http:\/\/stackoverflow.com\/questions\/16142446\/why-cant-i-block-an-ip-address-with-iptables-on-debian-6"},{"key":"346_CR18","unstructured":"Li Z, Lu S, Myagmar S, Zhou Y (2004) Cp-Miner: a tool for finding copy-paste and related bugs in operating system code. In: 6th USENIX symposium on operating systems design and implementation (OSDI)"},{"key":"346_CR19","unstructured":"IPTables only allow localhost access. https:\/\/serverfault.com\/questions\/247176\/iptables-only-allow-localhost-access"},{"key":"346_CR20","unstructured":"IP tables allow everything but restrict HTTP for only one IP. https:\/\/goo.gl\/VTRBui"},{"key":"346_CR21","unstructured":"Is there a rule for iptables to limit the amount of SYN packets. http:\/\/askubuntu.com\/questions\/240360\/is-there-a-rule-for-iptables-to-limit-%20the-amount-of-syn-packets-a-24-range-of-i"},{"key":"346_CR22","doi-asserted-by":"crossref","unstructured":"de\u00a0Moura LM, Bj\u00f8rner N (2008) Z3: an efficient SMT solver. In: 14th tools and algorithms for the construction and analysis of systems (TACAS)","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"346_CR23","unstructured":"Server fault. http:\/\/serverfault.com\/"},{"key":"346_CR24","unstructured":"Stack overflow. http:\/\/stackoverflow.com\/"},{"key":"346_CR25","unstructured":"Good iptables starting rules for a webserver. http:\/\/serverfault.com\/questions\/118669\/good-iptables-starting-rules-for-a-webserver"},{"key":"346_CR26","unstructured":"iptables issue cannot SSH remote machines. http:\/\/askubuntu.com\/questions\/476626\/iptables-issue-cant-ssh-remote-machines"},{"key":"346_CR27","unstructured":"What is the correct way to open a range of ports in iptables. https:\/\/goo.gl\/tNXsLp"},{"key":"346_CR28","unstructured":"Block range of IP addresses. https:\/\/serverfault.com\/questions\/592061\/block-range-of-ip-addresses"},{"key":"346_CR29","unstructured":"How can I rate limit SSH connections with iptables. http:\/\/serverfault.com\/questions\/298954\/how-can-i-rate-limit-ssh-connections%20-with-iptables"},{"key":"346_CR30","unstructured":"Limiting the number of global connections per second. https:\/\/serverfault.com\/questions\/378124\/limiting-the-number-of-global-connections-per-second"},{"issue":"2","key":"346_CR31","first-page":"27","volume":"7","author":"F Chen","year":"2012","unstructured":"Chen F, Liu AX, Hwang J, Xie T (2012) First step towards automatic correction of firewall policy faults. ACM TAAS 7(2):27","journal-title":"ACM TAAS"},{"key":"346_CR32","doi-asserted-by":"crossref","unstructured":"Chen F, Liu A.X, Hwang J, Xie T (2010) First step towards automatic correction of firewall policy faults. In: Proceedings of the 24th international conference on large installation system administration. USENIX Association, pp 1\u20138","DOI":"10.1145\/2240166.2240177"},{"key":"346_CR33","doi-asserted-by":"crossref","unstructured":"Plotkin GD, Bj\u00f8rner N, Lopes NP, Rybalchenko A, Varghese G (2016) Scaling network verification using symmetry and surgery. In: 43rd ACM symposium on principles of programming languages (POPL)","DOI":"10.1145\/2837614.2837657"},{"key":"346_CR34","doi-asserted-by":"crossref","unstructured":"Yuan Y, Lin D, Alur R, Loo BT (2015) Scenario-based programming for SDN policies. In: ACM CoNEXT (CoNEXT)","DOI":"10.1145\/2716281.2836119"},{"key":"346_CR35","unstructured":"Eppstein D, Muthukrishnan S (2001) Internet packet filter management and rectangle geometry. In: 12th symposium on discrete algorithms (SODA)"},{"key":"346_CR36","unstructured":"Adiseshu H, Suri S, Parulkar GM (2000) Detecting and resolving packet filter conflicts. In: 19th IEEE international conference on computer communications (INFOCOM)"},{"issue":"3","key":"346_CR37","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1016\/S0167-4048(01)00314-5","volume":"20","author":"M Frantzen","year":"2001","unstructured":"Frantzen M, Kerschbaum F, Schultz EE, Fahmy S (2001) A framework for understanding vulnerabilities in firewalls using a dataflow model of firewall internals. Comput Secur 20(3):263\u2013270","journal-title":"Comput Secur"},{"issue":"3","key":"346_CR38","doi-asserted-by":"publisher","first-page":"214","DOI":"10.1016\/S0167-4048(03)00310-9","volume":"22","author":"S Kamara","year":"2003","unstructured":"Kamara S, Fahmy S, Schultz EE, Kerschbaum F, Frantzen M (2003) Analysis of vulnerabilities in Internet firewalls. Comput Secur 22(3):214\u2013232","journal-title":"Comput Secur"},{"key":"346_CR39","unstructured":"Yuan L, Chen H, Mai J, Chuah CN, Su Z, Mohapatra P (2006) Fireman: a toolkit for firewall modeling and analysis. In: 2006 IEEE symposium on security and privacy. IEEE, p 15"},{"issue":"6","key":"346_CR40","doi-asserted-by":"publisher","first-page":"62","DOI":"10.1109\/MC.2004.2","volume":"37","author":"A Wool","year":"2004","unstructured":"Wool A (2004) A quantitative study of firewall configuration errors. IEEE Comput 37(6):62\u201367","journal-title":"IEEE Comput"},{"key":"346_CR41","unstructured":"El-Atawy A, Ibrahim K, Hamed HH (2005) Policy segmentation for intelligent firewall testing. In: IEEE workshop on secure network protocols (NPSec)"},{"issue":"3","key":"346_CR42","doi-asserted-by":"publisher","first-page":"302","DOI":"10.1109\/JSAC.2009.090406","volume":"27","author":"E Al-Shaer","year":"2009","unstructured":"Al-Shaer E, El-Atawy A, Samak T (2009) Automated pseudo-live testing of firewall configuration enforcement. IEEE J Sel Areas Commun 27(3):302\u2013314","journal-title":"IEEE J Sel Areas Commun"},{"key":"346_CR43","doi-asserted-by":"crossref","unstructured":"Brucker AD, Br\u00fcgger L, Wolff B (2013) Hol-TestGen\/fw\u2014an environment for specification-based firewall conformance testing. In: 10th theoretical aspects of computing (ICTAC)","DOI":"10.1007\/978-3-642-39718-9_7"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-020-00346-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10703-020-00346-0\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-020-00346-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,9,30]],"date-time":"2021-09-30T00:15:19Z","timestamp":1632960919000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10703-020-00346-0"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,9,30]]},"references-count":43,"journal-issue":{"issue":"1-3","published-print":{"date-parts":[[2020,12]]}},"alternative-id":["346"],"URL":"https:\/\/doi.org\/10.1007\/s10703-020-00346-0","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"type":"print","value":"0925-9856"},{"type":"electronic","value":"1572-8102"}],"subject":[],"published":{"date-parts":[[2020,9,30]]},"assertion":[{"value":"30 September 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}