Logo image
Back
Analyzing Operational Behavior of Stateful Protocol Implementations for Detecting Semantic Bugs
Conference proceeding

Analyzing Operational Behavior of Stateful Protocol Implementations for Detecting Semantic Bugs

Endadul Hoque, Omar Chowdhury, Sze Yiu Chau, Cristina Nita-Rotaru and Ninghui Li
2017 47th Annual IEEE/IFIP International Conference on Dependable Systems and Networks (DSN), pp.627-638
06/2017
DOI: 10.1109/DSN.2017.36

View Online

Abstract

Network protocol implementations must comply with their specifications that include properties describing the correct operational behavior of the protocol in response to different temporal orderings of network events. Due to inconsistent interpretations of the specification, developers can unknowingly introduce semantic bugs, which cause the implementations to violate the respective properties. Detecting such bugs in stateful protocols becomes significantly difficult as their operations depend on their internal state machines and the complex interactions between the protocol logic. In this paper, we present an automated tool to help developers analyze their protocol implementations and detect semantic bugs violating the temporal properties of the protocols. Given an implementation, our tool (1) extracts the implemented finite state machine (FSM) of the protocol from the source code by symbolically exploring the code and (2) determines whether the extracted FSM violates given temporal properties by using an off-the-shelf model checker. We demonstrated the efficacy of our tool by applying it on 6 protocol implementations. We detected 11 semantic bugs (2 with security implications) when we analyzed these implementations against properties obtained from their publicly available specifications.
 Computer bugs Model checking Protocols Security Semantics Servers Tools

Details

Metrics

19 Record Views
22 Times Cited - Web of Science
Logo image