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

Lorenzo Martignoni, Stephen McCamant, Pongsin Poosankam, Dawn Song, Petros Maniatis

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

52 Scopus citations

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.

Original languageEnglish (US)
Title of host publicationASPLOS XVII - 17th International Conference on Architectural Support for Programming Languages and Operating Systems
Pages337-348
Number of pages12
DOIs
StatePublished - Mar 28 2012
Event17th International Conference on Architectural Support for Programming Languages and Operating Systems, ASPLOS 2012 - London, United Kingdom
Duration: Mar 3 2012Mar 7 2012

Publication series

NameInternational Conference on Architectural Support for Programming Languages and Operating Systems - ASPLOS

Other

Other17th International Conference on Architectural Support for Programming Languages and Operating Systems, ASPLOS 2012
CountryUnited Kingdom
CityLondon
Period3/3/123/7/12

Keywords

  • CPU emulators
  • cross validation
  • symbolic binary execution

Fingerprint Dive into the research topics of 'Path-exploration lifting: Hi-fi tests for lo-fi emulators'. Together they form a unique fingerprint.

Cite this