Skip to main content
SpringerLink
Log in

Versatile Binary-Level Concolic Testing

  • Living reference work entry
  • First Online:
Handbook of Computer Architecture

Abstract

Computing systems are experiencing an explosive growth, both in complexities and diversities, ushered in by the proliferation of cloud computing, mobile computing, and Internet of Things. This growth has also exposed the consequences of unsafe, insecure, and unreliable computing systems. These all point to the great needs of sophisticated system validation techniques. This chapter presents versatile binary-level concolic testing, which defines a standard execution-trace format, and features an open and highly extensible architecture. It allows easy integration of multiple concrete execution frontends and symbolic execution backends, which significantly improves the applicability and flexibility of symbolic execution, especially to modern computing systems with various components, e.g., operating systems, firmware, and hardware devices. First, this chapter presents the design and implementation of CRETE, the infrastructure of versatile binary-level concolic testing. Second, this chapter presents COD, a framework based on versatile binary-level concolic testing for automated bug detection and replay of commercial off-the-shelf (COTS) Linux kernel modules (LKMs). This framework automatically generates compact sets of test cases for COTS LKMs, proactively checks for common kernel bugs, and allows to reproduce reported bugs repeatedly with actionable test cases. Last, this chapter presents how versatile binary-level concolic testing is leveraged for system-level validation of Systems-on-Chips (SoC). The authors capture runtime traces of hardware/software (HW/SW) components across the entire SoC stack which are emulated by multiple virtual platforms. Based on segmented traces captured from various SoC components, the authors assemble system-level traces and provide interfaces for users to inject system-level assertions to validate.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Similar content being viewed by others

References

  • Alam T, Yang Z, Chen B, Armour N, Ray S (2022) Firver: concolic testing for systematic validation of firmware binaries. In: 27th Asia and South Pacific design automation conference, ASP-DAC 2022, Taipei, 17–20 Jan 2022. IEEE, pp 352–357

    Google Scholar 

  • Avgerinos T, Rebert A, Cha SK, Brumley D (2014a) Enhancing symbolic execution with veritesting. In: 36th international conference on software engineering, ICSE’14, Hyderabad, pp 1083–1094

    Google Scholar 

  • Avgerinos T, Cha SK, Rebert A, Schwartz EJ, Woo M, Brumley D (2014b) Automatic exploit generation. Commun ACM 57(2):74–84

    Article  Google Scholar 

  • Bai JJ, Wang YP, Yin J, Hu SM (2016) Testing error handling code in device drivers using characteristic fault injection. In: Proceedings of the 2016 USENIX conference on Usenix annual technical conference, USENIX ATC’16, Berkeley. USENIX Association, pp 635–647

    Google Scholar 

  • Baldoni R, Coppa E, D’Elia DC, Demetrescu C, Finocchi I (2018) A survey of symbolic execution techniques. ACM Comput Surv 51(3):50:1–50:39

    Google Scholar 

  • Bessey A, Block K, Chelf B, Chou A, Fulton B, Hallem S, Henri-Gros C, Kamsky A, McPeak S, Engler D (2010) A few billion lines of code later: using static analysis to find bugs in the real world. Commun ACM 53(2):66–75

    Article  Google Scholar 

  • Bruening D, Zhao Q, Amarasinghe S (2012) Transparent dynamic instrumentation. In: Proceedings of the 8th ACM SIGPLAN/SIGOPS conference on virtual execution environments, VEE’12, New York. ACM, pp 133–144

    Chapter  Google Scholar 

  • Bucur S, Kinder J, Candea G (2014) Prototyping symbolic execution engines for interpreted languages. In: Proceedings of the 19th international conference on architectural support for programming languages and operating systems, ASPLOS’14, New York. ACM, pp 239–254

    Google Scholar 

  • Cadar C, Sen K (2013) Symbolic execution for software testing: three decades later. Commun ACM 56(2):82–90

    Article  Google Scholar 

  • Cadar C, Dunbar D, Engler D (2008) Klee: unassisted and automatic generation of high-coverage tests for complex systems programs. In: Proceedings of the 8th USENIX conference on operating systems design and implementation, OSDI’08, pp 209–224

    Google Scholar 

  • Cha SK, Avgerinos T, Rebert A, Brumley D (2012) Unleashing mayhem on binary code. In: IEEE symposium on security and privacy, SP2012, San Francisco, pp 380–394

    Google Scholar 

  • Cha S, Hong S, Lee J, Oh H (2018) Automatically generating search heuristics for concolic testing. In: Proceedings of the 40th international conference on software engineering, ICSE 2018, Gothenburg, pp 1244–1254

    Google Scholar 

  • Chen B (2019) Versatile binary-level concolic testing. PhD thesis, Portland State University

    Google Scholar 

  • Chen B, Havlicek C, Yang Z, Cong K, Kannavara R, Xie F (2018) CRETE: a versatile binary-level concolic testing framework. In: Fundamental approaches to software engineering. Springer International Publishing, Cham, pp 281–298

    Google Scholar 

  • Chen B, Cong K, Yang Z, Wang Q, Wang J, Lei L, Xie F (2019) End-to-end concolic testing for hardware/software co-validation. In: Proceedings of the 15th IEEE international conference on embedded software and systems, ICESS 2019, Las Vegas

    Google Scholar 

  • Chen B, Yang Z, Lei L, Cong K, Xie F (2020) Automated bug detection and replay for COTS linux kernel modules with concolic execution. In: 27th IEEE international conference on software analysis, evolution and reengineering, SANER 2020, London, 18–21 Feb 2020. IEEE, pp 172–183

    Google Scholar 

  • Chipounov V (2014) S2E: a platform for in-vivo multi-path analysis of software systems. PhD thesis, ÉCOLE POLYTECHNIQUE FÉDÉRALE DE LAUSANNE

    Google Scholar 

  • Chipounov V, Kuznetsov V, Candea G (2012) The s2e platform: design, implementation, and applications. ACM Trans Comput Syst 30(1):2:1–2:49

    Google Scholar 

  • Cong K, Lei L, Yang Z, Xie F (2015) Automatic fault injection for driver robustness testing. In: Proceedings of the 2015 international symposium on software testing and analysis, ISSTA 2015, New York. ACM, pp 361–372

    Chapter  Google Scholar 

  • Corteggiani N, Camurati G, Muench M, Poeplau S, Francillon A (2021) Soc security evaluation: reflections on methodology and tooling. IEEE Des Test 38(1):7–13

    Article  Google Scholar 

  • GNU (2022) Gnu coreutils – core utilities. https://www.gnu.org/s/coreutils

  • Godefroid P, Klarlund N, Sen K (2005) Dart: directed automated random testing. In: Proceedings of the 2005 ACM SIGPLAN conference on programming language design and implementation, PLDI’05, New York. ACM, pp 213–223

    Chapter  Google Scholar 

  • Godefroid P, Levin MY, Molnar DA (2012) SAGE: whitebox fuzzing for security testing. Commun ACM 55(3):40–44

    Article  Google Scholar 

  • Gu H, Chen M, Wei T, Lei L, Xie F (2018) Specification-driven automated conformance checking for virtual prototype and post-silicon designs. In: Proceedings of the 55th annual design automation conference, DAC 2018, San Francisco

    Google Scholar 

  • Horn A, Tautschnig M, Val C, Liang L, Melham T, Grundy J, Kroening D (2013) Formal co-validation of low-level hardware/software interfaces. In: Proceedings of FMCAD

    Book  Google Scholar 

  • Intel (2009) Pci/pci-x family of gigabit ethernet controllers software developer’s manual. https:// www.intel.com/content/dam/doc/manual/pci-pci-x-family-gbe-controllers-software-dev-manua l.pdf

  • Jakobs M, Pauck F, Platzner M, Wehrheim H, Wiersema T (2021) Software/hardware co-verification for custom instruction set processors. IEEE Access 9:160559–160579

    Article  Google Scholar 

  • Kannavara R, Havlicek CJ, Chen B, Tuttle MR, Cong K, Ray S, Xie F (2015) Challenges and opportunities with concolic testing. In: 2015 national aerospace and electronics conference (NAECON), pp 374–378

    Google Scholar 

  • Kasikci B, Zamfir C, Candea G (2015) Automated classification of data races under both strong and weak memory models. ACM Trans Program Lang Syst 37(3):8:1–8:44

    Google Scholar 

  • King JC (1976) Symbolic execution and program testing. Commun ACM 19(7):385–394

    Article  MathSciNet  MATH  Google Scholar 

  • Kurshan RP, Levin V, Minea M, Peled D, Yenigün H (2002) Combining software and hardware verification techniques. Formal Methods Syst Des (FMSD) 21(3):251–280

    Article  MATH  Google Scholar 

  • Kuznetsov V, Kinder J, Bucur S, Candea G (2012) Efficient state merging in symbolic execution. In: Proceedings of the 33rd ACM SIGPLAN conference on programming language design and implementation, PLDI’12, New York. ACM, pp 193–204

    Google Scholar 

  • Lattner C, Adve V (2004) LLVM: a compilation framework for lifelong program analysis & transformation. In: Proceedings of the international symposium on code generation and optimization: feedback-directed and runtime optimization, CGO’04, Washington, DC. IEEE Computer Society, p 75

    Google Scholar 

  • Lei L, Cong K, Yang Z, Chen B, Xie F (2019) Hardware/software co-monitoring. In: CoRR, arXiv:1905.03915 [cs.SE]

    Google Scholar 

  • Li Z, Chen B, Feng W, Xie F (2021) Concolic execution of nmap scripts for honeyfarm generation. In: Jaeger T, Qian Z (eds) MTD@CCS 2021: proceedings of the 8th ACM workshop on moving target defense, virtual event, Republic of Korea, 15 Nov 2021. ACM, pp 33–42

    Google Scholar 

  • Stoenescu T, Stefanescu A, Predut S, Ipate F (2016) RIVER: a binary analysis framework using symbolic execution and reversible x86 instructions. In: Fitzgerald JS, Heitmeyer CL, Gnesi S, Philippou A (eds) FM 2016: formal methods – 21st international symposium, Limassol, 9–11 Nov 2016, Proceedings. Volume 9995 of Lecture notes in computer science, pp 779–785

    Google Scholar 

  • Luk CK, Cohn R, Muth R, Patil H, Klauser A, Lowney G, Wallace S, Reddi VJ, Hazelwood K (2005) Pin: building customized program analysis tools with dynamic instrumentation. In: Proceedings of the 2005 ACM SIGPLAN conference on programming language design and implementation, PLDI’05, New York. ACM, pp 190–200

    Chapter  Google Scholar 

  • Lyu Y, Mishra P (2021) Scalable concolic testing of RTL models. IEEE Trans Comput 70(7):979–991

    Article  MathSciNet  MATH  Google Scholar 

  • Marinescu PD, Cadar C (2012) Make test-zesti: a symbolic execution solution for improving regression testing. In: Proceedings of the 34th international conference on software engineering, ICSE’12, Piscataway. IEEE Press, pp 716–726

    Google Scholar 

  • Mukherjee R, Purandare M, Polig R, Kroening D (2017) Formal techniques for effective co-verification of hardware/software co-designs. In: Proceedings of the 54th annual design automation conference, DAC 2017, Austin

    Google Scholar 

  • Nethercote N, Seward J (2007) Valgrind: a framework for heavyweight dynamic binary instrumentation. In: Proceedings of the 28th ACM SIGPLAN conference on programming language design and implementation, PLDI’07, New York. ACM, pp 89–100

    Google Scholar 

  • Palikareva H, Cadar C (2013) Multi-solver support in symbolic execution. In: Proceedings of the 25th international conference on computer aided verification, CAV’13. Springer, Berlin/Heidelberg, pp 53–68

    Chapter  Google Scholar 

  • Palikareva H, Kuchta T, Cadar C (2016) Shadow of a doubt: testing for divergences between software versions. In: Proceedings of the 38th international conference on software engineering, ICSE’16, New York. ACM, pp 1181–1192

    Google Scholar 

  • Ramos DA, Engler D (2015) Under-constrained symbolic execution: correctness checking for real code. In: Proceedings of the 24th USENIX conference on security symposium, SEC’15, Berkeley. USENIX Association, pp 49–64

    Google Scholar 

  • Redini N, Machiry A, Das D, Fratantonio Y, Bianchi A, Gustafson E, Shoshitaishvili Y, Kruegel C, Vigna G (2017) Bootstomp: on the security of bootloaders in mobile devices. In: 26th USENIX security symposium (USENIX security 17), Vancouver. USENIX Association, pp 781–798

    Google Scholar 

  • Renzelmann MJ, Kadav A, Swift MM (2012) Symdrive: testing drivers without devices. In: Proceedings of the 10th USENIX conference on operating systems design and implementation, OSDI’12, Berkeley. USENIX Association, pp 279–292

    Google Scholar 

  • Sen K, Marinov D, Agha G (2005) CUTE: a concolic unit testing engine for C. In: Proceedings of the 10th European software engineering conference held jointly with 13th ACM SIGSOFT international symposium on foundations of software engineering, ESEC/FSE-13, New York. ACM, pp 263–272

    Google Scholar 

  • Shoshitaishvili Y, Wang R, Salls C, Stephens N, Polino M, Dutcher A, Grosen J, Feng S, Hauser C, Krügel C, Vigna G (2016) SOK: (state of) the art of war: offensive techniques in binary analysis. In: IEEE symposium on security and privacy, SP’16. IEEE Computer Society, pp 138–157

    Google Scholar 

  • Song D, Brumley D, Yin H, Caballero J, Jager I, Kang MG, Liang Z, Newsome J, Poosankam P, Saxena P (2008) Bitblaze: a new approach to computer security via binary analysis. In: Proceedings of the 4th international conference on information systems security, ICISS’08. Springer, Berlin/Heidelberg, pp 1–25

    Google Scholar 

  • Stephens N, Grosen J, Salls C, Dutcher A, Wang R, Corbetta J, Shoshitaishvili Y, Kruegel C, Vigna G (2016) Driller: augmenting fuzzing through selective symbolic execution. In: Proceedings of the network and distributed system security symposium, NDSS’16. The Internet Society

    Google Scholar 

  • The Guardian (2017) IT meltdown has cost British Airways £80m so far, says Willie Walsh. https://www.theguardian.com/business/2017/jun/15/it-meltdown-cost-british-airlines-80m-so-far-willie-walsh-iag

  • The New York Times (2018) Facebook security breach exposes accounts of 50 million users. https://www.nytimes.com/2018/09/28/technology/facebook-hack-data-breach.html

  • Tianocore (2022) http://www.tianocore.org/

  • Tianocore (2022) EDK II. https://github.com/tianocore/edk2

  • Torvalds L (2005) Initial commit of linux kernel’s git repository. https://git.io/fjGug

  • Wong E, Zhang L, Wang S, Liu T, Tan L (2015) Dase: document-assisted symbolic execution for improving automated software testing. In: Proceedings of the 37th international conference on software engineering – Volume 1, ICSE’15, Piscataway. IEEE Press, pp 620–631

    Google Scholar 

  • Zheng H, Li D, Liang B, Zeng X, Zheng W, Deng Y, Lam W, Yang W, Xie T (2017) Automated test input generation for android: towards getting there in an industrial case. In: Proceedings of the 39th international conference on software engineering: software engineering in practice track, ICSE-SEIP’17, Piscataway. IEEE Press, pp 253–262

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Intel Corporation, Hillsboro, OR, USA

    Bo Chen

  2. Department of Computer Science, Portland State University, Portland, OR, USA

    Fei Xie

Authors
  1. Bo Chen
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Fei Xie
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Bo Chen .

Editor information

Editors and Affiliations

  1. Sch of Computer Science & Engineering, Nanyang Technological University, Singapore, Singapore

    Anupam Chattopadhyay

Section Editor information

  1. Intel, 6250 Santa Teresa Blvd., Apt 121, 95119, San Jose, California, USA

    Ray Sayak

Rights and permissions

Reprints and permissions

Copyright information

© 2022 Springer Nature Singapore Pte Ltd.

About this entry

Check for updates. Verify currency and authenticity via CrossMark

Cite this entry

Chen, B., Xie, F. (2022). Versatile Binary-Level Concolic Testing. In: Chattopadhyay, A. (eds) Handbook of Computer Architecture. Springer, Singapore. https://doi.org/10.1007/978-981-15-6401-7_40-1

Download citation

  • DOI: https://doi.org/10.1007/978-981-15-6401-7_40-1

  • Published:

  • Publisher Name: Springer, Singapore

  • Print ISBN: 978-981-15-6401-7

  • Online ISBN: 978-981-15-6401-7

  • eBook Packages: Springer Reference EngineeringReference Module Computer Science and Engineering

Publish with us

Policies and ethics

Search

Navigation