Formal methods and tools for testing communication protocol system security

Communication protocol is the cornerstone of today's network and distributed computing system. The correct functioning of a protocol relies on both a flawless specification and a correct implementation. While prevalent work focuses on validating the soundness of specification, implementations are inherently more complicated and might introduce discrepancy and very likely vulnerabilities. Hence, study on theory and practice of protocol testing is of significant importance. Furthermore, with the increasing consideration for properties such as security, privacy and robustness of protocol systems, the role of protocol testing goes beyond the traditional notion of checking conformance of an implementation. Existing solutions for testing security features rely largely on expert insights of protocols and manual efforts, and could hardly be generalized or automated.;Formal methods have proven to be promising toward developing automated and generic protocol verification and testing methods. This thesis studies a model based formal approach for testing security related properties for communication protocol systems. The first part of the work introduces a new formal protocol model--Symbolic Parameterized Extended Finite State Machine (SP-EFSM). SP-EFSM model augments the traditional communicating EFSM model with (1) a symbolic protocol message language; and (2) parameterized input and output symbols in order to cope with the rich semantics of modern protocol with cryptographic primitives. A protocol is specified by a set of SP-EFSM (each is called a component) interacting with each other through sending and receiving messages. Various properties--both functional and non-functional--and verification problems could be specified using this formal model.;The power of the proposed methodology is demonstrated by its application to several newly emerging and interesting research problems related to network protocol security and reliability. The second part of this thesis shows that the formal modeling techniques can contribute to solutions that are fundamentally more general and automatic than existing ones. We first study the problem of black box testing of message confidentiality--an important security property under Dolev-Yao attacker model. While it is well known that for validation problem could be reduced to a reachability problem in the composed SP-EFSM model, testing this property faces a major challenge that the specification may not be available or comprehensive to cover all implementation details. For this reason it is hard apply classic conformance testing approaches. To overcome this difficulty a supervised learning based approach is used to discover the internal structure of black-box implementations by active testing and to validate the confidentiality property on-the-fly.;The same formal modeling methodology is also applied to solve the problem of black-box protocol fingerprinting. Protocol fingerprinting refers to the process of distinguishing between different protocol implementation by their input and output behaviors, and it has been regarded as both a potential threat to cyberspace security and also as an effective mechanism for network management. SP-EFSM model is used to record the distinguishing structural aspects of an implementation by its states and transitions. A complete taxonomy of fingerprint matching and discovery problems is identified, based on (1) how much information about the candidate implementations is known; and (2) whether the fingerprinting experiment is active or passive. For fingerprint matching algorithm, we propose an 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 SP-EFSM, we apply across verification and back-tracing technique for active and passive discovery, respectively; if no specification is available, we take the learning approach described above and discover the fingerprint by active testing.;In last part of the thesis, the practicality of the proposed formal model is investigated. In the test generation module of a real world security testing system, SP-EFSM model is integrated and used to specify sophisticated features of a security device. Algorithms for manipulating the model are implemented, including particularly reachability analysis algorithm and test sequence generation algorithm. Test sequences are automatically translated into template of executable low level test cases. By providing test cases with high fault coverage and reducing significantly amount of manual effort required, we show that using formal techniques benefits network protocol testbed design in a realistic way.