G. Barthe, S. Blazy, V. Laporte, D. Pichardie, and A. Trieu, Veri?ed Translation Validation of Static Analyses, 2017 IEEE 30th Computer Security Foundations Symposium (CSF). 30th IEEE Computer Security Foundations Symposium, pp.405-419, 2017.
DOI : 10.1109/csf.2017.16
URL : https://hal.inria.fr/hal-01588422/file/csf17.pdf

S. Blazy, D. Pichardie, and A. Trieu, Verifying Constant-Time Implementations by Abstract Interpretation, European Symposium on Research in Computer Security. 22nd European Symposium on Research in Computer Security, 2017.
DOI : 10.3233/jcs-181136
URL : https://hal.archives-ouvertes.fr/hal-01588444

S. Blazy, D. Pichardie, and A. Trieu, Verifying ConstantTime Implementations by Abstract Interpretation (Extended version), In: Journal of Computer Security, 2018.
DOI : 10.3233/jcs-181136
URL : https://hal.inria.fr/hal-01588444/file/esorics17.pdf

S. Blazy and A. Trieu, Formal Veri?cation of Control-?ow Graph Flattening, Proceedings of the 5th ACM SIGPLAN Conference on Certi?ed Programs and Proofs. CPP 2016, pp.176-187, 2016.

M. José-bacelar-almeida, G. Barbosa, F. Barthe, M. Dupressoir, and . Emmi, Verifying Constant-Time Implementations, 25th USENIX Security Symposium, vol.16, pp.53-70, 2016.

J. Almeida, M. Barbosa, G. Barthe, A. Blot, B. Gré-goire et al., Jasmin: High-Assurance and High-Speed Cryptography, CCS 2017-Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, p.28, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01649140

M. Andrysco, D. Kohlbrenner, K. Mowery, R. Jhala, S. Lerner et al., On Subnormal Floating Point and Abnormal Timing, Proceedings of the 2015 IEEE Symposium on Security and Privacy. SP '15, vol.101, p.57, 2015.
DOI : 10.1109/sp.2015.44
URL : http://cseweb.ucsd.edu/%7Elerner/papers/subnormal.pdf

R. Martin, K. G. Albrecht, and . Paterson, Lucky Microseconds: A Timing Attack on Amazon's s2n Implementation of TLS, Advances in Cryptology -EUROCRYPT 2016, pp.622-643, 2016.

A. W. Appel, Veri?ed Software Toolchain -(Invited Talk), Lecture Notes in Computer Science, vol.6602, p.29, 2011.
DOI : 10.1007/978-3-642-19718-5_1
URL : https://link.springer.com/content/pdf/10.1007%2F978-3-642-19718-5_1.pdf

W. Andrew and . Appel, Veri?cation of a cryptographic primitive: SHA-256, ACM Transactions on Programming Languages and Systems, vol.37, p.29, 2015.

S. Arzt, S. Rasthofer, C. Fritz, E. Bodden, A. Bartel et al., FlowDroid: Precise Context, Flow, Field, Object-sensitive and Lifecycleaware Taint Analysis for Android Apps, Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation. PLDI '14, p.27, 2014.

M. Assaf, J. Signoles, F. Tronel, and E. Totel, Program Transformation for Non-interference Veri?cation on Programs with Pointers". In: 28th Security and Privacy Protection in Information Processing Systems (SEC), AICT-405. Security and Privacy Protection in Information Processing Systems, p.99, 2013.
DOI : 10.1007/978-3-642-39218-4_18
URL : https://link.springer.com/content/pdf/10.1007%2F978-3-642-39218-4_18.pdf

G. Barthe, G. Betarte, J. D. Campo, C. D. Luna, and D. Pichardie, System-level Non-interference for Constant-time Cryptography, 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

G. Barthe, S. Blazy, V. Laporte, D. Pichardie, and A. Trieu, Veri?ed Translation Validation of Static Analyses, Computer Security Foundations Symposium. 30th IEEE Computer Security Foundations Symposium, vol.60, 2017.
DOI : 10.1109/csf.2017.16
URL : https://hal.inria.fr/hal-01588422/file/csf17.pdf

G. Barthe, High-assurance cryptography: Cryptographic software we can trust, IEEE Security & Privacy, vol.13, p.28, 2015.
DOI : 10.1109/msp.2015.112

L. Beringer, A. Petcher, Y. Katherine, and A. W. Appel, Veri?ed Correctness and Security of OpenSSL HMAC, USENIX Security Symposium, p.29, 2015.

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

D. J. Bernstein, , p.28

D. J. Bernstein, Public Key Cryptography -PKC 2006: 9th International Conference on Theory and Practice in Public-Key Cryptography, p.55, 2006.

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

E. Biham, A Fast New DES Implementation in Software, Proceedings of the 4th International Workshop on Fast Software Encryption. FSE '97, p.100, 1997.
DOI : 10.1007/bfb0052352
URL : https://link.springer.com/content/pdf/10.1007%2FBFb0052352.pdf

B. Blanchet, P. Cousot, R. Cousot, J. Feret, L. Mauborgne et al., A static analyzer for large safety-critical software, p.26, 2003.
DOI : 10.1145/781131.781153
URL : https://hal.archives-ouvertes.fr/hal-00128135

J. Daniel, T. Bernstein, P. Lange, and . Schwabe, The security impact of a new cryptographic library, International Conference on Cryptology and Information Security in Latin America, vol.73, pp.159-176, 2012.

B. Bond, C. Hawblitzel, M. Kapritsos, M. Rustan, J. R. Leino et al., Vale: Verifying high-performance cryptographic assembly code, Proceedings of the USENIX Security Symposium, p.28, 2017.

W. Joppe, C. Bos, M. Costello, D. Naehrig, and . Stebila, PostQuantum Key Exchange for the TLS Protocol from the Ring Learning with Errors Problem, 2015 IEEE Symposium on Security and Privacy, vol.2015, pp.553-570, 2015.

S. Blazy, D. Pichardie, and A. Trieu, Verifying constant-time implementations by abstract interpretation, European Symposium on Research in Computer Security, pp.260-277, 2017.
DOI : 10.3233/jcs-181136
URL : https://hal.archives-ouvertes.fr/hal-01588444

S. Cauligi, G. Soeller, F. Brown, B. Johannesmeyer, Y. Huang et al., FaCT: A Flexible, Constant-Time Programming Language, Cybersecurity Development (SecDev, p.2017
DOI : 10.1109/secdev.2017.24

, IEEE, p.29, 2017.

P. Cousot and R. Cousot, Static determination of dynamic properties of programs, Proceedings of the Second International Symposium on Programming. Dunod, p.47, 1976.

B. Coppens, I. Verbauwhede, K. De-bosschere, and B. D. Sutter, Practical Mitigations for Timing-Based Side-Channel Attacks on Modern x86 Processors, 30th IEEE Symposium on Security and Privacy, p.100, 2009.
DOI : 10.1109/sp.2009.19

L. De-moura and N. Bjørner, Z3: An e?cient SMT solver, International conference on Tools and Algorithms for the Construction and Analysis of Systems, p.28, 2008.

F. Dewald, H. Mantel, and A. Weber, AVR Processors as a Platform for Language-Based Security, Computer Security -ESORICS 2017 -22nd European Symposium on Research in Computer Security, p.101, 2017.
DOI : 10.1007/978-3-319-66402-6_25

U. Erlingsson and M. Abadi, Operating system protection against sidechannel attacks that exploit memory latency, p.72, 2007.

W. Enck, P. Gilbert, B. Chun, L. P. Cox, J. Jung et al., TaintDroid: An Information?ow Tracking System for Realtime Privacy Monitoring on Smartphones, Proceedings of the 9th USENIX Conference on Operating Systems Design and Implementation. OSDI'10. USENIX Association, p.27, 2010.

A. Erbsen, J. Philipoom, J. Gross, R. Sloan, and A. Chlipala, Simple High-Level Code For Cryptographic Arithmetic -With Proofs, Without Compromises, Proceedings of the 40th IEEE Symposium on Security and Privacy (S&P'19), p.29, 2019.

R. W. Floyd, Assigning Meanings to Programs, p.14, 1967.
DOI : 10.1007/978-94-011-1793-7_4

H. Geuvers, Proof assistants: History, ideas and future, p.12, 2009.
DOI : 10.1007/s12046-009-0001-5
URL : http://www.cs.ru.nl/~herman/PUBS/proofassistants.pdf

J. A. Goguen and J. Meseguer, Security Policies and Security Models, 1982 IEEE Symposium on Security and Privacy, p.26, 1982.

G. Gonthier, A. Asperti, J. Avigad, Y. Bertot, C. Cohen et al., A Machine-Checked Proof of the Odd Order Theorem, Interactive Theorem Proving -4th International Conference, ITP 2013, pp.163-179, 2013.
URL : https://hal.archives-ouvertes.fr/hal-00816699

C. Hoare, An axiomatic basis for computer programming, Communications of the ACM, vol.12, p.14, 1969.
DOI : 10.1145/357980.358001

S. Hunt and D. Sands, On Flow-sensitive Security Types, Conference Record of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. POPL '06, p.27, 2006.
DOI : 10.1145/1111037.1111045
URL : http://openaccess.city.ac.uk/194/2/floatingX.pdf

Y. Ishai, A. Sahai, and D. Wagner, Private circuits: Securing hardware against probing attacks, Annual International Cryptology Conference, p.102, 2003.
DOI : 10.1007/978-3-540-45146-4_27
URL : https://link.springer.com/content/pdf/10.1007%2F978-3-540-45146-4_27.pdf

J. Jourdan, V. Laporte, S. Blazy, X. Leroy, and D. Pichardie, A Formally-Veri?ed C Static Analyzer, Proc. of the 42 th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp.247-259, 2015.
DOI : 10.1145/2775051.2676966
URL : https://hal.inria.fr/hal-01078386/file/verasco-popl2015.pdf

J. Jourdan, Verasco: a Formally Veri?ed C Static Analyzer, p.25, 2016.
DOI : 10.1145/2775051.2676966
URL : https://hal.inria.fr/hal-01078386/file/verasco-popl2015.pdf

T. Kaufmann, H. Pelletier, S. Vaudenay, and K. Villegas, When Constant-Time Source Yields Variable-Time Binary: Exploiting Curve25519-donna Built with MSVC, Cryptology and Network Security, p.78, 2015.
DOI : 10.1007/978-3-319-48965-0_36
URL : https://infoscience.epfl.ch/record/223794/files/32_1.pdf

P. Kocher, J. Ja?e, B. Jun, and P. Rohatgi, Introduction to di?erential power analysis, Journal of Cryptographic Engineering, vol.1, issue.1, pp.5-27, 2011.

P. Kocher, Timing Attacks on Implementations of Di?e-Hellman, RSA, DSS, and Other Systems, Advances in Cryptology -CRYPTO '96, vol.1109, pp.104-113, 1996.
DOI : 10.1007/3-540-68697-5_9
URL : https://link.springer.com/content/pdf/10.1007%2F3-540-68697-5_9.pdf

T. Kim, M. Peinado, and G. Mainar-ruiz, STEALTHMEM: system-level protection against cache-based side channel attacks in the cloud, USENIX Security 2012. USENIX Association, p.73, 2012.

A. Langley and . Donna, , vol.55, p.53

V. Laporte, Veri?ed static analyzes for low-level languages, p.25, 2015.

R. Leino, This is Boogie 2, Microsoft Research, p.28, 2008.

M. K-rustan and . Leino, Dafny: An automatic program veri?er for functional correctness, International Conference on Logic for Programming Arti?-cial Intelligence and Reasoning, p.28, 2010.

X. Leroy, Formal certi?cation of a compiler back-end, or: programming a compiler with a proof assistant, 33rd symposium Principles of Programming Languages, pp.42-54, 2006.

X. Leroy, A formally veri?ed compiler back-end, In: Journal of Automated Reasoning, vol.43, p.15, 2009.
DOI : 10.1007/s10817-009-9155-4
URL : http://arxiv.org/pdf/0902.2137

L. Li, F. Tegawendé, M. Bissyandé, S. Papadakis, A. Rasthofer et al., Static analysis of android apps: A systematic literature review, Information and Software Technology, vol.88, p.27, 2017.

H. Mantel, J. Schickel, A. Weber, and F. Weber, How Secure Is Green IT? The Case of Software-Based Energy Side Channels, Computer Security -23rd European Symposium on Research in Computer Security, ESORICS 2018, p.102, 2018.

, mbedTLS. mbedTLS (formerly known as PolarSSL, vol.57

D. Mercadier, P. Dagand, L. Lacassagne, and G. Muller, Usuba, Optimizing & Trustworthy Bitslicing Compiler, Workshop on Programming Models for SIMD/Vector Processing, p.101, 2018.
URL : https://hal.archives-ouvertes.fr/hal-01657259

D. Molnar, M. Piotrowski, D. Schultz, and D. Wagner, The Program Counter Security Model: Automatic Detection and Removal of Control-?ow Side Channel Attacks, Proceedings of the 8th International Conference on Information Security and Cryptology. ICISC'05, p.100, 2006.

. Gordon-d-plotkin, A structural approach to operational semantics, p.14, 1981.

T. Pornin and . Bearssl, , p.57

O. Reparaz, J. Balasch, and I. Verbauwhede, Dude, is my code constant time, Proc. of DATE 2017, p.53, 2017.
DOI : 10.23919/date.2017.7927267

H. G. Rice, Classes of Recursively Enumerable Sets and Their Decision Problems, Transactions of the American Mathematical Society, vol.74, issue.7, pp.358-366, 1953.
DOI : 10.1090/s0002-9947-1953-0053041-6
URL : https://www.ams.org/tran/1953-074-02/S0002-9947-1953-0053041-6/S0002-9947-1953-0053041-6.pdf

E. J. Schwartz, T. Avgerinos, and D. Brumley, All You Ever Wanted to Know About Dynamic Taint Analysis and Forward Symbolic Execution (but Might Have Been Afraid to Ask), Proceedings of the 2010 IEEE Symposium on Security and Privacy. SP '10, p.27, 2010.
DOI : 10.1109/sp.2010.26

, Open Quantum Safe. Open Quantum Safe, p.55

D. Schoepe, M. Balliu, F. Piessens, and A. Sabelfeld, Let's Face It: Faceted Values for Taint Tracking, Computer Security -ESORICS 2016. Ed. by Ioannis Askoxylakis, Sotiris Ioannidis, p.27, 2016.
DOI : 10.1007/978-3-319-45744-4_28

D. Scott and C. Strachey, Towards a Mathematical Semantics for Computer Languages. 1971 (cit, p.14

N. Swamy, J. Chen, C. Fournet, P. Strub, K. Bhargavan et al., Secure distributed programming with valuedependent types, Proceeding of the 16th ACM SIGPLAN international conference on Functional Programming, p.28, 2011.
URL : https://hal.archives-ouvertes.fr/inria-00596715

. Tis-ct and . Tis-ct, , p.53

D. Volpano, C. Irvine, and G. Smith, A Sound Type System for Secure Flow Analysis, J. Comput, pp.167-187, 1996.
DOI : 10.3233/jcs-1996-42-304

D. Volpano and G. Smith, Eliminating Covert Flows with Minimum Typings, Proceedings of the 10th IEEE Workshop on Computer Security Foundations. CSFW '97, p.27, 1997.
DOI : 10.1109/csfw.1997.596807
URL : https://calhoun.nps.edu/bitstream/10945/35282/1/csfw97.pdf

J. David, R. M. Wheeler, and . Needham, TEA, a tiny encryption algorithm, Fast Software Encryption: Second International Workshop Leuven, p.55, 1994.

X. Yang, Y. Chen, E. Eide, and J. Regehr, Finding and Understanding Bugs in C Compilers, Proceedings of the 32Nd ACM SIGPLAN Conference on Programming Language Design and Implementation. PLDI '11, pp.283-294, 2011.
DOI : 10.1145/2345156.1993532
URL : http://www.stanford.edu/class/cs343/resources/finding-bugs-compilers.pdf

K. Q. Ye, M. Green, N. Sanguansin, L. Beringer, A. Petcher et al., Veri?ed Correctness and Security of mbedTLS HMAC-DRBG, Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security. CCS '17, p.29, 2017.
DOI : 10.1145/3133956.3133974
URL : http://arxiv.org/pdf/1708.08542

Y. Yarom, D. Genkin, and N. Heninger, CacheBleed: a timing attack on OpenSSL constant-time RSA, Journal of Cryptographic Engineering, vol.7, issue.2, pp.99-112, 2017.
DOI : 10.1007/s13389-017-0152-y

J. Zinzindohoué, K. Bhargavan, J. Protzenko, and B. Beurdouche, HACL*: A Veri?ed Modern Cryptographic Library, Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security. CCS '17, p.28, 2017.

M. Zhao and G. E. Suh, FPGA-Based Remote Power Side-Channel Attacks, 2018 IEEE Symposium on Security and Privacy (SP), vol.00, pp.839-854, 2018.
DOI : 10.1109/sp.2018.00049