. .. , 10 2.2 Standard registers of PCI Type 0 (Non-Bridge) Configuration Space Header

, Typical caches organization of a x86 processor

, The Write-Back cache strategy

, A simple airlock system modeled as a labeled transition system, p.29

, From the processor to the flash memory

. .. , Pre and postconditions for Minx86 ReceiveSMI transitions, p.73

, Raw postcondition of a Write transition with a writeback strategy, p.79

, Postcondition of a Write transition with a writeback strategy, after the use of the remember tactic

, Exploring alternative paths using the destruct tactics

. .. , 5 Intermediary statements, generated using assert tactics, p.81

, Dividing a transition into sequences of intermediary states updates, p.81

. .. , Sequence diagram of the execution of movq $0, (%rax), vol.87

, Interface-driven modeling of the x86 architecture

, The memory controller in isolation

, The cache in isolation

. .. L-s-), List of labels dedicated to Minx86 software transitions, p.71

. .. L-h-), 72 Bibliography

X. Kovah, C. Kallenberg, J. Butterworth, S. Cornwell, and . Senter-sandman, Using Intel TXT to Attack Bioses. Hack in the Box, 2015.

. Intel, Intel Trusted Execution Technology (Intel TXT), vol.07, 2015.

M. Jeannette and . Wing, A Call to Action: Look beyond the Horizon, IEEE Security & Privacy, issue.6, pp.62-67, 2003.

L. Duflot, O. Levillain, B. Morin, and O. Grumelard, Getting into the SMRAM: SMM Reloaded. CanSecWest

R. Wojtczuk and J. Rutkowska, Attacking SMM Memory via Intel CPU Cache Poisoning

C. Domas, The Memory Sinkhole, 2015.

C. Kallenberg and R. Wojtczuk, Speed Racer: Exploiting an Intel Flash Protection Race Condition, 2015.

U. Stern, L. David, and . Dill, Automatic Verification of the SCI Cache Coherence Protocol, Advanced Research Working Conference on Correct Hardware Design and Verification Methods, pp.21-34, 1995.

M. Vijayaraghavan, A. Chlipala, and N. Dave, Modular Deductive Verification of Multiprocessor Hardware Designs, International Conference on Computer Aided Verification, pp.109-127, 2015.

J. Choi, M. Vijayaraghavan, B. Sherman, and A. Chlipala, A Platform for High-Level Parametric Hardware Specification and Its Modular Verification, Proceedings of the ACM on Programming Languages, vol.1, p.24, 2017.

N. Jomaa, D. Nowak, G. Grimaud, and S. Hym, Formal Proof of Dynamic Memory Isolation Based on MMU, Theoretical Aspects of Software Engineering (TASE), pp.73-80, 2016.
URL : https://hal.archives-ouvertes.fr/hal-01369769

, The Pip Development Team. The pip protokernel

D. Garg, J. Franklin, D. Kaynar, and A. Datta, Compositional System Security with Interface-Confined Adversaries. Electronic Notes in Theoretical Computer Science, vol.265, pp.49-71, 2010.

T. Heyman, R. Scandariato, and W. Joosen, Reusable Formal Models for Secure Software Architectures, Software Architecture (WICSA) and European Conference on Software Architecture (ECSA), 2012 Joint Working IEEE/IFIP Conference on, pp.41-50, 2012.

T. Letan, P. Chifflier, G. Hiet, P. Néron, and B. Morin, SpecCert: Specifying and Verifying Hardware-based Security Enforcement, 21st International Symposium on Formal Methods (FM, 2016.
URL : https://hal.archives-ouvertes.fr/hal-01356690

T. Letan, Y. Régis-gianas, P. Chifflier, and G. Hiet, Modular Verification of Programs with Effects and Effect Handlers, 28st International Symposium on Formal Methods (FM, 2018.
URL : https://hal.archives-ouvertes.fr/hal-01799712

L. Lamport, Proving the Correctness of Multiprocess Programs, IEEE transactions on software engineering, issue.2, pp.125-143, 1977.

L. Lamport, Logical Foundation. Distributed systems-methods and tools for specification, vol.190, pp.119-130, 1985.

F. B. Bowen-alpern and . Schneider, Defining Liveness, 1985.

R. Michael, F. B. Clarkson, and . Schneider, Hyperproperties. Journal of Computer Security, vol.18, issue.6, pp.1157-1210, 2010.

T. Letan, FreeSpec: a Compositional Reasoning Framework for the Coq Theorem Prover

. Inria, The Coq Proof Assistant

J. Simon-peyton, Tackling the Awkward Squad: monadic I/O, concurrency, exception and foreign-language calls in Haskell. Engineering theories of software construction, pp.47-96, 2005.

A. Bauer and M. Pretnar, Programming with Algebraic Effects and Handlers, Journal of Logical and Algebraic Methods in Programming, vol.84, issue.1, pp.108-123, 2015.

K. Yang, M. Hicks, Q. Dong, T. Austin, and D. Sylvester, A2: Analog Malicious Hardware, Security and Privacy (SP), 2016 IEEE Symposium on, pp.18-37, 2016.

S. Embleton, S. Sparks, and C. C. Zou, SMM rootkit: a new breed of OS independent malware, vol.6, pp.1590-1605, 2013.

Y. Bulygin, A. Loucaides, . Furtak, A. Bazhaniuk, and . Matrosov, Summary of Attacks Against BIOS and Secure Boot, Proceedings of the DefCon, 2014.

. Intel, Intel 64 and IA32 Architectures Software Developer Manual, chapter Introduction to Virtual Machine Extensions, 2014.

. Intel, Intel 64 and IA32 Architectures Software Developer Manual, chapter Introduction to Intel Software Guard Extenions, 2014.

V. Costan and S. Devadas, Intel SGX Explained. IACR Cryptology ePrint Archive, p.86, 2016.

R. Wojtczuk and J. Rutkowska, Attacking Intel TXT via SINIT Code Execution Hijacking, 2011.

E. Fernand-lone-sang, V. Lacombe, Y. Nicomette, and . Deswarte, Exploiting an I/OMMU vulnerability, Malicious and Unwanted Software (MALWARE), 2010 5th International Conference on, pp.7-14, 2010.

. Intel, Intel 64 and IA32 Architectures Software Developer Manual, 2014.

. Intel, Intel 5100 Memory Controller Hub Chipset

, Intel. Intel 7 Series / C216 Chipset Family Platform Controller Hub (PCH)

T. Letan, SpecCert: a framework for the Coq Theorem Prover

E. Michael and . Thomadakis, The Architecture of the Nehalem Processor and Nehalem-EP SMP Platforms, Resource, vol.3, issue.2, 2011.

J. Turley, White Paper Introduction to Intel® Architecture, 2014.

D. Marr, F. Binns, G. Hill, . Hinton, and . Koufaty, Hyper-Threading Technology in the Netburst® Microarchitecture, 2002.

A. Fog, The Microarchitecture of Intel, AMD and VIA CPUs: An Optimization Guide for Assembly Programmers and Compiler Makers, 2012.

M. Milenkovic, A. Milenkovic, and J. Kulick, Demystifying Intel Branch Predictors, Workshop on Duplicating, Deconstructing and Debunking, 2002.

. Simon-p-johnson, R. Uday, . Savagaonkar, R. Vincent, . Scarlata et al., Technique for Supporting Multiple Secure Enclaves, US Patent, vol.8, p.746, 2015.

H. Jerome, M. Saltzer, and . Schroeder, The Protection of Information in Computer Systems, Proceedings of the IEEE, vol.63, pp.1278-1308, 1975.

D. Abramson, J. Jackson, S. Muthrasanallur, G. Neiger, G. Regnier et al., Intel Virtualization Technology for Directed I/O, Intel technology journal, vol.10, issue.3, 2006.

M. Daubignard and Y. Perez, ProTIP: You Should Know What to Expect From Your Peripherals. Symposium sur la sécurité des technologies de l'information et des communications (SSTIC), 2017.

K. Nohl and J. Lell, BadUSB -On Accessories That Turn Evil, 2014.

T. Hudson and L. Rudolph, Thunderstrike: EFI Firmware Bootkits for Apple MacBooks, Proceedings of the 8th ACM International Systems and Storage Conference, p.15, 2015.

P. Chifflier, UEFI et bootkits PCI: le danger vient d'en bas, Actes du 11ème symposium sur la sécurité des technologies de l'information et des communications (SSTIC), pp.159-190, 2013.

D. Salihun, BIOS Disassembly Ninjutsu Uncovered, 2006.

V. Zimmer, Platform Trust Beyond BIOS Using the Unified Extensible Firmware Interface, Security and Management, pp.400-405, 2007.

, Unified Extensible Firmware Interface (UEFI) Specification, Version 2.7 Errata A, UEFI Forum, 2017.

J. Rutkowska, Intel x86 Considered Harmful. the Invisible Things Lab, 2015.

L. Rosenbaum and V. Zimmer, A Tour Beyond BIOS into UEFI Secure Boot, 2012.

J. Corbet, Protecting systems with the TPM, 2016.

. Hp-inc, HP Sure Start: Automatic Firmware Intrusion Detection and Repair System, 2016.

A. Regenscheid, Platform Firmware Resiliency Guidelines, NIST Special Publication, vol.800, p.193, 2018.

, Advanced Configuration and Power Interface (ACPI) Specification, Version 6.2 Errata A, UEFI Forum, 2017.

L. Duflot, O. Grumelard, O. Levillain, and B. Morin, ACPI and SMI Handlers: Some Limits to Trusted Computing, Journal in computer virology, vol.6, issue.4, pp.353-374, 2010.

V. Zimmer, M. Rothman, and S. Marisetty, Beyond BIOS: Developing with the Unified Extensible Firmware Interface, 2017.

J. Yao, J. Vincent, Q. Zimmer, and . Long, System Management Mode Isolation in Firmware, p.446, 2009.

A. Gupta, Formal Hardware Verification Methods: A Survey, Computer-Aided Verification, pp.5-92, 1992.

R. Leslie-hurd, D. Caspi, and M. Fernandez, Verifying Linearizability of Intel® Software Guard Extensions, International Conference on Computer Aided Verification, pp.144-160, 2015.

D. Lie, J. Mitchell, A. Chandramohan, M. Thekkath, and . Horowitz, Specifying and Verifying Hardware for Tamper-Resistant Software, Proceedings. 2003 Symposium on, pp.166-177, 2003.

C. Loiseaux, S. Graf, J. Sifakis, A. Bouajjani, S. Bensalem et al., Property Preserving Abstractions for the Verification of Concurrent Systems. Formal methods in system design, vol.6, pp.11-44, 1995.

A. Cimatti, E. Clarke, E. Giunchiglia, F. Giunchiglia, M. Pistore et al., NuSMV2: An Opensource Tool for Symbolic Model Checking, International Conference on Computer Aided Verification, pp.359-364, 2002.

D. Jackson, Software Abstractions: Logic, Language and Analysis, 2012.

G. Barthe, G. Betarte, J. D. Campo, and C. Luna, Formally Verifying Isolation and Availability in an Idealized Model of Virtualization, International Symposium on Formal Methods, pp.231-245, 2011.

F. B. Bowen-alpern and . Schneider, Recognizing Safety and Liveness. Distributed computing, vol.2, issue.3, pp.117-126, 1987.

F. B. Schneider, Enforceable Security Policies, ACM Transactions on Information and System Security (TISSEC), vol.3, issue.1, pp.30-50, 2000.

D. Basin, V. Jugé, F. Klaedtke, and E. Z?linescu, Enforceable Security Policies Revisited. ACM Transactions on Information and System Security (TISSEC), vol.16, issue.1, p.3, 2013.

A. Joseph, J. Goguen, and . Meseguer, Security Policies and Security Models, Security and Privacy, 1982 IEEE Symposium on, pp.11-11, 1982.

M. Edmund, T. A. Clarke, H. Henzinger, and . Veith, Introduction to Model Checking, Handbook of Model Checking, pp.1-26, 2018.

P. Carla, H. Gomes, A. Kautz, B. Sabharwal, and . Selman, Satisfiability Solvers. Foundations of Artificial Intelligence, vol.3, pp.89-134, 2008.

M. Edmund, W. Clarke, M. Klieber, P. Nová?ek, and . Zuliani, Model Checking and the State Explosion Problem, Tools for Practical Software Verification, pp.1-30, 2012.

. Raymond-r-smullyan, First-Order Logic, vol.43, 2012.

S. Malik and L. Zhang, Boolean Satisfiability From Theoretical Hardness to Practical Success, Communications of the ACM, vol.52, issue.8, pp.76-82, 2009.

. Matthew-w-moskewicz, F. Conor, Y. Madigan, L. Zhao, S. Zhang et al., Chaff: Engineering an Efficient SAT Solver, Proceedings of the 38th annual Design Automation Conference, pp.530-535, 2001.

C. Barrett, M. Deters, L. D. Moura, A. Oliveras, and A. Stump, 6 Years of SMT-COMP, Journal of Automated Reasoning, vol.50, issue.3, pp.243-277, 2013.

L. De-moura and N. Bjørner, Z3: An efficient SMT solver, International conference on Tools and Algorithms for the Construction and Analysis of Systems, pp.337-340, 2008.

A. Chagrov, Modal Logic, 1997.

P. Sistla and E. M. Clarke, The Complexity of Propositional Linear Temporal Logics, Journal of the ACM (JACM), vol.32, issue.3, pp.733-749, 1985.

M. Edmund, E. Clarke, and . Emerson, Design and Synthesis of Synchronization Skeletons Using Branching Time Temporal Logic, Workshop on Logic of Programs, pp.52-71, 1981.

G. J. Holzmann, The Model Checker SPIN, IEEE Transactions on software engineering, vol.23, issue.5, pp.279-295, 1997.

L. Lamport, Specifying Systems: the TLA+ Language and Tools for Hardware and Software Engineers, 2002.

. Kenneth-l-mcmillan, Symbolic Model Checking, Verification of Digital and Hybrid Systems, pp.117-137, 2000.

A. Biere, A. Cimatti, E. M. Clarke, O. Strichman, and Y. Zhu, Bounded Model Checking. Advances in computers, vol.58, issue.11, pp.117-148, 2003.

D. Leivant, Higher Order Logic, 1994.

T. Nipkow, C. Lawrence, M. Paulson, and . Wenzel, Isabelle/HOL: a proof assistant for higher-order logic, vol.2283, 2002.

J. Abrial and J. Abrial, The B-book: Assigning Programs to Meanings, 2005.

L. De-moura, S. Kong, J. Avigad, F. Van-doorn, and J. V. Raumer, The Lean Theorem Prover (System Description), International Conference on Automated Deduction, pp.378-388, 2015.

J. Harrison, Formal Verification of IA-64 Division Algorithms, International Conference on Theorem Proving in Higher Order Logics, pp.233-251, 2000.

R. Kaivola, R. Ghughal, N. Narasimhan, A. Telfer, J. Whittemore et al., Replacing Testing with Formal Verification in Intel?{\scriptsize\circledR} CoreTM i7 Processor Execution Engine Validation, International Conference on Computer Aided Verification, pp.414-429, 2009.

N. Potlapally, Hardware Security in Practice: Challenges and Opportunities, Hardware-Oriented Security and Trust (HOST), 2011 IEEE International Symposium on, pp.93-98, 2011.

G. Morrisett, G. Tan, J. Tassarotti, J. Tristan, and E. Gan, RockSalt: Better, Faster, Stronger SFI for the x86, ACM SIGPLAN Notices, vol.47, pp.395-404, 2012.

S. Goel, A. Warren, M. Hunt, S. Kaufmann, and . Ghosh, Simulation And Formal Verification Of x86 Machine-Code Programs That Make System Calls, Formal Methods in Computer-Aided Design (FMCAD), pp.91-98, 2014.

X. Leroy, The CompCert Verified Compiler. Documentation and user's manual, 2012.
URL : https://hal.archives-ouvertes.fr/hal-01399482

R. Gu, Z. Shao, H. Chen, (. Xiongnan, ). Newman et al., CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels, OSDI, vol.16, pp.653-669, 2016.

X. Hao-chen, Z. Wu, J. Shao, R. Lockerman, and . Gu, Toward Compositional Verification of Interruptible OS Kernels and Device Drivers, Journal of Automated Reasoning, vol.61, issue.1-4, pp.141-189, 2018.

/. Data61 and . Csiro, The seL4 Microkernel

G. Klein, K. Elphinstone, G. Heiser, J. Andronick, D. Cock et al., Formal verification of an OS kernel, Proceedings of the ACM SIGOPS 22nd symposium on Operating systems principles, pp.207-220, 2009.

G. Barthe, G. Betarte, J. D. Campo, and C. Luna, Cache-Leakage Resilient OS Isolation in an Idealized Model of Virtualization, Computer Security Foundations Symposium (CSF), 2012 IEEE 25th, pp.186-197, 2012.

G. Barthe, G. Betarte, J. Campo, C. Luna, and D. Pichardie, Systemlevel Non-Interference for Constant-Time Cryptography, Proceedings of the 2014 ACM SIGSAC Conference on Computer and Communications Security, pp.1267-1279, 2014.
URL : https://hal.archives-ouvertes.fr/hal-01101950

A. Fox and . Magnus-o-myreen, A Trustworthy Monadic Formalization of the ARMv7 Instruction Set Architecture, International Conference on Interactive Theorem Proving, pp.243-258, 2010.

A. Reid, Trustworthy specifications of ARM® v8-A and v8-M system level architecture, Proceedings of the 16th Conference on Formal Methods in Computer-Aided Design, pp.161-168, 2016.

A. Reid, R. Chen, A. Deligiannis, D. Gilday, D. Hoyes et al., End-to-end Verification of Processors with ISA-Formal, International Conference on Computer Aided Verification, pp.42-58, 2016.

. Arm-ltd, A64 ISA XML for Armv8, vol.4, 2018.

D. Lie, C. Thekkath, M. Mitchell, P. Lincoln, D. Boneh et al., Architectural Support for Copy and Tamper Resistant Software, ACM SIGPLAN Notices, vol.35, issue.11, pp.168-177, 2000.

A. Pnueli, In Transition from Global to Modular Temporal Reasoning about Programs, Logics and models of concurrent systems, pp.123-144, 1985.

C. B. Jones, Tentative Steps Toward a Development Method for Interfering Programs, ACM Transactions on Programming Languages and Systems (TOPLAS), vol.5, issue.4, pp.596-619, 1983.

T. A. Luca-de-alfaro and . Henzinger, Interface Automata. In ACM SIGSOFT Software Engineering Notes, vol.26, pp.109-120, 2001.

R. Milner, A Calculus of Communicating Systems, LNCS, vol.92, 1980.

C. Hoare, Communicating Sequential Processes, Communications of the ACM, vol.21, issue.8, pp.666-677, 1978.

R. Nikhil, Bluespec System Verilog: efficient, correct RTL from high level specifications. In Formal Methods and Models for Co-Design, MEMOCODE'04. Proceedings. Second ACM and IEEE International Conference on, pp.69-70, 2004.

L. Lamport, How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Progranm, IEEE transactions on computers, issue.9, pp.690-691, 1979.

J. Souquieres, Verifying the Compatibility of Component Interfaces using the B Formal Method. Software Engineering Research and Practice, pp.850-856, 2005.

S. Chouali, M. Heisel, and J. Souquières, Proving Component Interoperability with B Refinement, Electronic Notes in Theoretical Computer Science, vol.160, pp.157-172, 2006.
URL : https://hal.archives-ouvertes.fr/inria-00000171

A. Lanoix and J. Souquières, Component-based Development using the B method, 2006.
URL : https://hal.archives-ouvertes.fr/hal-00105041

G. Claret and . Coq,

P. Wadler, Comprehending Monads, Proceedings of the 1990 ACM conference on LISP and functional programming, pp.61-78, 1990.

M. Hyland, G. Plotkin, and J. Power, Combining Effects: Sum and Tensor, Theoretical Computer Science, vol.357, issue.1-3, pp.70-99, 2006.

S. Liang, P. Hudak, and M. Jones, Monad Transformers and Modular Interpreters, Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pp.333-343, 1995.

E. Brady, Programming and Reasoning with Algebraic Effects and Dependent Types, ACM SIGPLAN Notices, vol.48, pp.133-144, 2013.

O. Kiselyov, A. Sabry, and C. Swords, Extensible Effects: An Alternative To Monad Transformers, ACM SIGPLAN Notices, vol.48, pp.59-70, 2013.

J. Rutkowska and R. Wojtczuk, Preventing and Detecting Xen Hypervisor Subversions, Blackhat Briefings USA, 2008.

. Intel, Desktop 4th Generation Intel Core Processor Family, Desktop Intel Pentium Processor Family, and Desktop Intel Celeron Processor Family

P. Müller, A. Poetzsch-heffter, and G. T. Leavens, Modular Invariants for Layered Object Structures, Science of Computer Programming, vol.62, issue.3, pp.253-286, 2006.

H. Apfelmus, The operational package, 2010.

. Car-hoareetal, Tackling the Awkward Squad: monadic input/output, concurrency, exceptions, and foreign-language calls in Haskell. Engineering theories of software construction, 2001.

J. Gaisler, . Leon, and . Processor, The Past, Present and Future, 2007.