<p> Firewalls, packet filters placed at the boundary of a network in order to screen incoming packets of traffic (and discard any undesirable packets), are a prominent component of network security. In this dissertation, we make several contributions to the study of firewalls.</p><p> 1. Current algorithms for verifying the correctness of firewall policies use <i>O</i>(<i>n<sup>d</sup></i>) space, where <i>n</i> is the number of rules in the firewall (several thousand) and <i>d</i> the number of fields in a rule (about five). We develop a fast probabilistic firewall verification algorithm, which runs in time and space <i>O</i>(<i>nd</i>), and determines whether a firewall <i> F</i> satisfies a property <i>P.</i> The algorithm is provably correct in several interesting cases—notably, for every instance where it states that <i>F</i> does not satisfy <i>P</i>—and the overall probability of error is extremely small, of the order of .005%. </p><p> 2. As firewalls are often security-critical systems, it may be necessary to verify the correctness of a firewall with no possibility of error, so there is still a need for a fast deterministic firewall verifier. In this dissertation, we present a deterministic firewall verification algorithm that uses only <i> O</i>(<i>nd</i>) space.</p><p> 3. In addition to correctness, optimizing firewall performance is an important issue, as slow-running firewalls can be targeted by denial-of-service attacks. We demonstrate in this dissertation that in fact, there is a strong connection between firewall verification and detection of redundant rules; an algorithm for one can be readily adapted to the other task. We suggest that our algorithms for firewall verification can be used for firewall optimization also.</p><p> 4. In order to help design correct and efficient firewalls, we suggest two metrics for firewall complexity, and demonstrate how to design firewalls as a battery of simple firewall modules rather than as a monolithic sequence of rules. We also demonstrate how to convert an existing monolithic firewall into a modular firewall. We propose that modular design can make firewalls easy to design and easy to understand.</p><p> Thus, this dissertation covers all stages in the life cycle of a firewall—design, testing and verification, and analysis—and makes contributions to the current state of the art in each of these fields.</p>
| Identifer | oai:union.ndltd.org:PROQUEST/oai:pqdtoai.proquest.com:3572873 |
| Date | 20 September 2013 |
| Creators | Bhattacharya, Hrishikesh |
| Publisher | The University of Texas at Austin |
| Source Sets | ProQuest.com |
| Language | English |
| Detected Language | English |
| Type | thesis |
Page generated in 0.0023 seconds