This is a web version of the paper
'libLISA: Instruction Discovery and Analysis on x86-64'
by Jos Craaijo, Freek Verbeek, Binoy Ravindran, first published at OOPSLA'24.

Download PDF Visit liblisa.nl

7 Acknowledgements, Data-availabilty and References

7.1 Acknowledgements

We thank the anonymous reviewers for their insightful comments, which have greatly improved the paper.

This work is supported by the Defense Advanced Research Projects Agency (DARPA) and Naval Information Warfare Center Pacific (NIWC Pacific) under Contract No. N66001-21-C-4028.

7.2 Data-availability statement

The analysis results are available in an easily browsable format on https://explore.liblisa.nl/. The libLISA implementation is available under the AGPLv3 open source license on https://github.com/liblisa. A self-contained reproduction package is available on Zenodo [29].

7.3 References

  • [1] 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, in PLDI '19. Phoenix, AZ, USA: Association for Computing Machinery, 2019, pp. 1133–1148. doi: 10.1145/3314221.3314601.
  • [2] 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.
  • [3] X. Leroy, “Formal verification of a realistic compiler,” Commun. ACM, vol. 52, no. 7, pp. 107–115, Jul. 2009, doi: 10.1145/1538788.1538814.
  • [4] S. Goel, W. A. Hunt, M. Kaufmann, and S. Ghosh, “Simulation and Formal Verification of x86 Machine-Code Programs that make System Calls,” in Proceedings of the 14th Conference on Formal Methods in Computer-Aided Design, in FMCAD '14. Lausanne, Switzerland: FMCAD Inc, 2014, pp. 91–98. doi: 10.1109/FMCAD.2014.6987600.
  • [5] N. Hasabnis and R. Sekar, “Extracting instruction semantics via symbolic execution of code generators,” in Proceedings of the 2016 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering, in FSE 2016. Seattle, WA, USA: Association for Computing Machinery, 2016, pp. 301–313. doi: 10.1145/2950290.2950335.
  • [6] 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.
  • [7] J. Lim and T. Reps, “TSL: A System for Generating Abstract Interpreters and its Application to Machine-Code Analysis,” ACM Trans. Program. Lang. Syst., vol. 35, no. 1, Apr. 2013, doi: 10.1145/2450136.2450139.
  • [8] C. Domas, “Breaking the x86 ISA.” [Online]. Available: https://github.com/xoreaxeaxeax/sandsifter
  • [9] X. Li, Z. Wu, Q. Wei, and H. Wu, “UISFuzz: An Efficient Fuzzing Method for CPU Undocumented Instruction Searching,” IEEE Access, vol. 7, no. , pp. 149224–149236, 2019, doi: 10.1109/ACCESS.2019.2946444.
  • [10] R. Dofferhoff, M. Göebel, K. Rietveld, and E. van der Kouwe, “iScanU: A Portable Scanner for Undocumented Instructions on RISC Processors,” in 2020 50th Annual IEEE/IFIP International Conference on Dependable Systems and Networks, in DSN 2020, . 2020, pp. 306–317. doi: 10.1109/DSN48063.2020.00047.
  • [11] D. Kwan, K. Shtoyk, K. Serebryany, M. L. Lifantsev, and P. Hochschild, “SiliFuzz: fuzzing CPUs by proxy,” Google Research, 2021, doi: 10.48550/arXiv.2110.11519.
  • [12] 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, in ISSTA '09. Chicago, IL, USA: Association for Computing Machinery, 2009, pp. 261–272. doi: 10.1145/1572272.1572303.
  • [13] F. Solt, K. Ceesay-Seitz, and K. Razavi, “Cascade: CPU Fuzzing via Intricate Program Generation,” in 33rd USENIX Security Symposium (USENIX Security 24), Philadelphia, PA: USENIX Association, Aug. 2024, pp. 5341–5358.
  • [14] 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.
  • [15] E. Schkufza, R. Sharma, and A. Aiken, “Stochastic superoptimization,” in Proceedings of the Eighteenth International Conference on Architectural Support for Programming Languages and Operating Systems, in ASPLOS '13. Houston, Texas, USA: Association for Computing Machinery, 2013, pp. 305–316. doi: 10.1145/2451116.2451150.
  • [16] 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.
  • [17] 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.
  • [18] A. Reid, “Trustworthy specifications of ARM® v8-A and v8-M system level architecture,” in Proceedings of the 16th Conference on Formal Methods in Computer-Aided Design, in FMCAD '16. Mountain View, California: FMCAD Inc, 2016, pp. 161–168. doi: 10.1109/FMCAD.2016.7886675.
  • [19] P. Sewell, S. Sarkar, S. Owens, F. Z. Nardelli, and M. O. Myreen, “x86-TSO: a rigorous and usable programmer's model for x86 multiprocessors,” Commun. ACM, vol. 53, no. 7, pp. 89–97, Jul. 2010, doi: 10.1145/1785414.1785443.
  • [20] J. Ševčík, V. Vafeiadis, F. Zappa Nardelli, S. Jagannathan, and P. Sewell, “CompCertTSO: A Verified Compiler for Relaxed-Memory Concurrency,” J. ACM, vol. 60, no. 3, Jun. 2013, doi: 10.1145/2487241.2487248.
  • [21] A. Barrington, S. Feldman, and D. Dechev, “A scalable multi-producer multi-consumer wait-free ring buffer,” in Proceedings of the 30th Annual ACM Symposium on Applied Computing, in SAC '15. Salamanca, Spain: Association for Computing Machinery, 2015, pp. 1321–1328. doi: 10.1145/2695664.2695924.
  • [22] N. Jay and B. P. Miller, “Structured random differential testing of instruction decoders,” in 2018 IEEE 25th International Conference on Software Analysis, Evolution and Reengineering (SANER), 2018, pp. 84–94. doi: 10.1109/SANER.2018.8330199.
  • [23] A. Solar-Lezama, L. Tancau, R. Bodik, S. Seshia, and V. Saraswat, “Combinatorial sketching for finite programs,” in Proceedings of the 12th International Conference on Architectural Support for Programming Languages and Operating Systems, in ASPLOS XII. San Jose, California, USA: Association for Computing Machinery, 2006, pp. 404–415. doi: 10.1145/1168857.1168907.
  • [24] R. Alur, R. Singh, D. Fisman, and A. Solar-Lezama, “Search-Based Program Synthesis,” Commun. ACM, vol. 61, no. 12, pp. 84–93, Nov. 2018, doi: 10.1145/3208071.
  • [25] R. Alur, A. Radhakrishna, and A. Udupa, “Scaling Enumerative Program Synthesis via Divide and Conquer,” in Tools and Algorithms for the Construction and Analysis of Systems, A. Legay and T. Margaria, Eds., in TACAS 2017. Berlin, Heidelberg: Springer Berlin Heidelberg, 2017, pp. 319–336. doi: 10.1007/978-3-662-54577-5_18.
  • [26] L. de Moura and N. Bjørner, “Z3: An Efficient SMT Solver,” in Tools and Algorithms for the Construction and Analysis of Systems, C. R. Ramakrishnan and J. Rehof, Eds., in TACAS 2008. Berlin, Heidelberg: Springer Berlin Heidelberg, 2008, pp. 337–340. doi: 10.1007/978-3-540-78800-3_24.
  • [27] G. Roșu and T. F. Șerbănută, “An overview of the K semantic framework,” The Journal of Logic and Algebraic Programming, vol. 79, no. 6, pp. 397–434, 2010, doi: https://doi.org/10.1016/j.jlap.2010.03.012.
  • [28] D. Brumley, I. Jager, T. Avgerinos, and E. J. Schwartz, “BAP: A Binary Analysis Platform,” in Computer Aided Verification, G. Gopalakrishnan and S. Qadeer, Eds., Berlin, Heidelberg: Springer Berlin Heidelberg, 2011, pp. 463–469. doi: 10.1007/978-3-642-22110-1_37.
  • [29] J. Craaijo, F. Verbeek, and B. Ravindran, “Reproduction package (Docker container) for the OOPSLA 2024 Article ``libLISA: Instruction Discovery and Analysis on x86-64'',” 2024. doi: 10.5281/zenodo.13380062.