Article

Towards automatic discovery of deviations in binary implementations with applications to error detection and fingerprint generation

Authors:

Juan Caballero,

Dawn SongAuthors Info & Claims

SS'07: Proceedings of 16th USENIX Security Symposium on USENIX Security Symposium

Article No.: 15, Pages 1 - 16

Published: 06 August 2007 Publication History

Abstract

Different implementations of the same protocol specification usually contain deviations, i.e., differences in how they check and process some of their inputs. Deviations are commonly introduced as implementation errors or as different interpretations of the same specification. Automatic discovery of these deviations is important for several applications. In this paper, we focus on automatic discovery of deviations for two particular applications: error detection and fingerprint generation.

We propose a novel approach for automatically detecting deviations in the way different implementations of the same specification check and process their input. Our approach has several advantages: (1) by automatically building symbolic formulas from the implementation, our approach is precisely faithful to the implementation; (2) by solving formulas created from two different implementations of the same specification, our approach significantly reduces the number of inputs needed to find deviations; (3) our approach works on binaries directly, without access to the source code.

We have built a prototype implementation of our approach and have evaluated it using multiple implementations of two different protocols: HTTP and NTP. Our results show that our approach successfully finds deviations between different implementations, including errors in input checking, and differences in the interpretation of the specification, which can be used as fingerprints.

References

[1]

{1} The BitBlaze binary analysis platform. http:// www.cs.cmu.edu/~dbrumley/bitblaze.

[2]

{2} Bitscope. http://www.cs.cmu.edu/ ~chartwig/bitscope.

[3]

{3} IrcFuzz. http://www.digitaldwarf.be/ products/ircfuzz.c.

[4]

{4} ISIC: IP stack integrity checker. http://www. packetfactory.net/Projects/ISIC.

[5]

{5} JBroFuzz. http://www.owasp.org/index.php/Category:OWASP\_JBroFuzz.

[6]

{6} MangleMe. http://lcamtuf.coredump. cx.

[7]

{7} NetTime. http://nettime.sourceforge. net.

[8]

{8} Nmap. http://www.insecure.org.

[9]

{9} Peach. http://peachfuzz.sourceforge. net.

[10]

{10} QEMU: an open source processor emulator. http://www.qemu.org.

[11]

{11} Queso. http://ftp.cerias.purdue. edu/pub/tools/unix/scanners/queso.

[12]

{12} Spike. http://www.immunitysec.com/ resources-freesoftware.shtml.

[13]

{13} Windows NTP server. http://www.ee.udel. edu/~mills/ntp/html/build/hints/ winnt.html.

[14]

{14} Wireshark: fuzz testing tools. http://wiki. wireshark.org/FuzzTesting.

[15]

{15} Xprobe. http://www.sys-security.com.

[16]

{16} BERNERS-LEE, T., FIELDING, R., AND MASINTER, L. Uniform Resource Identifier (URI): Generic Syntax. RFC 3986 (Standard), 2005.

[17]

{17} BRUMLEY, D., HARTWIG, C., LIANG, Z., NEWSOME, J., SONG, D., AND YIN, H. Towards automatically identifying trigger-based behavior in malware using symbolic execution and binary analysis. Tech. Rep. CMU-CS-07-105, Carnegie Mellon University School of Computer Science, 2007.

[18]

{18} BRUMLEY, D., NEWSOME, J., SONG, D., W., H., AND JHA, S. Towards automatic generation of vulnerability-based signatures. In Proceedings of the 2006 IEEE Symposium on Security and Privacy (2006).

Digital Library

[19]

{19} BRUMLEY, D., WANG, H., JHA, S., AND SONG, D. Creating vulnerability signatures using weakest pre-conditions. In Proceedings of the 2007 Symposium on Computer Security Foundations Symposium (2007).

Digital Library

[20]

{20} CABALLERO, J., VENKATARAMAN, S., POOSANKAM, P., KANG, M. G., SONG, D., AND BLUM, A. Fig: Automatic fingerprint generation. In 14th Annual Network and Distributed System Security Conference (NDSS) (2007).

[21]

{21} CADAR, C., GANESH, V., PAWLOWSKI, P., DILL, D., AND ENGLER, D. EXE: A system for automatically generating inputs of death using symbolic execution. In Proceedings of the 13th ACM Conference on Computer and Communications Security (CCS) (2006).

Digital Library

[22]

{22} CHAKI, S., CLARKE, E., GROCE, A., JHA, S., AND VEITH, H. Modular verification of software components in C. In Proceedings of the 25th International Conference on Software Engineering (ICSE) (2003).

Digital Library

[23]

{23} CHEN, H., AND WAGNER, D. MOPS: an infrastructure for examining security properties of software. In Proceedings of the 9th ACM conference on Computer and Communications Security (CCS) (2002).

Digital Library

[24]

{24} COHEN, E. Programming in the 1990's. Springer-Verlag, 1990.

[25]

{25} COMER, D., AND LIN, J. C. Probing TCP implementations. In USENIX Summer 1994 (1994).

Digital Library

[26]

{26} DIJKSTRA, E. A Discipline of Programming. Prentice Hall, Englewood Cliffs, NJ, 1976.

Digital Library

[27]

{27} FIELDING, R., GETTYS, J., MOGUL, J., FRYSTYK, H., MASINTER, L., LEACH, P., AND BERNERS-LEE, T. Hypertext Transfer Protocol -- HTTP/1.1. RFC 2616 (Draft Standard), June 1999. Updated by RFC 2817.

Digital Library

[28]

{28} FLANAGAN, C., LEINO, K. R. M., LILLIBRIDGE, M., NELSON, G., SAXE, J. B., AND STATA, R. Estended static checking for Java. In ACM Conference on the Programming Language Design and Implementation (PLDI) (2002).

Digital Library

[29]

{29} FLANAGAN, C., AND SAXE, J. Avoiding exponential explosion: Generating compact verification conditions. In Proceedings of the 28th ACM Symposium on the Principles of Programming Languages (POPL) (2001).

Digital Library

[30]

{30} GANESH, V., AND DILL, D. STP: A decision procedure for bitvectors and arrays. http://theory.stanford.edu/~vganesh/stp.html.

[31]

{31} GANESH, V., AND DILL, D. A decision procedure for bit-vectors and arrays. In Proceedings of the Computer Aided Verification Conference (2007).

Digital Library

[32]

{32} GODEFROID, P., KLARLUND, N., AND SEN, K. DART: Directed automated random testing. In Proceedings of the 2005 Programming Language Design and Implementation Conference (PLDI) (2005).

Digital Library

[33]

{33} KAKSONEN, R. A Functional Method for Assessing Protocol Implementation Security. PhD thesis, Technical Research Centre of Finland, 2001.

[34]

{34} KING, J. Symbolic execution and program testing. Communications of the ACM 19 (1976), 386-394.

Digital Library

[35]

{35} KRUEGEL, C., KIRDA, E., MUTZ, D., ROBERTSON, W., AND VIGNA, G. Automating mimicry attacks using static binary analysis. In Proceedings of the 14th USENIX Security Symposium (2005).

Digital Library

[36]

{36} LEINO, K. R. M. Efficient weakest preconditions. Information Processing Letters 93, 6 (2005), 281-288.

Digital Library

[37]

{37} MARQUIS, S., DEAN, T. R., AND KNIGHT, S. SCL: a language for security testing of network applications. In Proceedings of the 2005 conference of the Centre for Advanced Studies on Collaborative research (2005).

Digital Library

[38]

{38} MILLS, D. Simple Network Time Protocol (SNTP) Version 4 for IPv4, IPv6 and OSI. RFC 4330 (Informational), 2006.

[39]

{39} MUCHNICK, S. Advanced Compiler Design and Implementation. Academic Press, 1997.

Digital Library

[40]

{40} MUSUVATHI, M., AND ENGLER, D. R. Model checking large network protocol implementations. In Proceedings of the First Symposium on Networked Systems Design and Implementation (NSDI) (2004).

Digital Library

[41]

{41} MUSUVATHI, M., PARK, D. Y., CHOU, A., ENGLER, D. R., AND DILL, D. L. CMC: A pragmatic approach to model checking real code. In Proceedings of the 5th Symposium on Operating Systems Design and Implementation (OSDI) (2002).

Digital Library

[42]

{42} NEWSOME, J., BRUMLEY, D., FRANKLIN, J., AND SONG, D. Replayer: Automatic protocol replay by binary analysis. In Proceedings of the 13th ACM Conference on Computer and Communications Security (CCS) (2006).

Digital Library

[43]

{43} OEHLERT, P. Violating assumptions with fuzzing. IEEE Security and Privacy Magazine 3, 2 (2005), 58-62.

Digital Library

[44]

{44} PAXSON, V. Automated packet trace analysis of TCP implementations. In ACM SIGCOMM 1997 (1997).

Digital Library

[45]

{45} UDREA, O., LUMEZANU, C., AND FOSTER, J. S. Rule-based static analysis of network protocol implementations. In Proceedings of the 15th USENIX Security Symposium (2006).

Digital Library

[46]

{46} XIAO, S., DENG, L., LI, S., AND WANG, X. Integrated tcp/ip protocol software testing for vulnerability detection. In Proceedings of International Conference on Computer Networks and Mobile Computing (2003).

Digital Library

[47]

{47} YANG, J., SAR, C., TWOHEY, P., CADAR, C., AND ENGLER, D. Automatically generating malicious disks using symbolic execution. In Proceedings of the 2006 IEEE Symposium on Security and Privacy (2006).

Digital Library

Cited By

Wang ZZhu SMan KZhu PHao YQian ZKrishnamurthy SLa Porta TDe Lucia MKim YKim JVigna GShi E(2021)Themis: Ambiguity-Aware Network Intrusion Detection based on Symbolic Model ComparisonProceedings of the 2021 ACM SIGSAC Conference on Computer and Communications Security10.1145/3460120.3484762(3384-3399)Online publication date: 12-Nov-2021
https://dl.acm.org/doi/10.1145/3460120.3484762
Liu XWang SWang PWu DBeecham SDamian D(2019)Automatic grading of programming assignmentsProceedings of the 41st International Conference on Software Engineering: Software Engineering Education and Training10.1109/ICSE-SEET.2019.00022(126-137)Online publication date: 27-May-2019
https://dl.acm.org/doi/10.1109/ICSE-SEET.2019.00022
Vetterl AClayton RRossow CYounan Y(2018)Bitter harvestProceedings of the 12th USENIX Conference on Offensive Technologies10.5555/3307423.3307432(9-9)Online publication date: 13-Aug-2018
https://dl.acm.org/doi/10.5555/3307423.3307432
Show More Cited By

Index Terms

Towards automatic discovery of deviations in binary implementations with applications to error detection and fingerprint generation

Recommendations

Towards the automatic generation of quality-of-service-preserving implementations from formal specifications

The possibility to automatically generate implementations from formal specifications of distributed systems and protocols is one of the major advantages of the use of formal methods. This process is well understood for standardized Formal Description ...
Fingerprint reference-point detection

A robust fingerprint recognition algorithm should tolerate the rotation and translation of the fingerprint image. One popular solution is to consistently detect a unique reference point and compute a unique reference orientation for translational and ...
A binary analysis method for protocol deviation discovery from implementations
ICOIN '13: Proceedings of the 2013 International Conference on Information Networking (ICOIN)

Generally there are several versions of implementations for a network protocol specification. However, these protocol implementations inevitably contain deviations, which are usually introduced by errors in engineering development process or different ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings

SS'07: Proceedings of 16th USENIX Security Symposium on USENIX Security Symposium

August 2007

351 pages

ISBN:1113335555779

Editor:
Niels Provos
Google Inc.

Publisher

USENIX Association

United States

Publication History

Published: 06 August 2007

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

33
Total Citations
View Citations
17
Total Downloads

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

Reflects downloads up to 03 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

Wang ZZhu SMan KZhu PHao YQian ZKrishnamurthy SLa Porta TDe Lucia MKim YKim JVigna GShi E(2021)Themis: Ambiguity-Aware Network Intrusion Detection based on Symbolic Model ComparisonProceedings of the 2021 ACM SIGSAC Conference on Computer and Communications Security10.1145/3460120.3484762(3384-3399)Online publication date: 12-Nov-2021
https://dl.acm.org/doi/10.1145/3460120.3484762
Liu XWang SWang PWu DBeecham SDamian D(2019)Automatic grading of programming assignmentsProceedings of the 41st International Conference on Software Engineering: Software Engineering Education and Training10.1109/ICSE-SEET.2019.00022(126-137)Online publication date: 27-May-2019
https://dl.acm.org/doi/10.1109/ICSE-SEET.2019.00022
Vetterl AClayton RRossow CYounan Y(2018)Bitter harvestProceedings of the 12th USENIX Conference on Offensive Technologies10.5555/3307423.3307432(9-9)Online publication date: 13-Aug-2018
https://dl.acm.org/doi/10.5555/3307423.3307432
Jain RPrathik SVinayakarao VPurandare RZaidman AKamei YHill E(2018)A search system for mathematical expressions on software binariesProceedings of the 15th International Conference on Mining Software Repositories10.1145/3196398.3196413(487-491)Online publication date: 28-May-2018
https://dl.acm.org/doi/10.1145/3196398.3196413
Katz DBultan TSen K(2017)Understanding intended behavior using models of low-level signalsProceedings of the 26th ACM SIGSOFT International Symposium on Software Testing and Analysis10.1145/3092703.3098237(424-427)Online publication date: 10-Jul-2017
https://dl.acm.org/doi/10.1145/3092703.3098237
Argyros GStais IJana SKeromytis AKiayias AWeippl EKatzenbeisser SKruegel CMyers AHalevi S(2016)SFADiffProceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security10.1145/2976749.2978383(1690-1701)Online publication date: 24-Oct-2016
https://dl.acm.org/doi/10.1145/2976749.2978383
Barrett CTinelli CDeters MLiang TReynolds ATsiskaridze NScherlis WBrumley D(2016)Efficient solving of string constraints for security analysisProceedings of the Symposium and Bootcamp on the Science of Security10.1145/2898375.2898393(4-6)Online publication date: 19-Apr-2016
https://dl.acm.org/doi/10.1145/2898375.2898393
Liang TReynolds ATsiskaridze NTinelli CBarrett CDeters M(2016)An efficient SMT solver for string constraintsFormal Methods in System Design10.1007/s10703-016-0247-648:3(206-234)Online publication date: 1-Jun-2016
https://dl.acm.org/doi/10.1007/s10703-016-0247-6
Qiu RYang GPăsăreanu CKhurshid SBertolino ACanfora GElbaum S(2015)Compositional symbolic execution with memoized replayProceedings of the 37th International Conference on Software Engineering - Volume 110.5555/2818754.2818832(632-642)Online publication date: 16-May-2015
https://dl.acm.org/doi/10.5555/2818754.2818832
Pedrosa LFogel AKothari NGovindan RMahajan RMillstein TBarham PKrishnamurthy A(2015)Analyzing protocol implementations for interoperabilityProceedings of the 12th USENIX Conference on Networked Systems Design and Implementation10.5555/2789770.2789804(485-498)Online publication date: 4-May-2015
https://dl.acm.org/doi/10.5555/2789770.2789804
Show More Cited By

View Options

View options

Figures

Tables

Media

View Table of Conten