Article

Analyzing protocol implementations for interoperability

Authors:

Ramesh Govindan,

Todd MillsteinAuthors Info & Claims

NSDI'15: Proceedings of the 12th USENIX Conference on Networked Systems Design and Implementation

Pages 485 - 498

Published: 04 May 2015 Publication History

Abstract

We propose PIC, a tool that helps developers search for non-interoperabilities in protocol implementations. We formulate this problem using intersection of the sets of messages that one protocol participant can send but another will reject as non-compliant. PIC leverages symbolic execution to characterize these sets and uses two novel techniques to scale to real-world implementations. First, it uses joint symbolic execution, in which receiver-side program analysis is constrained based on sender-side constraints, dramatically reducing the number of execution paths to consider. Second, it incorporates a search strategy that steers symbolic execution toward likely non-interoperabilities. We show that PIC is able to find multiple previously unknown noninteroperabilities in large and mature implementations of the SIP and SPDY (v2 through v3.1) protocols, some of which have since been fixed by the respective developers.

References

[1]

SPDY Protocol - Draft 3.1. http://www.chromium. org/spdy/spdy-protocol/spdy-protocol-draft3-1.

[2]

The LLVM Compiler Infrastructure Project. http://llvm.org/.

[3]

BHARGAVAN, K., OBRADOVIC, D., AND GUNTER, C. A. Formal verification of standards for distance vector routing protocols. J. ACM 49, 4 (July 2002).

Digital Library

[4]

BISHOP, S., FAIRBAIRN, M., NORRISH, M., SEWELL, P., SMITH, M., AND WANSBROUGH, K. Rigorous specification and conformance testing techniques for network protocols, as applied to TCP, UDP, and sockets. SIGCOMM '05.

Digital Library

[5]

BRUMLEY, D., CABALLERO, J., LIANG, Z., NEWSOME, J., AND SONG, D. Towards automatic discovery of deviations in binary implementations with applications to error detection and fingerprint generation. SS'07.

Digital Library

[6]

BRUMLEY, D., POOSANKAM, P., SONG, D. X., AND ZHENG, J. Automatic patch-based exploit generation is possible: Techniques and implications. In Security and Privacy (2008).

Digital Library

[7]

BUCUR, S., KINDER, J., AND CANDEA, G. Making Automated Testing of Cloud Applications an Integral Component of PaaS. In APSys 2013.

Digital Library

[8]

BUCUR, S., URECHE, V., ZAMFIR, C., AND CANDEA, G. Parallel symbolic execution for automated real-world software testing. EuroSys '11.

Digital Library

[9]

CADAR, C., DUNBAR, D., AND ENGLER, D. Klee: unassisted and automatic generation of high-coverage tests for complex systems programs. OSDI'08.

Digital Library

[10]

CADAR, C., AND ENGLER, D. R. Execution generated test cases: How to make systems code crash itself. In SPIN (2005), vol. 3639, Springer.

Digital Library

[11]

CADAR, C., TWOHEY, P., GANESH, V., AND ENGLER, D. Exe: A system for automatically generating inputs of death using symbolic execution. In CCS (2006).

[12]

FÄHNDRICH, M., REHOF, J., AND DAS, M. Scalable context-sensitive flow analysis using instantiation constraints. In PLDI 2000.

Digital Library

[13]

GE, X., TANEJA, K., XIE, T., AND TILLMANN, N. DyTa: Dynamic symbolic execution guided with static verication results. In ICSE 2011, Demonstration.

Digital Library

[14]

GODEFROID, P. Compositional dynamic test generation. POPL '07.

Digital Library

[15]

GODEFROID, P., KLARLUND, N., AND SEN, K. DART: directed automated random testing. In PLDI (2005).

Digital Library

[16]

GODEFROID, P., LEVIN, M. Y., AND MOLNAR, D. Automated whitebox fuzz testing. In NDSS 2008.

[17]

GUNASINGHE, H. SCIM interop event at IETF 83rd meeting. http://hasini-gunasinghe.blogspot.com/2012/03/scim-interop-event-at-ietf-83rd-meeting.html, Mar. 2012.

[18]

HALEPLIDIS, E., OGAWA, K., WANG, W., AND SALIM, J. H. Implementation report for forwarding and control element separation (ForCES). RFC 6053 http://tools.ietf.org/html/rfc6053, Nov. 2010.

[19]

Information processing systems - Open Systems Interconnection - LOTOS - A formal description technique based on the temporal ordering of observational behaviour, 1989.

[20]

KILLIAN, C., ANDERSON, J. W., JHALA, R., AND VAHDAT, A. Life, death, and the critical transition: finding liveness bugs in systems code. NSDI'07.

Digital Library

[21]

KILLIAN, C. E., ANDERSON, J. W., BRAUD, R., JHALA, R., AND VAHDAT, A. M. Mace: language support for building distributed systems. PLDI '07.

Digital Library

[22]

KING, J. C. Symbolic execution and program testing. CACM 19, 7 (1976).

Digital Library

[23]

KOTHARI, N., MAHAJAN, R., MILLSTEIN, T., GOVINDAN, R., AND MUSUVATHI, M. Finding Protocol Manipulation Attacks. In SNAP (August 2011).

Digital Library

[24]

KUZNETSOV, V., KINDER, J., BUCUR, S., AND CANDEA, G. Efficient state merging in symbolic execution. In PLDI 2012.

Digital Library

[25]

KUZNIAR, M., PERESINI, P., CANINI, M., VENZANO, D., AND KOSTIC, D. A SOFT way for OpenFlow switch interoperability testing. In CoNEXT (2012).

Digital Library

[26]

LABOVITZ, C., AHUJA, A., ABOSE, A., AND JAHANIAN, F. An Experimental Study of Delayed Internet Routing Convergence. In SIGCOMM 2000.

[27]

LEE, H., SEIBERT, J., KILLIAN, C., AND NITAROTARU, C. Gatling: Automatic attack discovery in large-scale distributed systems. NDSS 2012.

[28]

MA, K.-K., KHOO, Y. P., FOSTER, J. S., AND HICKS, M. Directed symbolic execution. In SAS (September 2011), vol. 6887 of Lecture Notes in Computer Science.

Digital Library

[29]

MAJUMDAR, R., AND XU, R.-G. Directed test generation using symbolic grammars. ASE '07.

Digital Library

[30]

MASINTER, L. WebDAV interop report. http://www.webdav.org/users/masinter/interop/report. html, July 1999.

[31]

MOME interoperability testing event. http://www. ist-mome.org/events/interop/, July 2005.

[32]

MUSUVATHI, M., AND ENGLER, D. R. Model checking large network protocol implementations. NSDI'04.

Digital Library

[33]

MUSUVATHI, M., PARK, D. Y. W., CHOU, A., ENGLER, D. R., AND DILL, D. L. Cmc: a pragmatic approach to model checking real code. SIGOPS Oper. Syst. Rev. 36, SI (Dec. 2002).

Digital Library

[34]

PERSON, S., YANG, G., RUNGTA, N., AND KHURSHID, S. Directed incremental symbolic execution. In PLDI 2011.

Digital Library

[35]

RAO, A., AND SCHULZRINNE, H. Real-world SIP interoperability: Still an elusive quest. http://www.sipforum.org/component/option,com_ docman/task,doc_view/gid,124/, 2007.

[36]

RCS VoLTE interoperability event 2012. http://www.msforum.org/interoperability/RCSVoLTE. shtml, Oct. 2012.

[37]

REHOF, J., AND FÄHNDRICH, M. Type-base flow analysis: from polymorphic subtyping to cfl-reachability. In POPL 2001.

Digital Library

[38]

REPS, T. W. Program analysis via graph reachability. In International Symposium on Logic Programming.

Digital Library

[39]

ROSENBERG, J. Basic level of interoperability for session initiation protocol (SIP) services (BLISS) problem statement. Internet draft http://tools.ietf. org/html/draft-ietf-bliss-problem-statement-04, Mar. 2009.

[40]

ROSENBERG, J., SCHULZRINNE, H., CAMARILLO, G., JOHNSTON, A., PETERSON, J., SPARKS, R., HANDLEY, M., AND SCHOOLER, E. SIP: Session Initiation Protocol. RFC 3261, June 2002.

Digital Library

[41]

RUSSELL, S. J., AND NORVIG, P. Artificial Intelligence - A Modern Approach (Third Edition). Pearson Education, 2010.

Digital Library

[42]

TSUJIKAWA, T. Spdylay - SPDY C Library. http://spdylay.sourceforge.net/.

[43]

YABANDEH, M., KNEZEVIC, N., KOSTIC, D., AND KUNCAK, V. Crystalball: Predicting and preventing inconsistencies in deployed distributed systems. NSDI '09.

Digital Library

[44]

ZAMFIR, C., AND CANDEA, G. Execution synthesis: A technique for automated software debugging. In EuroSys 2010.

Digital Library

Cited By

Zhang ZZhang QNguyen BSingapuram SMao ZMahlke SHamlen KLu L(2020)Automatic Feature Isolation in Network Protocol Software ImplementationsProceedings of the 2020 ACM Workshop on Forming an Ecosystem Around Software Transformation10.1145/3411502.3418425(29-34)Online publication date: 13-Nov-2020
https://dl.acm.org/doi/10.1145/3411502.3418425
Iyer RPedrosa LZaostrovnykh APirelli SArgyraki KCandea GLorch JYu M(2019)Performance contracts for software network functionsProceedings of the 16th USENIX Conference on Networked Systems Design and Implementation10.5555/3323234.3323277(517-530)Online publication date: 26-Feb-2019
https://dl.acm.org/doi/10.5555/3323234.3323277
Lin ZMoon SZarate CMulagalapalli RKulandaivel SFanti GSekar V(2019)Towards Oblivious Network Analysis using Generative Adversarial NetworksProceedings of the 18th ACM Workshop on Hot Topics in Networks10.1145/3365609.3365854(43-51)Online publication date: 13-Nov-2019
https://dl.acm.org/doi/10.1145/3365609.3365854
Show More Cited By

Analyzing protocol implementations for interoperability
1. Software and its engineering
  1. Software creation and management
    1. Software verification and validation
      1. Software defect analysis

Recommendations

Analysing Protocol Implementations
ISPEC '09: Proceedings of the 5th International Conference on Information Security Practice and Experience

Many protocols running over the Internet are neither formalised, nor formally analysed. The amount of documentation for tele- communication protocols used in real-life applications is huge, while the available analysis methods and tools require precise ...
Symbolic execution of security protocol implementations: handling cryptographic primitives
WOOT'18: Proceedings of the 12th USENIX Conference on Offensive Technologies

We show how to efficiently simulate cryptographic primitives during symbolic execution. This allows analysis of security protocol implementations, and revealed several flaws in implementations of WPA2's 4-way handshake.

Traditional symbolic execution ...
Automated Security Verification for Crypto Protocol Implementations: Verifying the Jessie Project

An important missing link in the construction of secure systems is finding a practical way to establish a correspondence between a software specification and its implementation. We address this problem for the case of crypto-based Java implementations (...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings

NSDI'15: Proceedings of the 12th USENIX Conference on Networked Systems Design and Implementation

May 2015

620 pages

ISBN:9781931971218

Program Chairs:
Paul Barham
Google
,
Arvind Krishnamurthy
University of Washington

Sponsors

VMware
NSF: National Science Foundation
Google Inc.
Microsoft Reasearch: Microsoft Reasearch
CISCO

Publisher

USENIX Association

United States

Publication History

Published: 04 May 2015

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

11
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 14 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Zhang ZZhang QNguyen BSingapuram SMao ZMahlke SHamlen KLu L(2020)Automatic Feature Isolation in Network Protocol Software ImplementationsProceedings of the 2020 ACM Workshop on Forming an Ecosystem Around Software Transformation10.1145/3411502.3418425(29-34)Online publication date: 13-Nov-2020
https://dl.acm.org/doi/10.1145/3411502.3418425
Iyer RPedrosa LZaostrovnykh APirelli SArgyraki KCandea GLorch JYu M(2019)Performance contracts for software network functionsProceedings of the 16th USENIX Conference on Networked Systems Design and Implementation10.5555/3323234.3323277(517-530)Online publication date: 26-Feb-2019
https://dl.acm.org/doi/10.5555/3323234.3323277
Lin ZMoon SZarate CMulagalapalli RKulandaivel SFanti GSekar V(2019)Towards Oblivious Network Analysis using Generative Adversarial NetworksProceedings of the 18th ACM Workshop on Hot Topics in Networks10.1145/3365609.3365854(43-51)Online publication date: 13-Nov-2019
https://dl.acm.org/doi/10.1145/3365609.3365854
McMillan KZuck LWu JHall W(2019)Formal specification and testing of QUICProceedings of the ACM Special Interest Group on Data Communication10.1145/3341302.3342087(227-240)Online publication date: 19-Aug-2019
https://dl.acm.org/doi/10.1145/3341302.3342087
Ahmadi RDingel JDumas MPfahl DApel SRusso A(2019)Concolic testing for models of state-based systemsProceedings of the 2019 27th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering10.1145/3338906.3338908(4-15)Online publication date: 12-Aug-2019
https://dl.acm.org/doi/10.1145/3338906.3338908
Rath FSchemmel DWehrle K(2018)Interoperability-Guided Testing of QUIC Implementations using Symbolic ExecutionProceedings of the Workshop on the Evolution, Performance, and Interoperability of QUIC10.1145/3284850.3284853(15-21)Online publication date: 4-Dec-2018
https://dl.acm.org/doi/10.1145/3284850.3284853
Pedrosa LIyer RZaostrovnykh AFietz JArgyraki KGorinsky STapolcai J(2018)Automated synthesis of adversarial workloads for network functionsProceedings of the 2018 Conference of the ACM Special Interest Group on Data Communication10.1145/3230543.3230573(372-385)Online publication date: 7-Aug-2018
https://dl.acm.org/doi/10.1145/3230543.3230573
Hong DChen QMao ZKim TWang CKim TWu D(2017)An Initial Investigation of Protocol CustomizationProceedings of the 2017 Workshop on Forming an Ecosystem Around Software Transformation10.1145/3141235.3141236(57-64)Online publication date: 3-Nov-2017
https://dl.acm.org/doi/10.1145/3141235.3141236
Sun WXu LElbaum SBultan TSen K(2017)Improving the cost-effectiveness of symbolic testing techniques for transport protocol implementations under packet dynamicsProceedings of the 26th ACM SIGSOFT International Symposium on Software Testing and Analysis10.1145/3092703.3092706(79-89)Online publication date: 10-Jul-2017
https://dl.acm.org/doi/10.1145/3092703.3092706
Kim JChoi HNamkung HChoi WChoi BHong HKim YLee JHan DMarkopoulou AFaloutsos MSekar VKostic D(2016)Enabling Automatic Protocol Behavior Analysis for Android ApplicationsProceedings of the 12th International on Conference on emerging Networking EXperiments and Technologies10.1145/2999572.2999596(281-295)Online publication date: 6-Dec-2016
https://dl.acm.org/doi/10.1145/2999572.2999596
Show More Cited By

View Options

View options

Media

Figures

Other

Tables

View Table of Contents