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.

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.

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.

This paper presents a system prototype to help elder persons being aware of changes in terrain ahead of them. Ultrasonic signal is used for the detection of terrain changes because of its stability in air transmission speed and its simplicity and cost in hardware designs. The prototype is designed and built using commercial-off-the-shelf (COTS) components with an 8051 microprocessor. It can detect obstacles of heights no more than 10 cm three steps away.