Lorenzo Martignoni
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.
- Advanced Micro Devices. AMD64 virtualization: Secure virtual machine architecture reference manual. AMD Publication no. 33047 rev. 3.01, 2005.Google Scholar
- 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. Google ScholarDigital Library
- U. Bayer, C. Kruegel, and E. Kirda. TTAnalyze: A Tool for Analyzing Malware. In European Institute for Computer Antivirus Research (EICAR), 2006.Google Scholar
- 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.Google Scholar
- 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. Google ScholarDigital Library
- C. Cadar, D. Dunbar, and D. Engler. KLEE: Unassisted and automatic generation of high-coverage tests for complex systems programs. In OSDI, 2008. Google ScholarDigital Library
- C. Cadar and D. Engler. Execution generated test cases: How to make systems code crash itself. In Model Checking Software (SPIN Workshop), 2005. Google ScholarDigital Library
- C. Cadar, V. Ganesh, P. M. Pawlowski, D. L. Dill, and D. Engler. EXE: automatically generating inputs of death. In CCS, 2006. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- V. Chipounov, V. Kuznetsov, and G. Candea. S2E: A platform for in-vivo multi-path analysis of software systems. In ASPLOS, 2011. Google ScholarDigital Library
- P. Collingbourne, C. Cadar, and P. H. J. Kelly. Symbolic Crosschecking of Floating-Point and SIMD Code. In EuroSys, 2011. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- V. Ganesh and D. L. Dill. A decision procedure for bit-vectors and arrays. In Computer Aided Verification (CAV), 2007. Google ScholarDigital Library
- P. Godefroid. Compositional dynamic test generation. In POPL, 2007. Google ScholarDigital Library
- P. Godefroid, N. Klarlund, and K. Sen. DART: directed automated random testing. In PLDI, 2005. Google ScholarDigital Library
- P. Godefroid, M. Y. Levin, and D. A. Molnar. Automated whitebox fuzz testing. In Network and Distributed System Security (NDSS), 2008.Google Scholar
- A. Ho, M. Fetterman, C. Clark, A. Warfield, and S. Hand. Practical Taint-Based Protection using Demand Emulation. In EuroSys, 2006. Google ScholarDigital Library
- J. C. King. Symbolic execution and program testing. Communications of the ACM, 19(7), 1976. Google ScholarDigital Library
- Kernel-based Virtual Machine (KVM). http://linux-kvm.org/.Google Scholar
- L. Martignoni, R. Paleari, G. F. Roglia, and D. Bruschi. Testing CPU emulators. In International Symposium on Software Testing and Analysis (ISSTA), 2009. Google ScholarDigital Library
- L. Martignoni, R. Paleari, G. F. Roglia, and D. Bruschi. Testing system virtual machines. In International Symposium on Software Testing and Analysis (ISSTA), 2010. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- A. Moser, C. Kruegel, and E. Kirda. Exploring Multiple Execution Paths for Malware Analysis. In IEEE Symposium on Security and Privacy (Oakland), 2007. Google ScholarDigital Library
- 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.Google ScholarCross Ref
- N. Nethercote and J. Seward. Valgrind: a framework for heavyweight dynamic binary instrumentation. In PLDI, 2007. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
Index Terms
- Path-exploration lifting: hi-fi tests for lo-fi emulators
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 EnvironmentsSoftware 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 '12Processor 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 '12Processor 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