Model Checking Speculation-Dependent Security Properties: Abstracting and Reducing Processor Models for Sound and Complete Verification

  • Gianpiero Cabodi
  • Paolo Camurati
  • Fabrizio Finocchiaro
  • Danilo VendraminettoEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11445)


Though modern microprocessors embed several hardware security mechanisms, aimed at guaranteeing confidentiality and integrity of sensible data, recently disclosed attacks such as Spectre and Meltdown witness weaknesses with potentially great impact on CPU security. Both vulnerabilities exploit speculative execution of modern high-performance micro-architectures, allowing the attacker to observe data leaked via a memory side channel, during speculated and mispredicted instructions.

In this paper we present a methodology to formally verify, by means of a model checker, speculative vulnerabilities, such as the class of Spectre/Meltdown attacks, in microprocessors based on speculative execution. In detail, we discuss the problem of formally verifying confidentiality violations, since we deem it will help preventing new vulnerabilities of the same typology.

We describe our methodology on a pipelined CPU inspired by the DLX RISC processor architecture. Due to scalability issues, and following related approaches in formal verification of correctness, our approach simplifies the model under verification by proper abstraction and reduction steps. The approach is based on flushing the pipeline, abstracting data and most of the speculative execution logic, keeping a subset of control data, plus speculated data state and tainting logic. Illegal propagation (data leakage) is encoded in terms of taint propagation, from a protected/invalid memory address to the address bus on a subsequent memory read, affecting the cache.

We introduce the theoretical flow, relying on known theoretical results combined and exploited to prove soundness and completeness. Finally, using a state-of-the-art model checking tool, we present preliminary data on formal verification based on Bounded Model Checking, that to support our claims and highlight the feasibility of the approach.


Model checking Secure CPU architecture Speculative execution Taint propagation Abstraction and reduction Pipeline flushing Confidentiality Reorder buffer Spectre Meltdown 


  1. 1.
    Cabodi, G., Palena, M., Pasini, P.: Interpolation with guided refinement: revisiting incrementality in SAT-based unbounded model checking. In: Formal Methods in Computer-Aided Design (FMCAD), pp. 43–50. IEEE (2014)Google Scholar
  2. 2.
    Beckers, K., Heisel, M., Hatebur, D.: Pattern and Security Requirements. Springer, Cham (2015). Scholar
  3. 3.
    Biere, A., Heljanko, K., Wieringa, S.: Aiger 1.9 and beyond. (2011)
  4. 4.
    Boritz, J.E.: Is practitioners’ views on core concepts of information integrity. Int. J. Acc. Inf. Syst. 6(4), 260–279 (2005)CrossRefGoogle Scholar
  5. 5.
    Bryant, R.E., Lahiri, S.K., Seshia, S.A.: Modeling and verifying systems using a logic of counter arithmetic with lambda expressions and uninterpreted functions. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 78–92. Springer, Heidelberg (2002). Scholar
  6. 6.
    Burch, J.R., Dill, D.L.: Automatic verification of pipelined microprocessor control. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol. 818, pp. 68–80. Springer, Heidelberg (1994). Scholar
  7. 7.
    Cabodi, G., Camurati, P., Finocchiaro, S., Loiacono, C., Savarese, F., Vendraminetto, D.: Secure embedded architectures: taint properties verification. In: 2016 International Conference on Development and Application Systems (DAS), pp. 150–157. IEEE (2016)Google Scholar
  8. 8.
    Cabodi, G., Camurati, P., Finocchiaro, S.F., Savarese, F., Vendraminetto, D.: Embedded systems secure path verification at the hardware/software interface. IEEE Des. Test 34(5), 38–46 (2017)CrossRefGoogle Scholar
  9. 9.
    Cabodi, G., Camurati, P., Garcia, L., Murciano, M., Nocco, S., Quer, S.: Speeding up model checking by exploiting explicit and hidden verification constraints. In: Design, Automation and Test in Europe, DATE 2009, Nice, France, 20–24 April 2009, pp. 1686–1691. IEEE (2009)Google Scholar
  10. 10.
    Cabodi, G., Loiacono, C., Vendraminetto, D.: Optimization techniques for craig interpolant compaction in unbounded model checking. In: Proceedings of DATE, pp. 1417–1422. Grenoble, France (Mar 2013)Google Scholar
  11. 11.
    Cabodi, G., Nocco, S.: Optimized model checking of multiple properties. In: Design, Automation and Test in Europe, DATE 2011, Grenoble, France, March 14-18, 2011. pp. 543–546. IEEE (2011)Google Scholar
  12. 12.
    Cabodi, G., Nocco, S., Quer, S.: Strengthening model checking techniques with inductive invariants. IEEE Trans. CAD Integr. Circuits Syst. 28(1), 154–158 (2009)CrossRefGoogle Scholar
  13. 13.
    Cabodi, G., Nocco, S., Quer, S.: Benchmarking a model checker for algorithmic improvements and tuning for performance. Form. Methods Syst. Des. 39(2), 205–227 (2011)CrossRefGoogle Scholar
  14. 14.
    Fan, J., Guo, X., De Mulder, E., Schaumont, P., Preneel, B., Verbauwhede, I.: State-of-the-art of secure ECC implementations: a survey on known side-channel attacks and countermeasures. In: 2010 IEEE International Symposium on Hardware-Oriented Security and Trust (HOST), pp. 76–87. IEEE (2010)Google Scholar
  15. 15.
    Hanna, Z.: Jasper case study on formally verifying secure on-chip datapaths (2013).
  16. 16.
    Hunt, W.A.: Microprocessor design verification. J. Autom. Reason. 5(4), 429–460 (1989)CrossRefGoogle Scholar
  17. 17.
    Hunt, W.A. (ed.): FM8501: A Verified Microprocessor. LNCS, vol. 795. Springer, Heidelberg (1994). Scholar
  18. 18.
    Jhala, R., McMillan, K.L.: Microarchitecture verification by compositional model checking. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 396–410. Springer, Heidelberg (2001). Scholar
  19. 19.
    Joy Persial, G., Prabhu, M., Shanmugalakshmi, R.: Side channel attack-survey. Int. J. Adv. Sci. Res. Rev. 1(4), 54–57 (2011)Google Scholar
  20. 20.
    Kocher, P., et al.: Spectre attacks: exploiting speculative execution. arXiv preprint arXiv:1801.01203 (2018)
  21. 21.
    Lipp, M., et al.: Meltdown. arXiv preprint arXiv:1801.01207 (2018)
  22. 22.
    Lowe-Power, J., Akella, V., Farrens, M.K., King, S.T., Nitta, C.J.: A case for exposing extra-architectural state in the ISA: position paper. In: Proceedings of the 7th International Workshop on Hardware and Architectural Support for Security and Privacy, p. 8. ACM (2018)Google Scholar
  23. 23.
    Manolios, P.: Correctness of pipelined machines. In: Hunt, W.A., Johnson, S.D. (eds.) FMCAD 2000. LNCS, vol. 1954, pp. 181–198. Springer, Heidelberg (2000). Scholar
  24. 24.
    Manolios, P.: Mechanical verification of reactive systems. Ph.D. thesis, The University of Texas at Austin, Department of Computer Sciences, Austin, TX (2001)Google Scholar
  25. 25.
    Manolios, P., Srinivasan, S.K.: Automatic verification of safety and liveness for xscale-like processor models using web refinements. In: Design, Automation and Test in Europe Conference and Exhibition, 2004, Proceedings, vol. 1, pp. 168–173. IEEE (2004)Google Scholar
  26. 26.
    Manolios, P., Srinivasan, S.K.: A complete compositional reasoning framework for the efficient verification of pipelined machines. In: IEEE/ACM International Conference on Computer-Aided Design, 2005, ICCAD-2005, pp. 863–870. IEEE (2005)Google Scholar
  27. 27.
    Manolios, P., Srinivasan, S.K.: Verification of executable pipelined machines with bit-level interfaces. In: Proceedings of the 2005 IEEE/ACM International Conference on Computer-Aided Design. IEEE Computer Society (2005)Google Scholar
  28. 28.
    Patterson, D.A., Hennessy, J.L., Goldberg, D.: Computer Architecture: A Quantitative Approach, vol. 2. Morgan Kaufmann, San Mateo (1990)Google Scholar
  29. 29.
    Skakkebæk, J.U., Jones, R.B., Dill, D.L.: Formal verification of out-of-order execution using incremental flushing. In: Hu, A.J., Vardi, M.Y. (eds.) CAV 1998. LNCS, vol. 1427, pp. 98–109. Springer, Heidelberg (1998). Scholar
  30. 30.
    Subramanyan, P., Arora, D.: Formal verification of taint-propagation security properties in a commercial SOC design. In: Proceedings of the Conference on Design, Automation & Test in Europe, p. 313. European Design and Automation Association (2014)Google Scholar
  31. 31.
    Subramanyan, P., Malik, S., Khattri, H., Maiti, A., Fung, J.: Verifying information flow properties of firmware using symbolic execution. In: Design, Automation & Test in Europe Conference & Exhibition (DATE), 2016, pp. 337–342. IEEE (2016)Google Scholar
  32. 32.
    Tomasulo, R.M.: An efficient algorithm for exploiting multiple arithmetic units. IBM J. Res. Dev. 11(1), 25–33 (1967)CrossRefGoogle Scholar
  33. 33.
    Zhou, Y., Feng, D.: Side-channel attacks: ten years after its publication and the impacts on cryptographic module security testing. IACR Cryptol. ePrint Arch. 2005, 388 (2005)Google Scholar

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  • Gianpiero Cabodi
    • 1
  • Paolo Camurati
    • 1
  • Fabrizio Finocchiaro
    • 1
  • Danilo Vendraminetto
    • 1
    Email author
  1. 1.Dip. di Automatica e InformaticaPolitecnico di TorinoTurinItaly

Personalised recommendations