Automated repair by example for firewalls
- PDF / 1,101,441 Bytes
- 27 Pages / 439.37 x 666.142 pts Page_size
- 8 Downloads / 203 Views
Automated repair by example for firewalls William T. Hallahan1 · Ennan Zhai1,2 · Ruzica Piskac1
© Springer Science+Business Media, LLC, part of Springer Nature 2020
Abstract Firewalls are widely deployed to manage enterprise networks. Because enterprise-scale firewalls contain hundreds or thousands of rules, ensuring the correctness of firewalls—that the rules in the firewalls meet the specifications of their administrators—is an important but challenging problem. Although existing firewall diagnosis and verification techniques can identify potentially faulty rules, they offer administrators little or no help with automatically fixing faulty rules. This paper presents FireMason, the first effort that offers automated repair by example for firewalls. Once an administrator observes undesired behavior in a firewall, she may provide input/output examples that comply with the intended behaviors. Based on the examples, FireMason automatically synthesizes new firewall rules for the existing firewall. This new firewall correctly handles packets specified by the examples, while maintaining the rest of the behaviors of the original firewall. Through a conversion of the firewalls to SMT formulas, we offer formal guarantees that the change is correct. Our evaluation results from real-world case studies show that FireMason can efficiently find repairs. Keywords Synthesis · Firewall repair · Programming by example · Network configuration
1 Introduction Firewalls play an important role in today’s individual and enterprise-scale networks. A typical firewall is responsible for managing all incoming and outgoing traffic between an internal network and the rest of the Internet by accepting, forwarding, or dropping packets based on a set of rules specified by its administrators. Because of the central role firewalls play in
This research was supported in part by the NSF under Grants CCF-1302327, CCF-1553168 and CCF-1715387.
B
Ruzica Piskac [email protected] William T. Hallahan [email protected] Ennan Zhai [email protected]
1
Computer Science Department, Yale University, New Haven, CT 06511, USA
2
Present Address: Alibaba Group, Seattle, USA
123
Formal Methods in System Design
networks, small changes can propagate unintended consequences throughout the networks. This is especially true in increasingly large and complex enterprise networks. A single line in a firewall could, for example, allow anyone to access production services, and therefore it is critical to ensure the correctness of firewall rules. Broadly speaking, a firewall is correct if the rules of that firewall meet the specification of its administrator. There have been many efforts that aim to check the correctness of firewall rules through techniques such as firewall analysis [1,2], verification [3], and root-cause troubleshooting [4–6]. For instance, systems like Margrave [4] and Fang [1] build an event tree recording states of an observed error, and backtrack through it to find the root causes. While existing tools can identify the cau
Data Loading...
