6 Acknowledgements, Data-availabilty and References

6.1 Acknowledgements

This paper is based upon work supported by the Defense Advanced Research Projects Agency (DARPA) and Naval Information Warfare Center Pacific (NIWC Pacific) under Prime Contract No. N66001-21-C-4028, and by DARPA under Prime Contract No. HR001124C0492. Any views, opinions, findings, and conclusions or recommendations expressed in this paper are those of the authors and should not be interpreted as presenting the official policies or position, either expressed or implied, of DARPA or the U.S. Government. The U.S. Government is authorized to reproduce and distribute reprints of publications for Government purposes notwithstanding any copyright notation hereon.

6.2 Data-availability statement

All source code is available on https://liblisa.nl/sem86 under the AGPLv3 open source license.

6.3 References

  • [1] O. Sahin, A. K. Coskun, and M. Egele, “Proteus: Detecting android emulators from instruction-level profiles,” in International Symposium on Research in Attacks, Intrusions, and Defenses, 2018, pp. 3–24.
  • [2] T. Raffetseder, C. Kruegel, and E. Kirda, “Detecting system emulators,” in International Conference on Information Security, 2007, pp. 1–18.
  • [3] Y. Choi, Y. Jeong, D. Jang, B. B. Kang, and H. Lee, “EmuID: Detecting presence of emulation through microarchitectural characteristic on ARM,” Computers & Security, vol. 113, p. 102569, 2022.
  • [4] X. Chen, J. Andersen, Z. M. Mao, M. Bailey, and J. Nazario, “Towards an understanding of anti-virtualization and anti-debugging behavior in modern malware,” in 2008 IEEE international conference on dependable systems and networks with FTCS and DCC (DSN), 2008, pp. 177–186.
  • [5] SonicWall, “New Anti-VM technique observed in the wild,” 2017. [Online]. Available: http://web.archive.org/web/20201026062235/https://www.mysonicwall.com/sonicalert/searchresults.aspx?ev=article&id=1085
  • [6] F. Bellard, “QEMU, a fast and portable dynamic translator.,” in USENIX annual technical conference, FREENIX Track, 2005, pp. 10–55.
  • [7] K. P. Lawton, “Bochs: A portable pc emulator for unix/x,” Linux Journal, vol. 1996, no. 29es, p. 7–es, 1996.
  • [8] N. Binkert et al., “The gem5 simulator,” ACM SIGARCH computer architecture news, vol. 39, no. 2, pp. 1–7, 2011.
  • [9] W. Ma, J.-C. Liu, and A. Forin, “Design and Testing of a CPU Emulator,” Texas A&M University, Microsoft Research Technical Report, United States of America, vol. 1, p. 12, 2009.
  • [10] L. Martignoni, R. Paleari, G. F. Roglia, and D. Bruschi, “Testing CPU emulators,” in Proceedings of the eighteenth international symposium on Software testing and analysis, 2009, pp. 261–272.
  • [11] A. Coglio and S. Goel, “Adding 32-bit Mode to the ACL2 Model of the x86 ISA,” arXiv preprint arXiv:1810.04313, 2018.
  • [12] A. Armstrong et al., “ISA semantics for ARMv8-a, RISC-v, and CHERI-MIPS,” Proc. ACM Program. Lang., vol. 3, no. POPL, Jan. 2019, doi: 10.1145/3290384.
  • [13] S. Heule, E. Schkufza, R. Sharma, and A. Aiken, “Stratified synthesis: automatically learning the x86-64 instruction set,” in Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, in PLDI '16. Santa Barbara, CA, USA: Association for Computing Machinery, 2016, pp. 237–250. doi: 10.1145/2908080.2908121.
  • [14] S. Dasgupta, D. Park, T. Kasampalis, V. S. Adve, and G. Roşu, “A complete formal semantics of x86-64 user-level instruction set architecture,” in Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2019, pp. 1133–1148.
  • [15] C. Barrett, A. Stump, C. Tinelli, and others, “The SMT-LIB Standard: Version 2.0,” in Proceedings of the 8th international workshop on satisfiability modulo theories (Edinburgh, UK), 2010, p. 14.
  • [16] J. Craaijo, F. Verbeek, and B. Ravindran, “libLISA: instruction discovery and analysis on x86-64,” Proceedings of the ACM on Programming Languages, vol. 8, no. OOPSLA2, pp. 333–361, 2024.
  • [17] D. Balsom, “MartyPC,” 2023. [Online]. Available: https://github.com/dbalsom/martypc
  • [18] C. Bolz-Tereick, L. Panayi, F. McKeogh, T. Spink, and M. Berger, “Pydrofoil: Accelerating Sail-Based Instruction Set Simulators,” in 39th European Conference on Object-Oriented Programming (ECOOP 2025), J. Aldrich and A. Silva, Eds., in Leibniz International Proceedings in Informatics (LIPIcs), vol. 333. Dagstuhl, Germany: Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2025, p. 3:1–3:31. doi: 10.4230/LIPIcs.ECOOP.2025.3.
  • [19] T. Spink, H. Wagstaff, and B. Franke, “A retargetable system-level DBT hypervisor,” ACM Transactions on Computer Systems (TOCS), vol. 36, no. 4, pp. 1–24, 2020.
  • [20] G. Morrisett, G. Tan, J. Tassarotti, J.-B. Tristan, and E. Gan, “RockSalt: better, faster, stronger SFI for the x86,” in Proceedings of the 33rd ACM SIGPLAN Conference on Programming Language Design and Implementation, in PLDI '12. Beijing, China: Association for Computing Machinery, 2012, pp. 395–404. doi: 10.1145/2254064.2254111.
  • [21] X. Leroy, “Formal verification of a realistic compiler,” Commun. ACM, vol. 52, no. 7, pp. 107–115, Jul. 2009, doi: 10.1145/1538788.1538814.
  • [22] P. Godefroid and A. Taly, “Automated synthesis of symbolic instruction encodings from I/O samples,” in Proceedings of the 33rd ACM SIGPLAN Conference on Programming Language Design and Implementation, in PLDI '12. Beijing, China: Association for Computing Machinery, 2012, pp. 441–452. doi: 10.1145/2254064.2254116.
  • [23] C. Domas, “Breaking the x86 ISA.” [Online]. Available: https://github.com/xoreaxeaxeax/sandsifter
  • [24] B. Ness and V. Ngo, “Regression containment through source change isolation,” in Proceedings Twenty-First Annual International Computer Software and Applications Conference (COMPSAC'97), 1997, pp. 616–621. doi: 10.1109/CMPSAC.1997.625082.