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
List of labels dedicated to Minx86 software transitions, p.71 ,
72 Bibliography ,
, Using Intel TXT to Attack Bioses. Hack in the Box, 2015.
Intel Trusted Execution Technology (Intel TXT), vol.07, 2015. ,
A Call to Action: Look beyond the Horizon, IEEE Security & Privacy, issue.6, pp.62-67, 2003. ,
Getting into the SMRAM: SMM Reloaded. CanSecWest ,
Attacking SMM Memory via Intel CPU Cache Poisoning ,
The Memory Sinkhole, 2015. ,
Speed Racer: Exploiting an Intel Flash Protection Race Condition, 2015. ,
Automatic Verification of the SCI Cache Coherence Protocol, Advanced Research Working Conference on Correct Hardware Design and Verification Methods, pp.21-34, 1995. ,
Modular Deductive Verification of Multiprocessor Hardware Designs, International Conference on Computer Aided Verification, pp.109-127, 2015. ,
A Platform for High-Level Parametric Hardware Specification and Its Modular Verification, Proceedings of the ACM on Programming Languages, vol.1, p.24, 2017. ,
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
, Compositional System Security with Interface-Confined Adversaries. Electronic Notes in Theoretical Computer Science, vol.265, pp.49-71, 2010.
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. ,
SpecCert: Specifying and Verifying Hardware-based Security Enforcement, 21st International Symposium on Formal Methods (FM, 2016. ,
URL : https://hal.archives-ouvertes.fr/hal-01356690
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
Proving the Correctness of Multiprocess Programs, IEEE transactions on software engineering, issue.2, pp.125-143, 1977. ,
Logical Foundation. Distributed systems-methods and tools for specification, vol.190, pp.119-130, 1985. ,
Defining Liveness, 1985. ,
, Hyperproperties. Journal of Computer Security, vol.18, issue.6, pp.1157-1210, 2010.
FreeSpec: a Compositional Reasoning Framework for the Coq Theorem Prover ,
The Coq Proof Assistant ,
Tackling the Awkward Squad: monadic I/O, concurrency, exception and foreign-language calls in Haskell. Engineering theories of software construction, pp.47-96, 2005. ,
Programming with Algebraic Effects and Handlers, Journal of Logical and Algebraic Methods in Programming, vol.84, issue.1, pp.108-123, 2015. ,
A2: Analog Malicious Hardware, Security and Privacy (SP), 2016 IEEE Symposium on, pp.18-37, 2016. ,
SMM rootkit: a new breed of OS independent malware, vol.6, pp.1590-1605, 2013. ,
Summary of Attacks Against BIOS and Secure Boot, Proceedings of the DefCon, 2014. ,
Intel 64 and IA32 Architectures Software Developer Manual, chapter Introduction to Virtual Machine Extensions, 2014. ,
Intel 64 and IA32 Architectures Software Developer Manual, chapter Introduction to Intel Software Guard Extenions, 2014. ,
, Intel SGX Explained. IACR Cryptology ePrint Archive, p.86, 2016.
Attacking Intel TXT via SINIT Code Execution Hijacking, 2011. ,
Exploiting an I/OMMU vulnerability, Malicious and Unwanted Software (MALWARE), 2010 5th International Conference on, pp.7-14, 2010. ,
Intel 64 and IA32 Architectures Software Developer Manual, 2014. ,
Intel 5100 Memory Controller Hub Chipset ,
, Intel. Intel 7 Series / C216 Chipset Family Platform Controller Hub (PCH)
SpecCert: a framework for the Coq Theorem Prover ,
The Architecture of the Nehalem Processor and Nehalem-EP SMP Platforms, Resource, vol.3, issue.2, 2011. ,
White Paper Introduction to Intel® Architecture, 2014. ,
Hyper-Threading Technology in the Netburst® Microarchitecture, 2002. ,
The Microarchitecture of Intel, AMD and VIA CPUs: An Optimization Guide for Assembly Programmers and Compiler Makers, 2012. ,
Demystifying Intel Branch Predictors, Workshop on Duplicating, Deconstructing and Debunking, 2002. ,
Technique for Supporting Multiple Secure Enclaves, US Patent, vol.8, p.746, 2015. ,
The Protection of Information in Computer Systems, Proceedings of the IEEE, vol.63, pp.1278-1308, 1975. ,
Intel Virtualization Technology for Directed I/O, Intel technology journal, vol.10, issue.3, 2006. ,
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. ,
BadUSB -On Accessories That Turn Evil, 2014. ,
Thunderstrike: EFI Firmware Bootkits for Apple MacBooks, Proceedings of the 8th ACM International Systems and Storage Conference, p.15, 2015. ,
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. ,
, BIOS Disassembly Ninjutsu Uncovered, 2006.
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.
Intel x86 Considered Harmful. the Invisible Things Lab, 2015. ,
A Tour Beyond BIOS into UEFI Secure Boot, 2012. ,
Protecting systems with the TPM, 2016. ,
HP Sure Start: Automatic Firmware Intrusion Detection and Repair System, 2016. ,
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.
ACPI and SMI Handlers: Some Limits to Trusted Computing, Journal in computer virology, vol.6, issue.4, pp.353-374, 2010. ,
Beyond BIOS: Developing with the Unified Extensible Firmware Interface, 2017. ,
System Management Mode Isolation in Firmware, p.446, 2009. ,
Formal Hardware Verification Methods: A Survey, Computer-Aided Verification, pp.5-92, 1992. ,
Verifying Linearizability of Intel® Software Guard Extensions, International Conference on Computer Aided Verification, pp.144-160, 2015. ,
Specifying and Verifying Hardware for Tamper-Resistant Software, Proceedings. 2003 Symposium on, pp.166-177, 2003. ,
Property Preserving Abstractions for the Verification of Concurrent Systems. Formal methods in system design, vol.6, pp.11-44, 1995. ,
NuSMV2: An Opensource Tool for Symbolic Model Checking, International Conference on Computer Aided Verification, pp.359-364, 2002. ,
Software Abstractions: Logic, Language and Analysis, 2012. ,
Formally Verifying Isolation and Availability in an Idealized Model of Virtualization, International Symposium on Formal Methods, pp.231-245, 2011. ,
, Recognizing Safety and Liveness. Distributed computing, vol.2, issue.3, pp.117-126, 1987.
Enforceable Security Policies, ACM Transactions on Information and System Security (TISSEC), vol.3, issue.1, pp.30-50, 2000. ,
, Enforceable Security Policies Revisited. ACM Transactions on Information and System Security (TISSEC), vol.16, issue.1, p.3, 2013.
Security Policies and Security Models, Security and Privacy, 1982 IEEE Symposium on, pp.11-11, 1982. ,
Introduction to Model Checking, Handbook of Model Checking, pp.1-26, 2018. ,
, Satisfiability Solvers. Foundations of Artificial Intelligence, vol.3, pp.89-134, 2008.
Model Checking and the State Explosion Problem, Tools for Practical Software Verification, pp.1-30, 2012. ,
First-Order Logic, vol.43, 2012. ,
Boolean Satisfiability From Theoretical Hardness to Practical Success, Communications of the ACM, vol.52, issue.8, pp.76-82, 2009. ,
Chaff: Engineering an Efficient SAT Solver, Proceedings of the 38th annual Design Automation Conference, pp.530-535, 2001. ,
6 Years of SMT-COMP, Journal of Automated Reasoning, vol.50, issue.3, pp.243-277, 2013. ,
Z3: An efficient SMT solver, International conference on Tools and Algorithms for the Construction and Analysis of Systems, pp.337-340, 2008. ,
Modal Logic, 1997. ,
The Complexity of Propositional Linear Temporal Logics, Journal of the ACM (JACM), vol.32, issue.3, pp.733-749, 1985. ,
Design and Synthesis of Synchronization Skeletons Using Branching Time Temporal Logic, Workshop on Logic of Programs, pp.52-71, 1981. ,
The Model Checker SPIN, IEEE Transactions on software engineering, vol.23, issue.5, pp.279-295, 1997. ,
, Specifying Systems: the TLA+ Language and Tools for Hardware and Software Engineers, 2002.
Symbolic Model Checking, Verification of Digital and Hybrid Systems, pp.117-137, 2000. ,
, Bounded Model Checking. Advances in computers, vol.58, issue.11, pp.117-148, 2003.
Higher Order Logic, 1994. ,
Isabelle/HOL: a proof assistant for higher-order logic, vol.2283, 2002. ,
The B-book: Assigning Programs to Meanings, 2005. ,
The Lean Theorem Prover (System Description), International Conference on Automated Deduction, pp.378-388, 2015. ,
Formal Verification of IA-64 Division Algorithms, International Conference on Theorem Proving in Higher Order Logics, pp.233-251, 2000. ,
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. ,
Hardware Security in Practice: Challenges and Opportunities, Hardware-Oriented Security and Trust (HOST), 2011 IEEE International Symposium on, pp.93-98, 2011. ,
RockSalt: Better, Faster, Stronger SFI for the x86, ACM SIGPLAN Notices, vol.47, pp.395-404, 2012. ,
Simulation And Formal Verification Of x86 Machine-Code Programs That Make System Calls, Formal Methods in Computer-Aided Design (FMCAD), pp.91-98, 2014. ,
The CompCert Verified Compiler. Documentation and user's manual, 2012. ,
URL : https://hal.archives-ouvertes.fr/hal-01399482
CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels, OSDI, vol.16, pp.653-669, 2016. ,
Toward Compositional Verification of Interruptible OS Kernels and Device Drivers, Journal of Automated Reasoning, vol.61, issue.1-4, pp.141-189, 2018. ,
The seL4 Microkernel ,
Formal verification of an OS kernel, Proceedings of the ACM SIGOPS 22nd symposium on Operating systems principles, pp.207-220, 2009. ,
Cache-Leakage Resilient OS Isolation in an Idealized Model of Virtualization, Computer Security Foundations Symposium (CSF), 2012 IEEE 25th, pp.186-197, 2012. ,
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 Trustworthy Monadic Formalization of the ARMv7 Instruction Set Architecture, International Conference on Interactive Theorem Proving, pp.243-258, 2010. ,
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. ,
End-to-end Verification of Processors with ISA-Formal, International Conference on Computer Aided Verification, pp.42-58, 2016. ,
A64 ISA XML for Armv8, vol.4, 2018. ,
Architectural Support for Copy and Tamper Resistant Software, ACM SIGPLAN Notices, vol.35, issue.11, pp.168-177, 2000. ,
In Transition from Global to Modular Temporal Reasoning about Programs, Logics and models of concurrent systems, pp.123-144, 1985. ,
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. ,
, Interface Automata. In ACM SIGSOFT Software Engineering Notes, vol.26, pp.109-120, 2001.
A Calculus of Communicating Systems, LNCS, vol.92, 1980. ,
Communicating Sequential Processes, Communications of the ACM, vol.21, issue.8, pp.666-677, 1978. ,
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. ,
How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Progranm, IEEE transactions on computers, issue.9, pp.690-691, 1979. ,
Verifying the Compatibility of Component Interfaces using the B Formal Method. Software Engineering Research and Practice, pp.850-856, 2005. ,
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
Component-based Development using the B method, 2006. ,
URL : https://hal.archives-ouvertes.fr/hal-00105041
,
Comprehending Monads, Proceedings of the 1990 ACM conference on LISP and functional programming, pp.61-78, 1990. ,
Combining Effects: Sum and Tensor, Theoretical Computer Science, vol.357, issue.1-3, pp.70-99, 2006. ,
Monad Transformers and Modular Interpreters, Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pp.333-343, 1995. ,
Programming and Reasoning with Algebraic Effects and Dependent Types, ACM SIGPLAN Notices, vol.48, pp.133-144, 2013. ,
Extensible Effects: An Alternative To Monad Transformers, ACM SIGPLAN Notices, vol.48, pp.59-70, 2013. ,
Preventing and Detecting Xen Hypervisor Subversions, Blackhat Briefings USA, 2008. ,
Desktop 4th Generation Intel Core Processor Family, Desktop Intel Pentium Processor Family, and Desktop Intel Celeron Processor Family ,
Modular Invariants for Layered Object Structures, Science of Computer Programming, vol.62, issue.3, pp.253-286, 2006. ,
The operational package, 2010. ,
Tackling the Awkward Squad: monadic input/output, concurrency, exceptions, and foreign-language calls in Haskell. Engineering theories of software construction, 2001. ,
, The Past, Present and Future, 2007.