Testing Security Properties of Protocol Implementations - a Machine Learning Based Approach

Security and reliability of network protocol implementations are essential for communication services. Most of the approaches for verifying security and reliability, such as formal validation and black-box testing, are limited to checking the specification or conformance of implementation. However, in practice, a protocol implementation may contain engineering details, which are not included in the system specification but may result in security flaws. We propose a new learning-based approach to systematically and automatically test protocol implementation security properties. Protocols are specified using symbolic parameterized extended finite state machine (SP-EFSM) model, and an important security property - message confidentiality under the general Dolev-Yao attacker model - is investigated. The new testing approach applies black-box checking theory and a supervised learning algorithm to explore the structure of an implementation under test while simulating the teacher with a conformance test generation scheme. We present the testing procedure, analyze its complexity, and report experimental results.