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, 2016.
DOI : 10.1145/1785414.1785443
URL : https://hal.archives-ouvertes.fr/hal-01356690

R. Wojtczuk and J. Rutkowska, Attacking SMM Memory via Intel CPU Cache Poisoning, Invisible Things Lab, 2009.

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

C. Domas, The Memory Sinkhole, 2015.

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

P. Stewin and I. Bystrov, Understanding DMA Malware, International Conference on Detection of Intrusions and Malware, and Vulnerability Assessment, pp.21-41, 2012.
DOI : 10.1007/978-3-642-37300-8_2

I. P. Manual, Intel IA-64 Architecture Software Developer's Manual. Itanium Processor Microarchitecture Reference for Software Optimization, 2000.

I. Reid and A. , Intel 5100 Memory Controller Hub Chipset 10 Who Guards the Guards? Formal Validation of the Arm v8-M Architecture Specification, Proceedings of the ACM on Programming Languages, vol.1, issue.OOPSLA, p.88, 2017.
DOI : 10.1145/3133912
URL : http://dl.acm.org/ft_gateway.cfm?id=3133912&type=pdf

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.
DOI : 10.1007/978-3-319-21668-3_9

J. Choi, M. Vijayaraghavan, B. Sherman, and A. Chlipala, Kami: a platform for high-level parametric hardware specification and its modular verification, Proceedings of the ACM on Programming Languages, vol.1, issue.ICFP, p.24, 2017.
DOI : 10.1109/HPCA.2014.6835949
URL : http://dl.acm.org/ft_gateway.cfm?id=3110268&type=pdf

. Inria, The Coq Proof Assistant https://coq.inria.fr

T. Braibant, Coquet: A Coq Library for Verifying Hardware, CPP, vol.19, issue.3, pp.330-345, 2011.
DOI : 10.1007/s00165-007-0028-5
URL : https://hal.archives-ouvertes.fr/inria-00611757

G. Morrisett, G. Tan, J. Tassarotti, J. B. Tristan, and E. Gan, RockSalt, ACM SIGPLAN Notices, vol.47, issue.6, pp.395-404, 2012.
DOI : 10.1145/2038642.2038687

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

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.
DOI : 10.1016/j.jlamp.2014.02.001
URL : http://arxiv.org/pdf/1203.1539

H. Apfelmus, The operational package https

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

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 , POPL '95, pp.333-343, 1995.
DOI : 10.1145/199448.199528
URL : http://www.cis.upenn.edu/~davor/transformers.ps

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

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

E. Brady, Resource-Dependent Algebraic Effects, International Symposium on Trends in Functional Programming, pp.18-33, 2014.
DOI : 10.1007/978-3-319-14675-1_2

A. Nanevski, G. Morrisett, A. Shinnar, P. Govereau, and L. Birkedal, Ynot, ACM SIGPLAN Notices, vol.43, issue.9, pp.229-240, 2008.
DOI : 10.1145/1411203.1411237

G. Claret and Y. Régis-gianas, Mechanical Verification of Interactive Programs Specified by Use Cases, 2015 IEEE/ACM 3rd FME Workshop on Formal Methods in Software Engineering, pp.61-67, 2015.
DOI : 10.1109/FormaliSE.2015.17
URL : https://hal.archives-ouvertes.fr/hal-01255107

O. Kiselyov and H. Ishii, Freer monads, more extensible effects, ACM SIGPLAN Notices, vol.50, issue.12, pp.94-105, 2015.
DOI : 10.1145/2775050.2633358

J. R. Abrial and J. R. Abrial, The B-Book: Assigning Programs to Meanings, 2005.
DOI : 10.1017/CBO9780511624162

F. Pessaux, FoCaLiZe: inside an F-IDE. arXiv preprint arXiv:1404, p.6607, 2014.
DOI : 10.4204/eptcs.149.7
URL : https://hal.archives-ouvertes.fr/hal-01203501