research-article

Path-exploration lifting: hi-fi tests for lo-fi emulators

Authors:

Lorenzo Martignoni,

Stephen McCamant,

Pongsin Poosankam,

Petros ManiatisAuthors Info & Claims

ACM SIGARCH Computer Architecture News, Volume 40, Issue 1

Pages 337 - 348

https://doi.org/10.1145/2189750.2151012

Published: 03 March 2012 Publication History

Abstract

Processor emulators are widely used to provide isolation and instrumentation of binary software. However they have proved difficult to implement correctly: processor specifications have many corner cases that are not exercised by common workloads. It is untenable to base other system security properties on the correctness of emulators that have received only ad-hoc testing. To obtain emulators that are worthy of the required trust, we propose a technique to explore a high-fidelity emulator with symbolic execution, and then lift those test cases to test a lower-fidelity emulator. The high-fidelity emulator serves as a proxy for the hardware specification, but we can also further validate by running the tests on real hardware. We implement our approach and apply it to generate about 610,000 test cases; for about 95% of the instructions we achieve complete path coverage. The tests reveal thousands of individual differences; we analyze those differences to shed light on a number of root causes, such as atomicity violations and missing security features.

References

[1]

Advanced Micro Devices. AMD64 virtualization: Secure virtual machine architecture reference manual. AMD Publication no. 33047 rev. 3.01, 2005.

[2]

T. Arons, E. Elster, L. Fix, S. Mador-Haim, M. Mishaeli, J. Shalev, E. Singerman, A. Tiemeyer, M. Vardi, and L. Zuck. Formal Verification of Backward Compatibility of Microcode. In Computer Aided Verification (CAV), 2005.

Digital Library

[3]

U. Bayer, C. Kruegel, and E. Kirda. TTAnalyze: A Tool for Analyzing Malware. In European Institute for Computer Antivirus Research (EICAR), 2006.

[4]

D. Brumley, C. Hartwig, Z. Liang, J. Newsome, D. Song, and H. Yin. Automatically identifying trigger-based behavior in malware. In W. Lee, C. Wang, and D. Dagon, editors, Botnet Detection, volume 36 of Advances in Information Security. Springer, 2008.

[5]

J. Caballero, P. Poosankam, S. McCamant, D. Babic, and D. Song. Input generation via decomposition and re-stitching: Finding bugs in malware. In CCS, 2010.

Digital Library

[6]

C. Cadar, D. Dunbar, and D. Engler. KLEE: Unassisted and automatic generation of high-coverage tests for complex systems programs. In OSDI, 2008.

Digital Library

[7]

C. Cadar and D. Engler. Execution generated test cases: How to make systems code crash itself. In Model Checking Software (SPIN Workshop), 2005.

Digital Library

[8]

C. Cadar, V. Ganesh, P. M. Pawlowski, D. L. Dill, and D. Engler. EXE: automatically generating inputs of death. In CCS, 2006.

Digital Library

[9]

X. Chen, T. Garfinkel, E. C. Lewis, P. Subrahmanyam, C. A. Waldspurger, D. Boneh, J. Dwoskin, and D. R. K. Ports. Overshadow: A Virtualization-Based Approach to Retrofitting Protection in Commodity Operating Systems. In ASPLOS, 2008.

Digital Library

[10]

V. Chipounov, V. Kuznetsov, and G. Candea. S2E: A platform for in-vivo multi-path analysis of software systems. In ASPLOS, 2011.

Digital Library

[11]

P. Collingbourne, C. Cadar, and P. H. J. Kelly. Symbolic Crosschecking of Floating-Point and SIMD Code. In EuroSys, 2011.

Digital Library

[12]

L. de Moura and N. Bjørner. Z3: An efficient SMT solver. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2008.

Digital Library

[13]

V. Ganesh and D. L. Dill. A decision procedure for bit-vectors and arrays. In Computer Aided Verification (CAV), 2007.

Digital Library

[14]

P. Godefroid. Compositional dynamic test generation. In POPL, 2007.

Digital Library

[15]

P. Godefroid, N. Klarlund, and K. Sen. DART: directed automated random testing. In PLDI, 2005.

Digital Library

[16]

P. Godefroid, M. Y. Levin, and D. A. Molnar. Automated whitebox fuzz testing. In Network and Distributed System Security (NDSS), 2008.

[17]

A. Ho, M. Fetterman, C. Clark, A. Warfield, and S. Hand. Practical Taint-Based Protection using Demand Emulation. In EuroSys, 2006.

Digital Library

[18]

J. C. King. Symbolic execution and program testing. Communications of the ACM, 19(7), 1976.

Digital Library

[19]

Kernel-based Virtual Machine (KVM). http://linux-kvm.org/.

[20]

L. Martignoni, R. Paleari, G. F. Roglia, and D. Bruschi. Testing CPU emulators. In International Symposium on Software Testing and Analysis (ISSTA), 2009.

Digital Library

[21]

L. Martignoni, R. Paleari, G. F. Roglia, and D. Bruschi. Testing system virtual machines. In International Symposium on Software Testing and Analysis (ISSTA), 2010.

Digital Library

[22]

D. Molnar, X. C. Li, and D. A. Wagner. Dynamic test generation to find integer bugs in x86 binary Linux programs. In USENIX Security Symposium, 2009.

Digital Library

[23]

A. Moser, C. Kruegel, and E. Kirda. Exploring Multiple Execution Paths for Malware Analysis. In IEEE Symposium on Security and Privacy (Oakland), 2007.

Digital Library

[24]

G. Neiger, A. Santoni, F. Leung, D. Rodgers, and R. Uhlig. Intel Virtualization Technology: Hardware support for efficient processor virtualization. Intel Technology Journal, 10(3), 2006.

[25]

N. Nethercote and J. Seward. Valgrind: a framework for heavyweight dynamic binary instrumentation. In PLDI, 2007.

Digital Library

[26]

K. Sen, D. Marinov, and G. Agha. CUTE: A concolic unit testing engine for C. In European Software Engineering Conference / Foundations of Software Engineering (ESEC/FSE), 2005.

Digital Library

[27]

D. Song, D. Brumley, H. Yin, J. Caballero, I. Jager, M. G. Kang, Z. Liang, J. Newsome, P. Poosankam, and P. Saxena. BitBlaze: A new approach to computer security via binary analysis. In International Conf. on Information Systems Security (ICISS), 2008. Keynote.

Digital Library

[28]

B. Yee, D. Sehr, G. Dardyk, J. B. Chen, R. Muth, T. Ormandy, S. Okasaka, N. Narula, and N. Fullagar. Native client: A sandbox for portable, untrusted x86 native code. In IEEE Symposium on Security and Privacy (Oakland), 2009.

Digital Library

[29]

Q. Zhang, J. McCullough, J. Ma, N. Schear, M. Vrable, A. Vahdat, A. C. Snoeren, G. M. Voelker, and S. Savage. Neon: system support for derived data management. In Virtual Execution Environments (VEE), 2010.

Digital Library

Cited By

Yao MFuller JSridhar RAgarwal SSikder ASaltaformaggio BCalandrino JTroncoso C(2023)Hiding in plain sightProceedings of the 32nd USENIX Conference on Security Symposium10.5555/3620237.3620579(6115-6132)Online publication date: 9-Aug-2023
https://dl.acm.org/doi/10.5555/3620237.3620579
Zhou SJiang MChen WZhou HWang HLuo XBissyandé TKlein JBird CSarro F(2023)WADIFF: A Differential Testing Framework for WebAssembly RuntimesProceedings of the 38th IEEE/ACM International Conference on Automated Software Engineering10.1109/ASE56229.2023.00188(939-950)Online publication date: 11-Nov-2023
https://dl.acm.org/doi/10.1109/ASE56229.2023.00188
Yilmaz FSridhar MChoi W(2020)Guide Me to Exploit: Assisted ROP Exploit Generation for ActionScript Virtual MachineProceedings of the 36th Annual Computer Security Applications Conference10.1145/3427228.3427568(386-400)Online publication date: 7-Dec-2020
https://dl.acm.org/doi/10.1145/3427228.3427568
Show More Cited By

Index Terms

Path-exploration lifting: hi-fi tests for lo-fi emulators
1. Software and its engineering
  1. Software creation and management
    1. Software verification and validation
      1. Software defect analysis
        Software testing and debugging

Recommendations

Fast PokeEMU: Scaling Generated Instruction Tests Using Aggregation and State Chaining
VEE '18: Proceedings of the 14th ACM SIGPLAN/SIGOPS International Conference on Virtual Execution Environments

Software that emulates a CPU has many applications, but is difficult to implement correctly and requires extensive testing. Since a large number of test cases are required for full coverage, it is important that the tests execute efficiently. We explore ...
Path-exploration lifting: hi-fi tests for lo-fi emulators
ASPLOS '12

Processor emulators are widely used to provide isolation and instrumentation of binary software. However they have proved difficult to implement correctly: processor specifications have many corner cases that are not exercised by common workloads. It is ...
Path-exploration lifting: hi-fi tests for lo-fi emulators
ASPLOS XVII: Proceedings of the seventeenth international conference on Architectural Support for Programming Languages and Operating Systems

Processor emulators are widely used to provide isolation and instrumentation of binary software. However they have proved difficult to implement correctly: processor specifications have many corner cases that are not exercised by common workloads. It is ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM SIGARCH Computer Architecture News

ACM SIGARCH Computer Architecture News Volume 40, Issue 1

ASPLOS '12

March 2012

453 pages

ISSN:0163-5964

DOI:10.1145/2189750

Issue’s Table of Contents

ASPLOS XVII: Proceedings of the seventeenth international conference on Architectural Support for Programming Languages and Operating Systems
March 2012
476 pages
ISBN:9781450307598
DOI:10.1145/2150976
General Chair:
Tim Harris
Microsoft Research
,
Program Chair:
Michael L. Scott
University of Rochester

Copyright © 2012 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 03 March 2012

Published in SIGARCH Volume 40, Issue 1

Check for updates

Author Tags

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

67
Total Citations
View Citations
538
Total Downloads

Downloads (Last 12 months)32
Downloads (Last 6 weeks)2

Reflects downloads up to 13 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Yao MFuller JSridhar RAgarwal SSikder ASaltaformaggio BCalandrino JTroncoso C(2023)Hiding in plain sightProceedings of the 32nd USENIX Conference on Security Symposium10.5555/3620237.3620579(6115-6132)Online publication date: 9-Aug-2023
https://dl.acm.org/doi/10.5555/3620237.3620579
Zhou SJiang MChen WZhou HWang HLuo XBissyandé TKlein JBird CSarro F(2023)WADIFF: A Differential Testing Framework for WebAssembly RuntimesProceedings of the 38th IEEE/ACM International Conference on Automated Software Engineering10.1109/ASE56229.2023.00188(939-950)Online publication date: 11-Nov-2023
https://dl.acm.org/doi/10.1109/ASE56229.2023.00188
Yilmaz FSridhar MChoi W(2020)Guide Me to Exploit: Assisted ROP Exploit Generation for ActionScript Virtual MachineProceedings of the 36th Annual Computer Security Applications Conference10.1145/3427228.3427568(386-400)Online publication date: 7-Dec-2020
https://dl.acm.org/doi/10.1145/3427228.3427568
Koltunov DEfimov VPadaryan V(2020)Automated Testing of a TCG Frontend for QemuProgramming and Computer Software10.1134/S036176882008005846:8(737-746)Online publication date: 22-Dec-2020
https://doi.org/10.1134/S0361768820080058
Alrabaee SDebbabi MShirani PWang LYoussef ARahimian ANouh LMouheb DHuang HHanna AAlrabaee SDebbabi MShirani PWang LYoussef ARahimian ANouh LMouheb DHuang HHanna A(2020)Binary Analysis OverviewBinary Code Fingerprinting for Cybersecurity10.1007/978-3-030-34238-8_2(7-44)Online publication date: 1-Mar-2020
https://doi.org/10.1007/978-3-030-34238-8_2
Wang WMcCamant SZhai AYew P(2018)Enhancing Cross-ISA DBT Through Automatically Learned Translation RulesACM SIGPLAN Notices10.1145/3296957.317716053:2(84-97)Online publication date: 19-Mar-2018
https://dl.acm.org/doi/10.1145/3296957.3177160
Rizzi EElbaum SDwyer MDillon LVisser WWilliams L(2016)On the techniques we create, the tools we build, and their misalignmentsProceedings of the 38th International Conference on Software Engineering10.1145/2884781.2884835(132-143)Online publication date: 14-May-2016
https://dl.acm.org/doi/10.1145/2884781.2884835
Cai JZou PMa JHe J(2016)SwordDTA: A dynamic taint analysis tool for software vulnerability detectionWuhan University Journal of Natural Sciences10.1007/s11859-016-1133-121:1(10-20)Online publication date: 9-Jan-2016
https://doi.org/10.1007/s11859-016-1133-1
Amit NTsafrir DSchuster AAyoub AShlomo EMiller EHand S(2015)Virtual CPU validationProceedings of the 25th Symposium on Operating Systems Principles10.1145/2815400.2815420(311-327)Online publication date: 4-Oct-2015
https://dl.acm.org/doi/10.1145/2815400.2815420
Chesser MNepal SRanasinghe DJust RFraser G(2023)Icicle: A Re-designed Emulator for Grey-Box Firmware FuzzingProceedings of the 32nd ACM SIGSOFT International Symposium on Software Testing and Analysis10.1145/3597926.3598039(76-88)Online publication date: 12-Jul-2023
https://dl.acm.org/doi/10.1145/3597926.3598039
Show More Cited By

View Options

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Issue’s Table of Contents