A model guided security vulnerability discovery approach for network protocol implementation

Our modern society is increasingly depending on information and communication systems. This demands a high level of security and robustness on the implementations of network protocols. This paper presents a model-guided approach to discover security vulnerabilities of network protocol implementations. Our approach, resulted in security tool “Styx”, introduces mutation analysis and model checking into fuzz testing and provides a synthesized protocol security testing. And it not only can perform syntax testing on the input data validation component of protocol implementations, but also is able to model the behaviors of a protocol and automatically generate test traces for the verification of its internal implemented functions. To proof the concept, experiments with the open source implementation of IKE/ISAKMP have also been provided. The results show that Styx can effectively be used to discover security vulnerabilities from network protocol implementations.