Advertisement

Engineering a Formal, Executable x86 ISA Simulator for Software Verification

  • Shilpi GoelEmail author
  • Warren A. HuntJr.
  • Matt Kaufmann
Chapter
Part of the NASA Monographs in Systems and Software Engineering book series (NASA)

Abstract

Construction of a formal model of a computing system is a necessary practice in formal verification. The results of formal analysis can only be valued to the same degree as the model itself. Model development is error-prone, not only due to the complexity of the system being modeled, but also because it involves addressing disparate requirements. For example, a formal model should be defined using simple constructs to enable efficient reasoning but it should also be optimized to offer fast concrete simulations. Models of large computing systems are themselves large software systems and must be subject to rigorous validation. We describe our formal, executable model of the x86 instruction-set architecture; we use our model to reason about x86 machine-code programs. Validation of our x86 ISA model is done by co-simulating it regularly against a physical x86 machine. We present design decisions made during model development to optimize both validation and verification, i.e., efficiency of both simulation and reasoning. Our engineering process provides insight into the development of a software verification and model animation framework from the points of view of accuracy, efficiency, scalability, maintainability, and usability.

Keywords

System Call Machine Code Address Translation Execution Efficiency Unsigned Integer 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Notes

Acknowledgements

This project was supported by the DARPA CRASH program under N66001-10-2-4087, and preparation of this chapter was also partially supported by the DARPA MUSE program under FA8750-15-C-0007. We are currently supported by NSF SaTC program under CNS-1525472. We thank Marijn Heule for his feedback on the chapter.

References

  1. 1.
    von Neumann, J.: First draft of a report on the EDVAC. IEEE Ann. Hist. Comput. 15(4), 27–75 (1993). http://doi.ieeecomputersociety.org/10.1109/85.238389
  2. 2.
    Turing, A.M.: On computable numbers, with an application to the Entscheidungsproblem. J. Math. 58(345–363), 5 (1936)zbMATHGoogle Scholar
  3. 3.
    Rojas, R.: Konrad Zuse’s legacy: the architecture of the Z1 and Z3. Ann. Hist. Comput. IEEE 19(2), 5–16 (1997)CrossRefGoogle Scholar
  4. 4.
    Intel Manuals (September, 2015) Intel 64 and IA-32 Architectures Software Developer’s Manuals. Order Number: 325462-056USGoogle Scholar
  5. 5.
    Intel (Accessed: October, 2015.) Intel Developer Zone - ISA Extensions. See https://software.intel.com/en-us/isa-extensions/
  6. 6.
    Kaufmann, M., Moore, J.S.: (Accessed: 2015) ACL2 home page. (see http://www.cs.utexas.edu/users/moore/acl2)
  7. 7.
    Kaufmann, M., Manolios, P., Moore, J.S.: Computer-Aided Reasoning: An Approach. Kluwer Academic Publishers, Boston (2000)Google Scholar
  8. 8.
    Boyer, R.S., Kaufmann, M., Moore, J.S.: The boyer-moore theorem prover and its interactive enhancement. Comput. Math. Appl. 29(2), 27–62 (1995). http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.51.7689
  9. 9.
    Sawada, J., Hunt Jr., J.W.: Verification of FM9801: an out-of-order microprocessor model with speculative execution, exceptions, and program-modifying capability. Form. Methods Syst. Des. 20(2), 187–222 (2002). http://dl.acm.org/citation.cfm?id=584665
  10. 10.
    Hunt Jr., W.A.: FM8501: A Verified Microprocessor, LNAI, vol. 795. Springer (1994)Google Scholar
  11. 11.
    Section 2.2.10: Intel 64 Architecture, Vol. 1, Intel 64 and IA-32 Architectures Software Developer’s Manual. (September, 2015) Order Number: 325462-056USGoogle Scholar
  12. 12.
    x86isa Books in the ACL2 Community Books Project on Github (Accessed: October, 2015). See https://github.com/acl2/acl2/tree/master/books/projects/x86isa
  13. 13.
    x86isa ACL2 Books (Accessed: October, 2015) Documentation of the bleeding-edge ACL2-based model of the x86 ISA. http://www.cs.utexas.edu/users/moore/acl2/manuals/current/manual/index.html?topic=ACL2____X86ISA
  14. 14.
    Bevier, W.R., Hunt Jr., W.A., Moore, J.S., Young, W.D.: Special issue on system verification. J. Autom. Reason. 5(4), 409–530 (1989)Google Scholar
  15. 15.
    Kaufmann, M., Moore, J.S., Ray, S., Reeber, E.: Integrating external deduction tools with ACL2. J. Appl. Log. 7(1), 3–25 (2009). doi: 10.1016/j.jal.2007.07.002, http://www.sciencedirect.com/science/article/pii/S1570868307000602, special Issue: Empirically Successful Computerized Reasoning
  16. 16.
    Swords, S.: A Verified Framework for Symbolic Execution in the ACL2 Theorem Prover. PhD thesis, Department of Computer Sciences, The University of Texas at Austin (2010). http://repositories.lib.utexas.edu/handle/2152/ETD-UT-2010-12-2210
  17. 17.
    Glucose SAT Solver (Accessed: October, 2015). http://www.labri.fr/perso/lsimon/glucose/
  18. 18.
    Minisat SAT Solver (Accessed: October, 2015). http://minisat.se/
  19. 19.
    ACL2 System and Books Repository on Github (Accessed: October, 2015). See https://github.com/acl2/acl2
  20. 20.
    Davis, J., Kaufmann, M.: Industrial-Strength Documentation for ACL2. EPTCS 152:9–25 (2014). http://www.cs.utexas.edu/users/kaufmann/talks/acl2-workshop-2014/acl2-14-davis-kaufmann.pdf
  21. 21.
    Kaufmann, M., Moore, J.S.: (Accessed: October, 2015) ACL2 documentation. See http://www.cs.utexas.edu/users/moore/acl2/current/manual/index.html?topic=ACL2____ACL2
  22. 22.
    2005 ACM Software System Award (2005) The Boyer-Moore Theorem Prover. (see http://awards.acm.org/software_system/)
  23. 23.
  24. 24.
    Centaur Technology (Accessed: October 2015). http://www.centtech.com
  25. 25.
    FV Group at Centaur (Accessed: October, 2015). http://fv.centtech.com
  26. 26.
    Davis, J., Slobodova, A., Swords, S.: Microcode verification — another piece of the microprocessor verification puzzle. In: Klein, G., Gamboa, R. (eds.) Interactive Theorem Proving, Lecture Notes in Computer Science, vol. 8558, pp. 1–16. Springer International Publishing (2014). doi: 10.1007/978-3-319-08970-6_1
  27. 27.
    Hunt Jr., W.A., Swords, S., Davis, J., Slobodova, A.: Use of formal verification at centaur technology. In: Hardin, D.S. (ed.) Design and Verification of Microprocessor Systems for High-Assurance Applications, pp. 65–88. Springer (2010). https://www.cs.utexas.edu/~jared/publications/2010-hardin-centaur.pdf
  28. 28.
    Flatau, A., Kaufmann, M., Reed, D.F., Russinoff, D., Smith, E.W., Sumners, R.: Formal verification of microprocessors at AMD. In: 4th International Workshop on Designing Correct Circuits (DCC 2002), Grenoble, France (2002)Google Scholar
  29. 29.
    Russinoff, D.M.: A case study in formal verification of register-transfer logic with ACL2: the floating point adder of the AMD athlon TM processor. In: Formal Methods in Computer-Aided Design, pp. 22–55. Springer (2000)Google Scholar
  30. 30.
    Russinoff, David: Computation and formal verification of SRT quotient and square root digit selection tables. IEEE Trans. Comput. 62(5), 900–913 (2013)MathSciNetCrossRefGoogle Scholar
  31. 31.
    Russinoff, D., Kaufmann, M., Smith, E., Sumners, R.: Formal verification of floating-point RTL at AMD using the ACL2 theorem prover. In: Proceedings of the 17th IMACS World Congress on Scientific Computation, Applied Mathematics and Simulation, Paris, France (2005)Google Scholar
  32. 32.
    Reeber, E., Sawada, J.: Combining ACL2 and an automated verification tool to verify a multiplier. In: Proceedings of the Sixth International Workshop on the ACL2 Theorem Prover and Its Applications, pp. 63–70. ACM (2006)Google Scholar
  33. 33.
    Sawada, J., Reeber, E.: ACL2SIX: a hint used to integrate a theorem prover and an automated verification tool. In: Formal Methods in Computer Aided Design, 2006. FMCAD ’06, pp. 161–170 (2006). doi: 10.1109/FMCAD.2006.3
  34. 34.
    Sawada, J., Gamboa, R.: Mechanical verification of a square root algorithm using Taylor’s theorem. In: Formal Methods in Computer-Aided Design, pp. 274–291. Springer (2002)Google Scholar
  35. 35.
    Sawada, J., Sandon, P., Paruthi, V., Baumgartner, J., Case, M., Mony, H.: Hybrid verification of a hardware modular reduction engine. In: Proceedings of the International Conference on Formal Methods in Computer-Aided Design, FMCAD Inc, Austin, TX, FMCAD ’11, pp. 207–214 (2011). http://dl.acm.org.ezproxy.lib.utexas.edu/citation.cfm?id=2157654.2157686
  36. 36.
    O’Leary, J.W., Russinoff, D.M.: Modeling algorithms in SystemC and ACL2. In: Verbeek, F., Schmaltz, J. (eds.) Proceedings Twelfth International Workshop on the ACL2 Theorem Prover and its Applications, Vienna, Austria, 12-13th July 2014, Open Publishing Association, Electronic Proceedings in Theoretical Computer Science, vol. 152, pp. 145–162 (2014). doi: 10.4204/EPTCS.152.12
  37. 37.
    Coglio, A.: Second-order functions and theorems in ACL2. In: Kaufmann, M., Rager, D.L. (eds.) Proceedings Thirteenth International Workshop on the ACL2 Theorem Prover and Its Applications, Austin, Texas, USA, 1-2 October 2015, Open Publishing Association, Electronic Proceedings in Theoretical Computer Science, vol. 192, pp. 17–33 (2015). doi: 10.4204/EPTCS.192.3
  38. 38.
    Selfridge, S., Smith, E.W.: Polymorphic types in ACL2. In: Verbeek, F., Schmaltz, J., (eds.) Proceedings Twelfth International Workshop on the ACL2 Theorem Prover and its Applications, Vienna, Austria, 12-13th July 2014, Open Publishing Association, Electronic Proceedings in Theoretical Computer Science, vol. 152, pp. 49–59 (2014). doi: 10.4204/EPTCS.152.4
  39. 39.
    Rager, D.L., Ebergen, J., Lee, A., Nadezhin, D., Selfridge, B., Chau, C.K.: A brief introduction to oracle’s use of ACL2 in verifying floating-point and integer arithmetic. In: Kaufmann, M., Rager, D.L. (eds.) Proceedings Thirteenth International Workshop on the ACL2 Theorem Prover and Its Applications, Austin, Texas, USA, 1-2 October 2015, Open Publishing Association, Electronic Proceedings in Theoretical Computer Science, vol. 192 (2015)Google Scholar
  40. 40.
    Greve, D.: Address enumeration and reasoning over linear address spaces. In: Fifth International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2-2004) (2004)Google Scholar
  41. 41.
    Greve, D., Richards, R., Wilding, M.: A summary of intrinsic partitioning verification. In: 5th International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2 2004), Austin, TX (2004)Google Scholar
  42. 42.
    Hardin, D.S., Smith, E.W., Young, W.D.: A robust machine code proof framework for highly secure applications. In: Proceedings of the Sixth International Workshop on the ACL2 Theorem Prover and Its Applications, pp. 11–20. ACM, New York, NY, USA, ACL2 ’06 (2006). doi: 10.1145/1217975.1217978
  43. 43.
    CLHS (Accessed: October, 2015) Common Lisp HyperSpec. http://www.lispworks.com/reference/HyperSpec/index.html
  44. 44.
  45. 45.
    Greve, D.A., Kaufmann, M., Manolios, P., Moore, J.S., Ray, S., Ruiz-Reina, J.-L., Sumners, R., Vroon, D., Wilding, M.: Efficient execution in an automated reasoning environment. J. Funct. Program. 18(1) (2008)Google Scholar
  46. 46.
    System Class Integer (Accessed: October, 2015) CLHS, Common Lisp HyperSpec. http://www.lispworks.com/documentation/HyperSpec/Body/t_intege.htm
  47. 47.
  48. 48.
    ACL2 Feature: Untouchable Functions (Accessed: October, 2015). See http://www.cs.utexas.edu/users/moore/acl2/manuals/current/manual/?topic=ACL2____PUSH-UNTOUCHABLE
  49. 49.
    The CompCert Project (Accessed: October, 2015). The CompCert C Compiler. http://compcert.inria.fr/compcert-C.html
  50. 50.
    Linux Memory Management (Accessed: October, 2015). Linux System Administrators Guide. http://www.tldp.org/LDP/sag/html/memory-management.html
  51. 51.
    McKusick, M.K., Neville-Neil, G.V., Watson, R.N.M.: Chapter 6: Memory Management. The Design and Implementation of the FreeBSD Operating System, Addison Wesley Professional (2014)Google Scholar
  52. 52.
    Kerrisk, M.: The Linux Programming Interface: A Linux and UNIX System Programming Handbook, 1st edn. No Starch Press, San Francisco (2010)Google Scholar
  53. 53.
    Windows Memory Management (Accessed: October, 2015.) Windows System Administrators Guide. http://msdn.microsoft.com/en-us/library/windows/desktop/aa366779(v=vs.85).aspx
  54. 54.
    Yu, D., Shao, Z.: Verification of safety properties for concurrent assembly code. In: Proceedings of 2004 International Conference on Functional Programming (ICFP’04) (2004)Google Scholar
  55. 55.
    Morrisett, G., Tan, G., Tassarotti, J., Tristan, J.-B., Gan, E.: RockSalt: better, faster, stronger SFI for the x86. In: Proceedings of the 33rd ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 395–404. ACM, PLDI ’12 (2012). doi: 10.1145/2254064.2254111
  56. 56.
    Myreen, M.O.: Formal Verification of Machine-code Programs. PhD thesis, University of Cambridge, Computer Laboratory, Trinity College (2008). http://www.cl.cam.ac.uk/~mom22/thesis.pdf
  57. 57.
    Smith, E.W.: Axe, An Automated Formal Equivalence Checking Tool For Programs. PhD thesis, Department of Computer Science, Stanford University (2011)Google Scholar
  58. 58.
    Moore, J.S.: (Accessed: October, 2015) Codewalker. See https://github.com/acl2/acl2/books/projects/codewalker
  59. 59.
    Myreen, M.O., Gordon, M.J.C., Slind, K.: Decompilation into logic - improved. In: Formal Methods in Computer-Aided Design (FMCAD), 2012, pp. 78–81 (2012). http://www.cs.utexas.edu/~hunt/FMCAD/FMCAD12/016.pdf
  60. 60.
    Bellard, F.: QEMU, a fast and portable dynamic translator. In: USENIX Annual Technical Conference, FREENIX Track, pp. 41–46 (2005)Google Scholar
  61. 61.
    Lawton, K.P.: Bochs: A Portable PC Emulator for Unix/X. Linux J 1996(29es) (1996). http://dl.acm.org/citation.cfm?id=326350.326357
  62. 62.
    Unicorn (Accessed: October, 2015) Unicorn: Slides from BlackHat USA 2015. http://www.unicorn-engine.org/BHUSA2015-unicorn.pdf
  63. 63.
    AMD Manuals (Accessed: October, 2015.) AMD64 Architecture: Developer Guides, Manuals and ISA Documents. http://developer.amd.com/resources/documentation-articles/developer-guides-manuals/
  64. 64.
    Goel, S., Hunt Jr., W.A., Kaufmann, M.: Abstract stobjs and their application to ISA modeling. In: Proceedings of the ACL2 Workshop 2013, EPTCS 114, pp. 54–69 (2013). http://arxiv.org/pdf/1304.7858.pdf
  65. 65.
    Luk, C.-K., Cohn, R., Muth, R., Patil, H., Klauser, A., Lowney, G., Wallace, S., Reddi, V.J., Hazelwood, K.: Pin: Building Customized Program Analysis Tools with Dynamic Instrumentation. SIGPLAN Not 40(6), 190–200 (2005). doi: 10.1145/1064978.1065034
  66. 66.
    Kaufmann, M., Hunt Jr., W.A.: Towards a Formal Model of the x86 ISA. Technical report, Department of Computer Science, University of Texas at Austin, Technical Report TR-12-07 (May 2012). see http://apps.cs.utexas.edu/tech_reports/reports/tr/TR-2075.pdf
  67. 67.
    Moore, J.S.: (Accessed: October, 2015.) Mechanized Operational Semantics. Lectures in the Marktoberdorf Summer School (August 5-16, 2008). See http://www.cs.utexas.edu/users/moore/publications/talks/marktoberdorf-08/index.html
  68. 68.
    Boyer, R.S., Moore, J.S.: Single-threaded Objects in ACL2. In: Krishnamurthy, S., Ramakrishnan, C.R. (eds.) Practical Aspects of Declarative Languages (PADL), vol. 2257, pp. 9–27. Springer, LNCS (2002)Google Scholar
  69. 69.
    Hunt Jr., W.A., Kaufmann, M.: A formal model of a large memory that supports efficient execution. In: Proceedings of the 12th International Conference on Formal Methods in Computer-Aided Design (FMCAD 2012, Cambrige, UK, October 22–25) (2012). http://www.cs.utexas.edu/~hunt/FMCAD/FMCAD12/014.pdf
  70. 70.
  71. 71.
    Kaufmann, M., Sumners, R.: Efficient rewriting of operations on finite structures in ACL2. In: ETAPS 2002: European joint conference on theory and practice of software. Satellite workshop, pp. 141–150 (2002)Google Scholar
  72. 72.
    Greve, D.: Scalable normalization for heap manipulating functions. In: ACL2 Workshop 2007 (2007). http://www.cs.uwyo.edu/~ruben/acl2-07/uploads/Main/017.pdf
  73. 73.
    Goel, S., Hunt Jr., W.A., Kaufmann, M., Ghosh, S.: 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 (FMCAD’14), pp. 18:91–98 (2014). http://dl.acm.org/citation.cfm?id=2682923.2682944
  74. 74.
    Bitops (Accessed: October, 2015) An ACL2 Library for Reasoning about Bit-Vector Arithmetic. See http://www.cs.utexas.edu/users/moore/acl2/manuals/current/manual/?topic=ACL2____BITOPS
  75. 75.
    Rager D.L.: (Accessed: October, 2015.) Maintaining community [in] sanity with Jenkins and Github. ACL2 Workshop 2015, Rump Session Talk. See https://www.cs.utexas.edu/users/moore/acl2/workshop-2015/rump-session-abstracts.html#rager and http://leeroy.defthm.com/
  76. 76.
    Matz, M., Hubicka, J., Jaeger, A., Mitchell, M.: Chapter 4: Object Files in System V Application Binary Interface. AMD64 Architecture Processor Supplement, Draft v0 99 (2005)Google Scholar
  77. 77.
    Mach-O File Format (Accessed: October, 2015.) OS X ABI Mach-O File Format Reference. Mac Developer Library. https://developer.apple.com/library/mac/documentation/DeveloperTools/Conceptual/MachORuntime/index.html
  78. 78.
    Swords, S., Davis, J.: Bit-blasting ACL2 theorems. In: Proceedings 10th International Workshop on the ACL2 Theorem Prover and its Applications, ACL2 2011, Austin, Texas, USA, November 3–4, 2011, pp. 84–102 (2011). doi: 10.4204/EPTCS.70.7
  79. 79.
    Anderson, S.: (Accessed: 2015) Bit Twiddling Hacks. See http://graphics.stanford.edu/~seander/bithacks.html
  80. 80.
    Goel, S., Hunt Jr., W.A.: Automated code proofs on a formal model of the x86. In: Verified Software: Theories, Tools, Experiments (VSTTE’13). Lecture Notes in Computer Science, vol. 8164, pp. 222–241. Springer, Berlin, Heidelberg (2014). doi: 10.1007/978-3-642-54108-7_12
  81. 81.
    Moore, J.S.: Stateman: using metafunctions to manage large terms representing machine states. In: Kaufmann, M., Rager, D.L. (eds.) Proceedings Thirteenth International Workshop on the ACL2 Theorem Prover and Its Applications, Austin, Texas, USA, 1-2 October 2015, Open Publishing Association, Electronic Proceedings in Theoretical Computer Science, vol. 192, pp. 93–109 (2015). doi: 10.4204/EPTCS.192.8
  82. 82.
    Turing, A.M.: Checking a Large Routine, pp. 67–69 (1949). http://www.turingarchive.org/browse.php/B/8
  83. 83.
    Hunt Jr., W.A.: Microprocessor design verification. J. Autom. Reason. 5(4), 429–460 (1989). http://www.cs.utexas.edu/~boyer/ftp/cli-reports/048.pdf
  84. 84.
    Moore, J.S.: Piton: A Mechanically Verified Assembly-Level Language. Automated Reasoning Series. Kluwer Academic Publishers (1996)Google Scholar
  85. 85.
    Young, William D.: A mechanically verified code generator. J. Autom. Reason. 5(4), 493–518 (1989)CrossRefGoogle Scholar
  86. 86.
    Boyer, R.S., Yu, Y.: Automated proofs of object code for a widely used microprocessor. J. ACM 43(1), 166–192 (1996). http://dl.acm.org/citation.cfm?id=227603
  87. 87.
    Bryant, R.E., O’Hallaron, D.R.: Chapter 4: Processor Architecture, of Computer Systems: A Programmer’s Perspective. Prentice-Hall (2003)Google Scholar
  88. 88.
    Goel, S., Hunt Jr., W.A., Kaufmann, M., Krug, R.: (Accessed: 2015) y86 Specifications in the ACL2 Community Books. See https://github.com/acl2/acl2/tree/master/books/models/y86
  89. 89.
    Greve, D.A.: Symbolic simulation of the JEM1 microprocessor. In: Gopalakrishnan, G., Windley, P., (eds.) Formal Methods in Computer-Aided Design. Lecture Notes in Computer Science, vol. 1522, pp. 321–333. Springer, Berlin, Heidelberg (1998). doi: 10.1007/3-540-49519-3_21
  90. 90.
    Owre, S., Rushby, J.M., Shankar, N.: PVS: a prototype verification system. In: Kapur, D. (ed.) 11th International Conference on Automated Deduction (CADE). Lecture Notes in Artificial Intelligence, vol. 607, pp. 748–752. Springer, Saratoga, NY (1992)Google Scholar
  91. 91.
    Greve, D., Wilding, M., Hardin, D.: High-speed, analyzable simulators. In: Computer-Aided Reasoning, pp. 113–135. Springer (2000)Google Scholar
  92. 92.
    Wilding, M., Greve, D., Hardin, D.: Efficient simulation of formal processor models. Form. Methods Syst. Des. 18(3), 233–248 (2001)CrossRefzbMATHGoogle Scholar
  93. 93.
    Fox, A.: Formal specification and verification of ARM6. In: Theorem Proving in Higher Order Logics, pp. 25–40. Springer (2003)Google Scholar
  94. 94.
    Alglave, J., Fox, A., Ishtiaq, S., Myreen, M.O., Sarkar, S., Sewell, P., Nardelli, F.Z.: The semantics of power and ARM multiprocessor machine code. In: Proceedings of DAMP 2009: the 4th Workshop on Declarative Aspects of Multicore Programming, ACM, New York, NY, USA, 553091 (2009)Google Scholar
  95. 95.
    Sewell, P., Sarkar, S., Owens, S., Zappa Nardelli, F., Myreen, M.O.: x86-TSO: a rigorous and usable programmer’s model for x86 multiprocessors. Commun. ACM 53(7), 89–97 (2010) (Research Highlights)Google Scholar
  96. 96.
    Owens, S., Sarkar, S., Sewell, P.: A better x86 memory model: x86-TSO. In: Proceedings of TPHOLs 2009: Theorem Proving in Higher Order Logics, LNCS 5674, pp. 391–407 (2009)Google Scholar
  97. 97.
    Sarkar, S., Sewell, P., Zappa Nardelli, F., Owens, S., Ridge, T., Braibant, T., Myreen, M., Alglave, J.: The semantics of x86-CC multiprocessor machine code. In: Proceedings of POPL 2009: the 36th annual ACM SIGPLAN-SIGACT symposium on Principles of Programming Languages, pp. 379–391 (2009). doi: 10.1145/1594834.1480929
  98. 98.
    Gordon, M.J.C., Melham, T.F. (eds.): Introduction to HOL: A Theorem-Proving Environment for Higher-Order Logic. Cambridge University Press, Cambridge (1993)Google Scholar
  99. 99.
    Fox, A., Myreen, M.O.: A trustworthy monadic formalization of the ARMv7 instruction set architecture. In: Kaufmann, M., Paulson, L.C., (eds.) Interactive Theorem Proving, Lecture Notes in Computer Science, vol. 6172, pp. 243–258. Springer, Berlin (2010). doi: 10.1007/978-3-642-14052-5_18
  100. 100.
    Myreen, M.O., Gordon, M., Slind, K.: Machine-code verification for multiple architectures - an application of decompilation into logic. In: Formal Methods in Computer-Aided Design, 2008. FMCAD ’08, pp. 1–8 (2008). doi: 10.1109/FMCAD.2008.ECP.24, http://www.cl.cam.ac.uk/~mom22/decomp.pdf
  101. 101.
    Klein, G., Elphinstone, K., Heiser, G., Andronick, J., Cock, D., Derrin, P., Elkaduwe, D., Engelhardt, K., Kolanski, R., Norrish, M., et al.: seL4: formal verification of an OS kernel. In: Proceedings of the ACM SIGOPS 22nd Symposium on Operating Systems Principles, pp. 207–220. ACM (2009). http://www.sigops.org/sosp/sosp09/papers/klein-sosp09.pdf
  102. 102.
    sel4: General Dynamics C4 Systems (Accessed: October, 2015). http://sel4.systems/
  103. 103.
    Morrisett, G.: Scalable formal machine models. In: Proceedings of the Second International Conference on Certified Programs and Proofs, pp. 1–3. Springer, Berlin, Heidelberg, CPP’12 (2012). doi 10.1007/978-3-642-35308-6_1
  104. 104.
    Coq Proof Assistant (Accessed: October, 2015). http://coq.inria.fr/
  105. 105.
    Feng, X., Shao, Z., Guo, Y., Dong, Y.: Certifying low-level programs with hardware interrupts and preemptive threads. J. Autom. Reason. 42(2), 301–347 (2009). http://flint.cs.yale.edu/flint/publications/aimjar.pdf
  106. 106.
    Shao, Z.: Clean-slate development of certified OS kernels. In: Proceedings of the 2015 Workshop on Certified Programs and Proofs, pp. 95–96. ACM, New York, NY, USA, CPP ’15 (2015). doi: 10.1145/2676724.2693180
  107. 107.
    Fox, A.: Directions in ISA Specification. Interactive Theorem Proving (ITP), pp. 338–344 (2012). https://www.cl.cam.ac.uk/~acjf3/papers/itp12.pdf
  108. 108.
    Degenbaev, U.: Formal Specification of the x86 Instruction Set Architecture. PhD thesis, Universität des Saarlandes (2012). http://rg-master.cs.uni-sb.de/publikationen/UD11.pdf
  109. 109.
    Shi, X.: Certification of an instruction set simulator. PhD thesis, Université de Grenoble (2013)Google Scholar
  110. 110.
    Leroy, X.: Formal verification of a realistic compiler. Commun. ACM 52(7), 107–115 (2009). http://gallium.inria.fr/~xleroy/publi/compcert-CACM.pdf
  111. 111.
    Bjørner, D.: A ProCoS project description. International Conference on AI and Robotics, North Holland (1989)Google Scholar
  112. 112.
    Bowen, J.P.: A ProCoS II project description: ESPRIT Basic Research project 7071. Bull. Eur. Assoc. Theor. Comput. Sci. (EATCS) 50, 128–137 (1993)zbMATHGoogle Scholar

Copyright information

© Springer International Publishing AG 2017

Authors and Affiliations

  • Shilpi Goel
    • 1
    Email author
  • Warren A. HuntJr.
    • 1
  • Matt Kaufmann
    • 1
  1. 1.Department of Computer ScienceThe University of Texas at AustinAustinUSA

Personalised recommendations