This work is on formal modeling, analysis and detection of job interference in large distributed multi-agent systems. Such an analysis usually requires an examination of all the global system states-often impossible due to the well-known state space explosion. We obtain a sufficient condition so that job interference can be detected by observations of individual system component without the knowledge of global system states. Given that the job interference can be detected locally, we propose a guided random walk algorithm for detecting interference. We apply it to Kansei, a large and distributed wireless sensor network system with multi-agents. Ten job interference traces are identified; they have not been detected before by manual analysis and system operations. We further diagnose the detected interference for a correction of system design.

Botmaster sets up Command and Control (C&C) server and stepping-stones in the Internet for stealing sensitive information from victim's machine. Clouds provide botmaster with an ideal environment of rich computing resources where he can easily deploy/remove C&C server and establish/tear-down stepping-stones for anonymous attacks. It is of vital importance for cloud service providers to detect botnet, prevent attack, and trace back to the botmaster. We present our Pebble trace scheme for the trace back to the botmaster. It first identifies cryptographic keys of the botnet communications for configuring botnet operations and then traces back to the botmaster. We design and implement a new key identification scheme and propose an approach for tracing back to the botmaster across stepping-stones and beyond multiple clouds without universal deployment of monitors, router updates, or ISP support. We implement our method and build a Pebble-trace prototype that is applied to Zeus botnet in OpSource cloud with promising results.

In 2009 UnrealIRCd 3.2.8.1, an IRC (Internet Relay Chat) server, was replaced by a version with a backdoor at its mirror sites. It was not detected until seven months later and it had caused irrevocable damages in IRC services. It is of vital importance and also a challenge to detect implanted malicious code in newly developed systems before their deployment. We apply machine learning to uncover a system implementation structure that includes its normal functions from the design, as well as the hidden malicious behaviors. Published works with machine learning often assume that systems are completely specified. Unfortunately, practical system implementations are usually incompletely specified and the prevalent algorithms do not apply. We design generalized and efficient machine learning algorithms for incompletely specified protocol system implementations for detecting implanted malicious code. We further extend the results where machine learning starts from an approximate model instead of an empty conjecture - a usual approach of machine learning algorithms, and our approach learns an implementation structure more efficiently than the known algorithms. We implement and apply our method to two case studies: an IRC server with backdoor and an MSN client with message flooder. Experiments show that our procedures successfully and efficiently detect the implanted malicious behaviors.

As computer networks turn into an indispensable part of technology and entertainment of human life today, security and reliability become the forefront issue of network protocol design and implementation. Any security or reliability flaws in network protocol operation can lead to great loss in private data, business opportunity and reputation. As a result, methods and tools for preventing and detecting such security breach in network protocol design and implementation are urgently needed. Formal methods have proven to be successful in system verification and testing. This thesis is devoted to formally design algorithm and tools to efficiently and effectively investigate security of both protocol specification and implementation.For protocol specification, we first model a protocol as a state machine. To verify certain security property against the state machine, we need to explore all reachable states in the state machine. However, traditional reachability problem suffers from the classic state space explosion problem. We propose two techniques to tackle this problem: trace inclusion transformation and online minimization. We first transform the original state machine to a simplified machine which is a trace inclusion transformation of the original machine by removing certain system parameters. We apply online minimization to construct a minimal reachable graph of manageable size that is bisimulation equivalent to the reachability graph of the simplified machine. Then we can verify the desired security property against the minimal reachable graph. However, we may introduce false positive and false negative since we have simplified the original machine. In the second phase of analysis, we show that there is no false negative if the simplified machine is a trace inclusion transformation of the original machine. We also design algorithm to eliminate false positive. Then we can conclude if the state machine (the protocol design) is security against the checked security property.However, even with perfect design, fault can still be introduced during the implementation and integration phase. Due to the black-box nature of protocol implementation and often unavailability of specification, traditional verification techniques do not apply here. In this thesis, we first automatically synthesize a formal model to represent the behavior of the implementation and then use the synthesized model to assist different security flaw detection applications. We study both active and passive synthesize approaches and compare their advantages and disadvantages. We incorporate the formal model to two different security flaw detection applications. In the first application, we build a model based fuzz testing framework in which the formal model is used to guide test input selection and served as test coverage criteria. Our framework significantly improves existing black-box protocol security testing techniques. In the second application, we examine the synthesized model to determine if there is any malicious function hidden inside a protocol implementation and determine the behavior of the hidden function.We show the proposed approaches are effective with extensive case studies for various scenarios and applications. Nevertheless, the techniques and framework proposed in this thesis is generic and could be easily adapted for different problem domains and applications.

As content providers adopt peer-to-peer approaches for content sharing and distribution, they face new challenges in guaranteeing privacy to their clients. Participating peers can glean information from their communication with other peers, such as their identities or the shared data and use this information for malicious purposes. We present Nemor, a protocol that allows a requesting peer and a corresponding serving peer to communicate anonymously with each other and from other participating peers, while protecting the identity of the content being exchanged. Nemor relies on a trusted intermediary, such as a provider-managed tracker, to identify a potential serving peer. A peer in Nemor joins one or more trees. Using a combination of a random walk, a probabilistic jump from one tree to another and constrained flooding, the requesting and serving peer dynamically construct an overlay path between them. A key differentiator of Nemor is the integrated design of a congestion avoidance mechanism that yields significant performance benefits without compromising on anonymity. Using experimental results from PlanetLab and simulations with traces from an operational VoD system, we demonstrate that Nemor outperforms state of the art approaches like TOR and OneSwarm. Our results confirm that Nemor, while being resilient to attacks on anonymity, achieves high performance and scalability and is suitable for a range of applications, including distribution of large volume content, such as streaming video.

Network protocol fingerprinting refers to the process of identifying a protocol implementation by their input and output behaviors. It has been regarded as both a potential threat to network security and also as a useful mechanism for network management. Existing protocol fingerprinting tools share common disadvantages such as being protocol-specific and difficult to automate. This paper proposes a formal methodology for fingerprinting experiments using which we can model a broad spectrum of fingerprinting problems and design-efficient algorithms. We present a formal behavioral model that specifies a protocol principal by its states and transitions, then identify a complete taxonomy of fingerprint matching and discovery problems is identified based on 1) whether the fingerprinting experiment is active or passive and 2) the information available about the specifications and implementations. Algorithms to solve the problems are discussed. In particular, for fingerprint matching algorithm, we propose an efficient PEFSM online separation algorithm for active experiment and concurrent passive testing for passive experiments. For fingerprint discovery problem, there are two cases: if the protocol specification is available as a nondeterministic PEFSM, we apply across verification and back-tracing technique for active and passive discovery, respectively; if no specification is available, we take the machine learning approach and discover the fingerprint by active testing.

“Inroduction” contains an introduction to IM system and its security threats along with a survey of various defense methods. “Instant Messaging Spam: SPIM” is on IM spam filtering. “Instant Messaging Worm” presents a mathematical model and analysis of IM worm along with its defense mechanisms.

A major hurdle of formal analysis of protocol security properties is the well-known state explosion - a protocol system usually contains infinitely many or a formidable number of states. As a result, most of the analysis resorts to heuristics, such as state space pruning. Given the temporal property of authentication and authorization protocols, we introduce trace inclusion transformation of protocol specification to reduce significantly the state space. We further cut down the number of states by online minimization for obtaining a model of a manageable size for a formal and rigorous analysis. However, the two state space reduction procedures may result in false negative and false positives. We show that our trace inclusion transformation and online minimization do not introduce any false negative. On the other hand, we design an efficient algorithm for ruling out all the possible false positives. Therefore, our analysis is sound and complete. For a case study, we analyze OAuth, a standardization of API authentication protocols. Our automated analysis identifies a number of attacks in the original specification, including the one that has been detected. We also analyze the second version of OAuth and prove it is secure if the API interface is secure.

The use of peer-to-peer (P2P) mechanisms for content delivery is attractive to content and service providers alike. P2P data transfers offload the demand on servers and reduce the bandwidth requirements, with corresponding benefits of improved scalability and performance. This, however, poses interesting challenges in ensuring content integrity. Peers may be malicious and attempt to send corrupt and/or inappropriate content to disrupt the service. Consequently, service providers must provide clients with the capability to validate the integrity of content delivered from peers. This goal is particularly challenging in the context of streaming video because the content needs to be validated in real time. A practical solution must provide high integrity assurance while incurring low communication and computation overhead. In this paper, we present a packet-based validation approach for ensuring the integrity of data obtained from peers. Our proposed scheme randomly selects packets and validates their correctness. Through detailed experiments, we show that this mechanism is not only lightweight but is also able to detect content corruption with very high probability, thus protecting the viewing experience and the provider's content delivery service.

Security, reliability and interoperability are indispensable in today's distributed heterogeneous information infrastructure. For government and military applications, it is crucial to conduct effective and efficient testing of security properties for newly developed systems, which are to be integrated into existing information system. Yet little progress has been made in the technology advancement of rigorous and automated security testing. In this contribution we present virtual cyber security testing capability (VCSTC) - a DoD funded project-for developing an automated testing capability that can assess the operational functions and security impact of a target system without physically integrating it into an intended network infrastructure. VCSTC first synthesizes a model to emulate the real network infrastructure; then it automatically generates and executes test cases with guaranteed coverage of the features and security properties under test. This report presents the architecture of VCSTC, its key techniques and experimental results on real systems.

Network security devices are becoming more sophisticated and so are the testing processes. Traditional network testbeds face challenges in terms of fidelity, scalability and complexity of security features. In this paper we propose a new methodology of testing security devices using network virtualization techniques, and present an integrated solution, including network emulation, test case specification and automated test execution. Our hybrid network emulation scheme provides high fidelity by host virtualization and scalability by lightweight protocol stack emulation. We also develop an intermediate level test case description language that is suitable for security tests at various network protocol layers and that can be executed automatically on the emulated network. The methodology presented in this paper has been implemented and integrated into a security infrastructure testing system for US Department of Defense and we report the experimental results.

A lot of efforts have been devoted to the analysis of network protocol specification for reliability and security properties using formal techniques. However, faults can also be introduced during system implementation; it is indispensable to detect protocol implementation flaws, yet due to the black-box nature of protocol implementation and the unavailability of protocol specification most of the approaches resort to random or manual testing. In this paper we propose a model-based approach for security flaw detection of protocol implementation with a high fault coverage, measurability, and automation. Our approach first synthesizes an abstract behavioral model from a protocol implementation and then uses it to guide the testing process for detecting security and reliability flaws. For protocol specification synthesis we reduce the problem a trace minimization with a finite state machine model and an efficient algorithm is presented for state space reduction. Our method is implemented and applied to real network protocols. Guided by the synthesized model our testing tool reveals a number of unknown reliability and security issues by automatically crashing the implementations of the Microsoft MSN instant messaging (MSNIM) protocol. Analytical comparison between our model-based and prevalent syntax-based flaw detection schemes is also provided with the support of experimental results.