Analyzing Operational Behavior of Stateful Protocol Implementations for Detecting Semantic Bugs

Endadul Hoque, Omar Chowdhury, Sze Yiu Chau, Cristina Nita-Rotaru, Ninghui Li

Research output: Chapter in Book/Report/Conference proceedingConference contribution

2 Scopus citations

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.

Original languageEnglish (US)
Title of host publicationProceedings - 47th Annual IEEE/IFIP International Conference on Dependable Systems and Networks, DSN 2017
PublisherInstitute of Electrical and Electronics Engineers Inc.
Pages627-638
Number of pages12
ISBN (Electronic)9781538605417
DOIs
StatePublished - Aug 30 2017
Externally publishedYes
Event47th Annual IEEE/IFIP International Conference on Dependable Systems and Networks, DSN 2017 - Denver, United States
Duration: Jun 26 2017Jun 29 2017

Publication series

NameProceedings - 47th Annual IEEE/IFIP International Conference on Dependable Systems and Networks, DSN 2017

Conference

Conference47th Annual IEEE/IFIP International Conference on Dependable Systems and Networks, DSN 2017
CountryUnited States
CityDenver
Period6/26/176/29/17

ASJC Scopus subject areas

  • Hardware and Architecture
  • Computer Networks and Communications
  • Safety, Risk, Reliability and Quality

Fingerprint Dive into the research topics of 'Analyzing Operational Behavior of Stateful Protocol Implementations for Detecting Semantic Bugs'. Together they form a unique fingerprint.

  • Cite this

    Hoque, E., Chowdhury, O., Chau, S. Y., Nita-Rotaru, C., & Li, N. (2017). Analyzing Operational Behavior of Stateful Protocol Implementations for Detecting Semantic Bugs. In Proceedings - 47th Annual IEEE/IFIP International Conference on Dependable Systems and Networks, DSN 2017 (pp. 627-638). [8023160] (Proceedings - 47th Annual IEEE/IFIP International Conference on Dependable Systems and Networks, DSN 2017). Institute of Electrical and Electronics Engineers Inc.. https://doi.org/10.1109/DSN.2017.36