TY - GEN
T1 - Path-exploration lifting
T2 - 17th International Conference on Architectural Support for Programming Languages and Operating Systems, ASPLOS 2012
AU - Martignoni, Lorenzo
AU - McCamant, Stephen
AU - Poosankam, Pongsin
AU - Song, Dawn
AU - Maniatis, Petros
PY - 2012
Y1 - 2012
N2 - 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.
AB - 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.
KW - CPU emulators
KW - cross validation
KW - symbolic binary execution
UR - http://www.scopus.com/inward/record.url?scp=84858788346&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84858788346&partnerID=8YFLogxK
U2 - 10.1145/2150976.2151012
DO - 10.1145/2150976.2151012
M3 - Conference contribution
AN - SCOPUS:84858788346
SN - 9781450307598
T3 - International Conference on Architectural Support for Programming Languages and Operating Systems - ASPLOS
SP - 337
EP - 348
BT - ASPLOS XVII - 17th International Conference on Architectural Support for Programming Languages and Operating Systems
Y2 - 3 March 2012 through 7 March 2012
ER -