Name
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. |
Year | DOI | Venue |
|---|---|---|
2017 | 10.23919/FMCAD.2017.8102263 | 2017 Formal Methods in Computer Aided Design (FMCAD) |
Keywords | Field | DocType |
automated repair,enterprise network management,FireMason,SMT formulas,firewall rules,verification techniques,firewall diagnosis,enterprise-scale firewalls | Firewall (construction),Computer science,Computer security,Network packet,Correctness,Application firewall,Real-time computing | Conference |
Volume | Issue | ISSN |
56 | 1 | 0925-9856 |
ISBN | Citations | PageRank |
978-1-5386-1012-1 | 2 | 0.37 |
References | Authors | |
17 | 3 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| William T. Hallahan | 1 | 15 | 2.75 |
| Ennan Zhai | 2 | 100 | 19.42 |
| Ruzica Piskac | 3 | 373 | 24.47 |