M. Abadi, Control-flow Integrity Principles, Implementations, and Applications, vol.13, pp.1094-9224, 2009.

, ACCESS_ONCE() and compiler bugs, 2014.

. José-bacelar-almeida, Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, pp.1807-1823, 2017.

. José-bacelar-almeida, The Last Mile: High-Assurance and High-Speed Cryptographic Implementations, 2019.

. José-bacelar-almeida, « Verifying Constant-Time Implementations, USENIX Security 16, USENIX, pp.53-70, 2016.

J. Ansel, « Language-independent Sandboxing of Just-in-time Compilation and Self-modifying Code, SIGPLAN Not, vol.46, pp.362-1340, 2011.

A. Askarov and S. Chong, « Learning is Change in Knowledge: Knowledge-Based Security for Dynamic Policies, CSF 2012, pp.308-322, 2012.

A. Askarov, A. Sabelfeld, and . Release, Unifying Declassification, Encryption and Key Release Policies, SP'07, pp.207-221, 2007.

M. Backes and B. Köpf, « Formally Bounding the Side-Channel Leakage in Unknown-Message Attacks, pp.517-532, 2008.

G. Barthe, D. Demange, and D. Pichardie, « Formal Verification of an SSA-Based Middle-End for CompCert, ACM Trans. Program. Lang. Syst, vol.36, issue.1, 2014.

G. Barthe, B. Grégoire, and V. Laporte, « Secure Compilation of Side-Channel Countermeasures: The Case of Cryptographic "Constant-Time" », pp.328-343, 2018.

G. Barthe, Foundations of Security Analysis and Design VII: FOSAD 2012/2013 Tutorial Lectures, pp.146-166, 2014.

D. A. Basin, « Formal Analysis of 5G Authentication, 2018.

D. J. Bernstein, Cache-timing attacks on AES, 2005.

Y. Bertot and P. Castéran, Interactive theorem proving and program development, p.3540208542, 2004.
URL : https://hal.archives-ouvertes.fr/hal-00344237

F. Besson, S. Blazy, and P. Wilke, A Precise and Abstract Memory Model for C Using Symbolic Values, vol.8858, pp.449-468, 2014.
URL : https://hal.archives-ouvertes.fr/hal-01093312

F. Besson, S. Blazy, P. Wilke, and «. , Verified CompCert Front-End for a Memory Model Supporting Pointer Arithmetic and Uninitialised Data, Journal of Automated Reasoning, pp.1573-0670, 2018.
URL : https://hal.archives-ouvertes.fr/hal-01656895

F. Besson, S. Blazy, P. Wilke, and . Compcerts, A Memory-Aware Verified C Compiler Using Pointer as Integer Semantics, LNCS, vol.10499, pp.81-97, 2017.
URL : https://hal.archives-ouvertes.fr/hal-02401182

F. Besson, T. Jensen, and J. Lepiller, Modular Software Fault Isolation as Abstract Interpretation », in: Static Analysis, pp.978-981, 2018.

J. Bowman, Format String Attacks, vol.101, 2000.

M. Castro, Proceedings of the ACM SIGOPS 22Nd Symposium on Operating Systems Principles, SOSP '09, pp.45-58, 2009.

S. Chari, « Towards sound approaches to counteract power-analysis attacks, pp.398-412, 1999.

S. Chong and A. C. Myers, CSF'08, pp.98-111, 2008.

S. Chong and A. C. Myers, « Language-Based Information Erasure, CSFW'05, pp.241-254, 2005.

/. Csfw, , 2005.

V. Cortier, A. Filipiak, J. Lallemand, and . Beleniosvs, Secrecy and Verifiability against a Corrupted Voting Device, 32nd IEEE Computer Security Foundations Symposium (CSF'19), 2019.
URL : https://hal.archives-ouvertes.fr/hal-02126077

C. Cowan, Automatic adaptive detection and prevention of buffer-overflow attacks, Proceedings of the 7th USENIX Security Symposium, pp.63-78, 1998.

. Cwe-14, Compiler removal of code to clear buffers, 2013.

D. Vijay, M. Silva, D. Payer, and . Song, « The Correctness-Security Gap in Compiler Optimization, SPW '15, pp.73-87, 2015.

J. Damato, Beware of Compiler Optimizations, 2006.

C. Deng and K. S. Namjoshi, « Securing a Compiler Transformation, LNCS, vol.9837, pp.170-188, 2016.

C. Deng and K. S. Namjoshi, « Securing the SSA Transform, LNCS, vol.10422, pp.88-105, 2017.

S. Dhooghe, S. Nikova, and V. Rijmen, Threshold Implementations in the Robust Probing Model, Cryptology ePrint Archive, 1005.

Z. Durumeric, The Matter of Heartbleed, pp.475-488, 2014.

C. Ellison and G. Ro?u, « An executable formal semantics of C with applications, 2012.

Ú. Erlingsson, Software Guards for System Address Spaces, Proceedings of the 7th Symposium on Operating Systems Design and Implementation, OSDI '06, pp.75-88, 2006.

J. Fisher-ogden, Hardware support for efficient virtualization, 2006.

B. Ford, R. Cox, and . Vx32, Lightweight User-level Sandboxing on the x86, USENIX 2008 Annual Technical Conference, ATC'08, pp.293-306, 2008.

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

L. Goubin and J. Patarin, Proceedings of the First International Workshop on Cryptographic Hardware and Embedded Systems, CHES '99, pp.158-172, 1999.

M. Gruhn and T. Müller, 2013 International Conference on Availability, Reliability and Security, pp.390-397, 2013.

M. R. Guthaus, A free, commercially representative embedded benchmark suite, IEEE, pp.3-14, 2001.

J. and A. Halderman, Lest We Remember: Cold Boot Attacks on Encryption Keys, 2008.

C. Hathhorn, C. Ellison, and G. Ro?u, « Defining the Undefinedness of C, pp.336-345, 2015.

S. Hunt and D. Sands, Just Forget It: The Semantics and Enforcement of Information Erasure », in: ESOP'08, pp.239-253, 2008.

Y. Ishai, A. Sahai, and D. Wagner, Private Circuits: Securing Hardware against Probing Attacks, pp.978-981, 2003.

. Iso and . Iso-c-standard, , 1999.

J. Daemen and V. Rijmen, Resistance Against Implementation Attacks: A Comparative Study of the AES Proposals, 1999.

J. Jacob, On the Derivation of Secure Components, pp.242-247, 1989.

J. A. Drew-dean and . Kroll, BakerSFIeld: Bringing software fault isolation to x64, 2009.

J. Kang, « Lightweight verification of separate compilation, pp.178-190, 2016.

C. Paul, . Kocher-;-hellman, D. Rsa, O. Systems, and ». , Proceedings of the 16th Annual International Cryptology Conference on Advances in Cryptology, CRYPTO '96, pp.104-113, 1996.

C. Paul, J. Kocher, and B. Jaffe, Proceedings of the 19th Annual International Cryptology Conference on Advances in Cryptology, CRYPTO '99, pp.388-397, 1999.

P. Kocher, 40th IEEE Symposium on Security and Privacy (S&P'19), 2019.

B. Köpf and M. Dürmuth, « A Provably Secure And Efficient Countermeasure Against Timing Attacks, IACR Cryptology ePrint Archive, p.89, 2009.

, Robbert Krebbers, « An operational and axiomatic semantics for non-determinism and sequence points in C, 2014.

J. A. Kroll, G. Stewart, and A. W. Appel, Proceedings of the 2014 IEEE 27th Computer Security Foundations Symposium, CSF '14, pp.18-32, 2014.

R. Kumar, A Verified Implementation of ML, Principles of Programming Languages (POPL), pp.179-191, 2014.

C. Lattner, What Every C Programmer Should Know About Undefined Behaviour, 2011.

M. K-rustan, «. Leino, and . Dafny, An Automatic Program Verifier for Functional Correctness, pp.348-370, 2010.

S. Lerner, Automated Soundness Proofs for Dataflow Analyses and Transformations Via Local Rules, Proc. of the 32nd Symposium on Principles of Programming Languages, pp.364-377, 2005.

X. Leroy, Journal of Automated Reasoning, vol.43, pp.363-446, 2009.

X. Leroy, « Formal Certification of a Compiler Back-end or: Programming a Compiler with a Proof Assistant, POPL'06, pp.42-54, 2006.

X. Leroy, « Formal Verification of a Realistic Compiler, Commun. ACM, vol.52, pp.1-0782, 2009.

X. Leroy and S. Blazy, « Formal verification of a C-like memory model and its uses for verifying program transformations, Journal of Automated Reasoning, vol.41, p.1, 2008.

X. Leroy, Program Logics for Certified Compilers, p.9781107048010, 2014.

S. Kyung-suk-lhee and . Chapin, Buffer Overflow and Format String Overflow Vulnerabilities, vol.33, 2003.

M. Lipp, Reading Kernel Memory from User Space, 27th USENIX Security Symposium (USENIX Security 18), 2018.

H. Mantel, Preserving information flow properties under refinement, Proceedings 2001 IEEE Symposium on Security and Privacy. S P, pp.78-91, 2001.

S. Mccamant and G. Morrisett, « Evaluating SFI for a CISC architecture, 15th USENIX Security Symposium, pp.209-224, 2006.

B. Miller, L. Fredriksen, and B. So, « An Empirical Study of the Reliability of UNIX Utilities, Commun. ACM, vol.33, pp.32-44, 1990.

M. Strother, « A Mechanically Verified Language Implementation, Journal of Automated Reasoning, vol.5, pp.461-492, 1989.

G. Morrisett, Better, Faster, Stronger SFI for the x86, pp.978-979, 2012.

G. Morrisett, Better, Faster, Stronger SFI for the x86 », in: SIGPLAN Not, vol.47, pp.362-1340, 2012.

L. De-moura, N. Bjørner, and «. Z3, Tools and Algorithms for the Construction and Analysis of Systems, pp.337-340, 2008.

G. C. Necula, Proof-Carrying Code, pp.106-119, 1997.

C. George, P. Necula, and . Lee, Safe Kernel Extensions Without Run-Time Checking, pp.229-243, 1996.

F. Nielson, R. Hanne, C. Nielson, and . Hankin, Principles of Program Analysis, p.3540654100, 1999.

S. Nikova, C. Rechberger, and V. Rijmen, Proceedings of the 8th International Conference on Information and Communications Security, ICICS'06, pp.529-545, 2006.

T. Nipkow, L. Paulson, and M. Wenzel, Isabelle/HOL -A Proof Assistant for Higher-Order Logic, 2002.

M. Norrish, , 1998.

, Optimizer Removes Code Necesseray for Security, 2002.

A. Pnueli, M. Siegel, and E. Singerman, Tools and Algorithms for Construction and Analysis of Systems, vol.1384, pp.151-166, 1998.

T. Popp, S. Mangard, and E. Oswald, « Power Analysis Attacks and Countermeasures, IEEE Design & Test of Computers, vol.24, pp.535-543, 2007.

E. Prouff and M. Rivain, « Masking against side-channel attacks: A formal security proof, LNCS, vol.7881, pp.142-159, 2013.

L. Van-put, A reliable, retargetable and extensible link-time rewriting framework, IEEE International Symposium On Signal Processing And Information Technology, 2005.

J. Reardon, « 50 Ways to Leak Your Data: An Exploration of Apps' Circumvention of the Android Permissions System, 28th USENIX Security Symposium (USENIX Security 19), pp.978-979, 2019.

S. Rideau and X. Leroy, « Validating Register Allocation and Spilling, Compiler Construction, 19th International Conference, CC 2010, vol.6011, pp.224-243, 2010.

R. Roemer, Return-Oriented Programming: Systems, Languages, and Applications, vol.15, pp.1-34, 2012.

A. Sabelfeld, D. Sands, and . Declassification, Dimensions and principles, Journal of Computer Security, vol.17, pp.517-548, 2009.

,

K. Schramm and C. Paar, Proceedings of the 2006 The Cryptographers' Track at the RSA Conference on Topics in Cryptology, pp.208-225, 2006.

R. C. Seacord, Dangerous Optimizations and the Loss of Causality, 2010.

F. Seehusen and K. Stølen, « Maintaining Information Flow Security Under Refinement and Transformation, vol.4691, pp.143-157, 2006.

D. Sehr, Proceedings of the 19th USENIX Conference on Security, USENIX Security'10, pp.1-1, 2010.

D. Sehr, « Adapting Software Fault Isolation to Contemporary CPU Architectures, 19th USENIX Security Symposium, USENIX Association, pp.1-12, 2010.

S. Selvaraj, Overview of Intel Software Guard Extensions Enclave Life Cycle, 2016.

R. Shu, « A Study of Security Isolation Techniques, ACM Comput. Surv, vol.49, issue.3, pp.360-0300, 2016.

J. Siefers, G. Tan, G. Morrisett, and . Robusta, Proceedings of the 17th ACM Conference on Computer and Communications Security, CCS '10, pp.201-211, 2010.

P. Simmons and . Security, Through Amnesia: A Software-Based Solution to the Cold Boot Attack on Disk Encryption, 2011.

L. Simon, D. Chisnall, and R. J. Anderson, What You Get is What You C: Controlling Side Effects in Mainstream C Compilers, pp.1-15, 2018.

L. Simon, D. Chisnall, and R. J. Anderson, What You Get is What You C: Controlling Side Effects in Mainstream C Compilers, pp.1-15, 2018.

R. Sinha, « A Design and Verification Methodology for Secure Isolated Regions, pp.665-681, 2016.

C. Small and M. Seltzer, Abstract MiSFIT: A Tool for Constructing Safe Extensible C++ Systems, 1997.

M. Stump, , 2002.

M. Sun, « Bringing Java's Wild Native World Under Control, ACM Trans. Inf. Syst. Secur, vol.16, issue.3, pp.1094-9224, 2013.

. Scut and . Teso, Exploiting format strings vulnerabilities, 2001.

, The Coq development team, The Coq proof assistant reference manual, Version, 2017.

L. Torvalds, Linux bug in cfs, 2007.

R. Wahbe, « Efficient Software-based Fault Isolation, SIGOPS Oper. Syst. Rev, vol.27, pp.163-5980, 1993.

X. Wang, « Undefined behavior: what happened to my code?, APSys '12, p.9, 2012.

Z. Yang, « Dead Store Elimination (Still) Considered Harmful, Proceedings of the 26th USENIX Conference on Security Symposium, SEC'17, USENIX Association, pp.1025-1040, 2017.

B. Yee, Untrusted x86 Native Code, « Native Client: A Sandbox for Portable, vol.53, pp.1-0782, 2010.

B. Zeng, G. Tan, and G. Morrisett, « Combining Control-flow Integrity and Static Analysis for Efficient and Validated Data Sandboxing, Proceedings of the 18th ACM Conference on Computer and Communications Security, CCS '11, pp.29-40, 2011.

J. Zhao, « Formalizing the LLVM Intermediate Representation for Verified Program Transformations », in: SIGPLAN Not, vol.47, pp.362-1340, 2012.

L. Zhao, Proceedings of the Ninth ACM International Conference on Embedded Software, EM-SOFT '11, pp.289-298, 2011.

F. Besson, A. Dang, and T. P. Jensen, Information-Flow Preservation in Compiler Optimisations, 32nd IEEE Computer Security Foundations Symposium, pp.230-242, 2019.
URL : https://hal.archives-ouvertes.fr/hal-02180303

F. Besson, A. Dang, and T. P. Jensen, Proceedings of the 13th Workshop on Programming Languages and Analysis for Security, pp.29-40, 2018.

F. Besson, Compiling Sandboxes: Formally Verified Software Fault Isolation, pp.499-524, 2019.
URL : https://hal.archives-ouvertes.fr/hal-02316189