Thesis (M.S.)--University of Missouri--Rolla, 2007. / Vita. The entire thesis text is included in file. Title from title screen of thesis/dissertation PDF file (viewed April 11, 2007) Includes bibliographical references (p. 54-55).

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. 1. Current algorithms for verifying the correctness of firewall policies use O(n[superscrip d]) space, where n is the number of rules in the firewall (several thousand) and d the number of fields in a rule (about five). We develop a fast probabilistic firewall verification algorithm, which runs in time and space O(nd), and determines whether a firewall F satisfies a property P. The algorithm is provably correct in several interesting cases -- notably, for every instance where it states that F does not satisfy P -- and the overall probability of error is extremely small, of the order of .005%. 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 O(nd) space. 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. 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. 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. / text

Typescript. Includes bibliographical references (p. 55-60).

Remote attacks on vehicles have become alarmingly more common over the past decade. Attackers often can compromise a single Electronic Control Unit (ECU) in the In-Vehicle Network (IVN) and then use it to send malicious messages that can cause a vehicle to stop, turn, or even crash. It is critical that we find a way to block or discard these messages. However, current IVNs contain few measures to prevent such threats. Most research in this area focuses on cryptography-based approaches that are too slow or too expensive for vehicle applications. In this thesis, we explore how we can stop many of these remote attacks without cryptography. We define a `security policy' that describes what messages are allowed in an IVN and then create a system of distributed firewalls to enforce it, blocking many remote attacks. Using newer, switched IVN topologies, we can authenticate messages with nearly zero additional overhead and implement our system with minimal changes to each ECU. This places the security responsibility on a few centralized network devices that automakers can more easily control and update, even after a vehicle is sold. We evaluate our firewall design using a network simulator and find that our approach is significantly faster than state-of-the-art cryptographic approaches. / Master of Science / Over the past decade, hackers and security researchers have found many ways to remotely take control of a vehicle. Most modern vehicles contain numerous Electronic Control Units (ECUs) that each control some aspect of the vehicle, such as the brakes or engine. It is difficult to design all ECUs perfectly, however, and attackers are often able to remotely hack into one of them. From there, attackers can send malicious messages throughout the In-Vehicle Network (IVN) that connects ECUs. These messages can cause the car to stop, turn, or even crash. Thus, we must find a way to block or discard these messages. Most current research uses cryptography to accomplish this, which is a computationally expensive technique that uses math to determine if messages are legitimate. In this thesis, we examine how we can stop these malicious messages without cryptography. We introduce an approach based on firewalls, which are devices in the network that inspect messages and block them if they do not pass a set of rules. Our approach, which leverages new trends in IVN architectures, allows us to stop many of these malicious messages in the network with nearly zero additional overhead. In addition, our system of firewalls is much easier for an automaker to manage and update than previous approaches. We simulate our idea and find that it is significantly faster than previous state-of-the-art techniques.

Approved for public release; distribution is unlimited / In order to ensure the confidentially, integrity, and availability of networked resources operating on the Global Information Grid, the Department of Defense has incorporated a "Defense-in-Depth" posture. This posture includes the use of network security mechanisms and does not rely on a single defense for protection. Firewalls, Intrusion Detection Systems (IDS's), Anti-Virus (AV) software, and routers are such tools used. In recent years, computer security discussion groups have included IDS's as one of their most relevant issues. These systems help identify intruders that exploit vulnerabilities associated with operating systems, application software, and computing hardware. When IDS's are utilized on a host computer or network, there are two primary approaches to detecting and / or preventing attacks. Traditional IDS's, like most AV software, rely on known "signatures" to detect attacks. This thesis will focus on the secondary approach: Anomaly or "behavioral based" IDS's look for abnormal patterns of activity on a network to identify suspicious behavior. / Major, United States Marine Corps

The performance aspect and security capabilities of the Embedded Firewall (EFW) system are studied in this thesis. EFW is a host-based, centrally controlled firewall system consisting of network interface cards and the "Policy Server" software. A network consisting of EFW clients and a Policy Server is set up in the Advanced Network Laboratory at the Naval Postgraduate School. The Smartbits packet generator is used to simulate realistic data transfer environment. The evaluation is performed centered on two main categories: performance analysis and security capability tests. TTCP program and a script written in TCL are used to perform throughput and packet loss tests respectively. The penetration and vulnerability tests are conducted in order to analyze the security capabilities of EFW. Symantec Personal Firewall is used as a representative application firewall for comparing test results. Our study shows that EFW has better performance especially in connections with high amounts of encrypted packets and more effective in preventing insider attacks. However, current implementation of EFW has some weaknesses such as not allowing sophisticated rules that application firewalls usually do. We recommend that EFW be used as one of the protection mechanisms in a system based on the defense-in-depth concept that consists of application firewalls, intrusion detection systems and gateway protocols.

Approved for public release, distribution unlimited / The progression of technology is continuous and the technology that drives interpersonal communication is not an exception. Recent technology advancements in the areas of multicast, firewalls, encryption techniques, and bandwidth availability have made the next level of interpersonal communication possible. This thesis answers why collaborative environments are important in today's online productivity. In doing so, it gives the reader a comprehensive background in distributed collaborative environments, answers how collaborative environments are employed in the Department of Defense and industry, details the effects network security has on multicast protocols, and compares collaborative solutions with a focus on security. The thesis ends by providing a recommendation for collaborative solutions to be utilized by NPS/DoD type networks. Efficient multicast collaboration, in the framework of security is a secondary focus of this research. As such, it takes security and firewall concerns into consideration while comparing and contrasting both multicast-based and non-multicast-based collaborative solutions.

Our world teems with networked devices. Their configuration exerts an ever-expanding influence on our daily lives. Yet correctly configuring systems, networks, and access-control policies is notoriously difficult, even for trained professionals. Automated static analysis techniques provide a way to both verify a configuration's correctness and explore its implications. One such approach is scenario-finding: showing concrete scenarios that illustrate potential (mis-)behavior. Scenarios even have a benefit to users without technical expertise, as concrete examples can both trigger and improve users' intuition about their system. This thesis describes a concerted research effort toward improving scenario-finding tools for configuration analysis. We developed Margrave, a scenario-finding tool with special features designed for security policies and configurations. Margrave is not tied to any one specific policy language; rather, it provides an intermediate input language as expressive as first-order logic. This flexibility allows Margrave to reason about many different types of policy. We show Margrave in action on Cisco IOS, a common language for configuring firewalls, demonstrating that scenario-finding with Margrave is useful for debugging and validating real-world configurations. This thesis also presents a theorem showing that, for a restricted subclass of first-order logic, if a sentence is satisfiable then there must exist a satisfying scenario no larger than a computable bound. For such sentences scenario-finding is complete: one can be certain that no scenarios are missed by the analysis, provided that one checks up to the computed bound. We demonstrate that many common configurations fall into this subclass and give algorithmic tests for both sentence membership and counting. We have implemented both in Margrave. Aluminum is a tool that eliminates superfluous information in scenarios and allows users' goals to guide which scenarios are displayed. We quantitatively show that our methods of scenario-reduction and exploration are effective and quite efficient in practice. Our work on Aluminum is making its way into other scenario-finding tools. Finally, we describe FlowLog, a language for network programming that we created with analysis in mind. We show that FlowLog can express many common network programs, yet demonstrate that automated analysis and bug-finding for FlowLog are both feasible as well as complete.

As our society grows more dependent on digital systems, policies that regulate access to electronic resources are becoming more common. However, such policies are notoriously difficult to configure properly, even for trained professionals. An incorrectly written access-control policy can result in inconvenience, financial damage, or even physical danger. The difficulty is more pronounced when multiple types of policy interact with each other, such as in routers on a network. This thesis presents a policy-analysis tool called Margrave. Given a query about a set of policies, Margrave returns a complete collection of scenarios that satisfy the query. Since the query language allows multiple policies to be compared, Margrave can be used to obtain an exhaustive list of the consequences of a seemingly innocent policy change. This feature gives policy authors the benefits of formal analysis without requiring that they state any formal properties about their policies. Our query language is equivalent to order-sorted first-order logic (OSL). Therefore our scenario-finding approach is, in general, only complete up to a user-provided bound on scenario size. To mitigate this limitation, we identify a class of OSL that we call Order-Sorted Effectively Propositional Logic (OS-EPL). We give a linear-time algorithm for testing membership in OS-EPL. Sentences in this class have the Finite Model Property, and thus Margrave's results on such queries are complete without user intervention.

Comparative Analysis of Firewall Systems / Vergleichende Analyse von Firewall Systemen