, HOL4

J. B. Almeida, M. Barbosa, G. Barthe, F. Dupressoir, and M. Emmi, Verifying constant-time implementations, USENIX Security 16. USENIX, pp.53-70, 2016.

A. Askarov and S. Chong, Learning is change in knowledge: Knowledge-based security for dynamic policies, CSF 2012, pp.308-322, 2012.

A. Askarov, S. Moore, C. Dimoulas, and S. Chong, Cryptographic Enforcement of Language-Based Information Erasure

, IEEE, pp.334-348, 2015.

A. Askarov and A. Sabelfeld, Gradual Release: Unifying Declassification, Encryption and Key Release Policies, pp.207-221, 2007.

G. Barthe, B. Grégoire, and V. Laporte, Secure Compilation of Side-Channel Countermeasures: The Case of Cryptographic "ConstantTime, CSF 2018, pp.328-343, 2018.
URL : https://hal.archives-ouvertes.fr/hal-01959560

F. Besson, A. Dang, and T. Jensen, Securing Compilation Against Memory Probing, PLAS'18, pp.29-40, 2018.
URL : https://hal.archives-ouvertes.fr/hal-01901765

S. Blazy, D. Pichardie, and A. Trieu, Verifying Constant-Time Implementations by Abstract Interpretation, ESORICS 2017, ser. LNCS, vol.10492, pp.260-277, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01588444

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

, End-to-End Enforcement of Erasure and Declassification, CSF'08, pp.98-111, 2008.

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

, Securing the SSA transform, SAS, ser. LNCS, vol.10422, pp.88-105, 2017.

, Securing a compiler transformation, Formal Methods in System Design, vol.53, issue.2, pp.166-188, 2018.

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

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

T. Kaufmann, H. Pelletier, S. Vaudenay, and K. Villegas, When Constant-Time Source Yields Variable-Time Binary: Exploiting Curve25519-donna Built with MSVC 2015, vol.10052, pp.573-582, 2016.

P. C. Kocher, J. Jaffe, and B. Jun, Differential Power Analysis, CRYPTO '99, ser, vol.1666, pp.388-397, 1999.

R. Kumar, M. O. Myreen, M. Norrish, and S. Owens, Cakeml: a verified implementation of ML, POPL '14, pp.179-192, 2014.

X. Leroy, Formal certification of a compiler back-end or: Programming a compiler with a proof assistant, POPL'06, pp.42-54, 2006.
URL : https://hal.archives-ouvertes.fr/inria-00000963

, Formal verification of a realistic compiler, Commun. ACM, vol.52, issue.7, pp.107-115, 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, issue.1, 2008.
URL : https://hal.archives-ouvertes.fr/inria-00289542

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

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

S. Rideau and X. Leroy, Validating register allocation and spilling, Compiler Construction, 19th International Conference, CC 2010, ser. LNCS, vol.6011, pp.224-243, 2010.
URL : https://hal.archives-ouvertes.fr/inria-00529841

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

T. Sewell, M. Myreen, and G. Klein, Translation validation for a verified os kernel, PLDI 2013, 2013.

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

, What you get is what you C: controlling side effects in mainstream C compilers, EuroS&P, pp.1-15, 2018.

X. Wang, H. Chen, A. Cheung, Z. Jia, N. Zeldovich et al., Undefined Behavior: What Happened to My Code?, in APSYS, vol.12, 2012.

X. Yang, Y. Chen, E. Eide, and J. Regehr, Finding and understanding bugs in C compilers, PLDI 2011. ACM, pp.283-294, 2011.

Z. Yang, B. Johannesmeyer, A. T. Olesen, S. Lerner, and K. Levchenko, Dead Store Elimination (Still) Considered Harmful, Proceedings of the 26th USENIX Conference on Security Symposium, ser. SEC'17. USENIX Association, pp.1025-1040, 2017.