Rule-Based Verification of Network Protocol Implementations Using Symbolic Execution

JaeSeung Song, Tiejun Ma, Cristian Cadar, Peter Pietzuch

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

Abstract

The secure and correct implementation of network protocols for resource discovery, device configuration and network management is complex and error-prone. Protocol specifications contain ambiguities, leading to implementation flaws and security vulnerabilities in network daemons. Such problems are hard to detect because they are often triggered by complex sequences of packets that occur only after prolonged operation. The goal of this work is to find semantic bugs in network daemons. Our approach is to replay a set of input packets that result in high source code coverage of the daemon and observe potential violations of rules derived from the protocol specification. We describe SYMNV, a practical verification tool that first symbolically executes a network daemon to generate high coverage input packets and then checks a set of rules constraining permitted input and output packets. We have applied SYMNV to three different implementations of the Zeroconf protocol and show that it is able to discover non-trivial bugs.
Original languageEnglish
Title of host publication2011 Proceedings of 20th International Conference on Computer Communications and Networks (ICCCN)
PublisherIEEE
Pages1-8
Number of pages8
ISBN (Electronic)978-1-4577-0638-7
ISBN (Print)978-1-4577-0637-0
DOIs
Publication statusPublished - 1 Jul 2011
Event20th International Conference on Computer Communications and Network - Maui, United States
Duration: 31 Jul 20114 Aug 2011
http://www.icccn.org/icccn11/cfp.html

Publication series

Name
PublisherIEEE
ISSN (Print)1095-2055

Conference

Conference20th International Conference on Computer Communications and Network
Abbreviated titleICCCN 2011
Country/TerritoryUnited States
CityMaui
Period31/07/114/08/11
Internet address

Fingerprint

Dive into the research topics of 'Rule-Based Verification of Network Protocol Implementations Using Symbolic Execution'. Together they form a unique fingerprint.

Cite this