TY - GEN
T1 - Analyzing Operational Behavior of Stateful Protocol Implementations for Detecting Semantic Bugs
AU - Hoque, Endadul
AU - Chowdhury, Omar
AU - Chau, Sze Yiu
AU - Nita-Rotaru, Cristina
AU - Li, Ninghui
N1 - Publisher Copyright:
© 2017 IEEE.
PY - 2017/8/30
Y1 - 2017/8/30
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=85031674074&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85031674074&partnerID=8YFLogxK
U2 - 10.1109/DSN.2017.36
DO - 10.1109/DSN.2017.36
M3 - Conference contribution
AN - SCOPUS:85031674074
T3 - Proceedings - 47th Annual IEEE/IFIP International Conference on Dependable Systems and Networks, DSN 2017
SP - 627
EP - 638
BT - Proceedings - 47th Annual IEEE/IFIP International Conference on Dependable Systems and Networks, DSN 2017
PB - Institute of Electrical and Electronics Engineers Inc.
T2 - 47th Annual IEEE/IFIP International Conference on Dependable Systems and Networks, DSN 2017
Y2 - 26 June 2017 through 29 June 2017
ER -