G. Barthe, G. Betarte, J. D. Campo, and C. Luna, Formally Verifying Isolation and Availability in an Idealized Model of Virtualization, FM 2011: Formal Methods, pp.231-245, 2011.
DOI : 10.1007/s10207-004-0057-5

G. Barthe, G. Betarte, J. D. Campo, and C. Luna, Cache-Leakage Resilient OS Isolation in an Idealized Model of Virtualization, 2012 IEEE 25th Computer Security Foundations Symposium, pp.2012-2037, 2012.
DOI : 10.1109/CSF.2012.17
URL : http://doi.org/10.1109/csf.2012.17

G. Barthe, G. Betarte, J. D. Campo, C. Luna, and D. Pichardie, System-level noninterference for constant-time cryptography, Proceedings of the 2014 ACM SIGSAC Conference on Computer and Communications Security, pp.1267-1279, 2014.
DOI : 10.1145/2660267.2660283
URL : https://hal.archives-ouvertes.fr/hal-01101950

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.
DOI : 10.1007/978-3-642-28641-4_17

C. Kallenberg, S. Cornwell, X. Kovah, and J. Butterworth, Setup For Failure: Defeating Secure Boot

C. Domas, The Memory Sinkhole, In: BlackHat USA, 2015.

S. Drzevitzky, Proof-Carrying Hardware: Runtime Formal Verification for Secure Dynamic Reconfiguration, 2010 International Conference on Field Programmable Logic and Applications, pp.255-258, 2010.
DOI : 10.1109/FPL.2010.59
URL : http://www.cs.uni-paderborn.de/fileadmin/Informatik/AG-Platzner/publications/drzevitzky10_fpl/drzevitzky10_fpl.pdf

X. Guo, R. G. Dutta, P. Mishra, and Y. Jin, Scalable SoC trust verification using integrated theorem proving and model checking, 2016 IEEE International Symposium on Hardware Oriented Security and Trust (HOST), pp.124-129, 2016.
DOI : 10.1109/HST.2016.7495569

. Intel, CHIPSEC: Platform Security Assessment Framework

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

C. Kallenberg and R. Wojtczuk, Speed racer: Exploiting an intel flash protection race condition

A. Kennedy, N. Benton, J. B. Jensen, and P. E. Dagand, Coq, Proceedings of the 15th Symposium on Principles and Practice of Declarative Programming, PPDP '13, pp.13-24, 2013.
DOI : 10.1145/2505879.2505897
URL : https://hal.archives-ouvertes.fr/hal-01081548

T. Letan, G. Hiet, P. Chifflier, P. Néron, and B. Morin, SpecCert: Specifying and Verifying Hardware-Based Security Enforcement, Centrale- Supélec ; Agence Nationale de Sécurité des Systèmes d'Information, 2016.
DOI : 10.1145/1785414.1785443
URL : https://hal.archives-ouvertes.fr/hal-01356690

D. Lie, J. Mitchell, C. Thekkath, and M. Horowitz, Specifying and verifying hardware for tamper-resistant software, Proceedings 19th International Conference on Data Engineering (Cat. No.03CH37405), pp.166-177, 2003.
DOI : 10.1109/SECPRI.2003.1199335
URL : http://www.princeton.edu/~rblee/ELE572Papers/Fall04Readings/LIE_IEEESP04.pdf

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

E. Love, Y. Jin, and Y. Makris, Proof-carrying hardware intellectual property: A pathway to trusted module acquisition. Information Forensics and Security, IEEE Transactions on, vol.7, issue.1, pp.25-40, 2012.
DOI : 10.1109/tifs.2011.2160627

Y. Makris, Trusted module acquisition through proof-carrying hardware intellectual property, Tech. rep, 2015.

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

R. Wojtczuk and J. Rutkowska, Attacking intel TXT via SINIT code execution hijacking

R. Wojtczuk and J. Rutkowska, Attacking SMM memory via intel CPU cache poisoning

J. Rutkowska and R. Wojtczuk, Preventing and detecting xen hypervisor subversions, Blackhat Briefings USA, 2008.

F. B. Schneider, Enforceable security policies, ACM Transactions on Information and System Security, vol.3, issue.1, pp.30-50, 2000.
DOI : 10.1145/353323.353382
URL : http://www.cs.cornell.edu/fbs/publications/99-1759.pdf

P. Sewell, S. Sarkar, S. Owens, F. Z. Nardelli, and M. O. Myreen, x86-TSO, Communications of the ACM, vol.53, issue.7, pp.89-97, 2010.
DOI : 10.1145/1785414.1785443