M. R. Albrecht and K. G. Paterson, Lucky microseconds: A timing attack on amazon's s2n implementation of TLS, Advances in Cryptology -EUROCRYPT 2016 -35th Annual International Conference on the Theory and Applications of Cryptographic Techniques, vol.9665, pp.622-643, 2016.

N. J. Alfardan and K. G. Paterson, Lucky thirteen: Breaking the TLS and DTLS record protocols, IEEE Symposium on Security and Privacy, SP 2013, pp.526-540, 2013.

J. B. Almeida, M. Barbosa, G. Barthe, A. Blot, B. Grégoire et al., Jasmin: High-assurance and high-speed cryptography, Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, pp.1807-1823, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01649140

J. B. Almeida, M. Barbosa, G. Barthe, and F. Dupressoir, Certified computer-aided cryptography: efficient provably secure machine code from high-level implementations, ACM CCS, 2013.

J. B. Almeida, M. Barbosa, G. Barthe, and F. Dupressoir, Verifiable side-channel security of cryptographic implementations: Constant-time MEE-CBC, Fast Software Encryption -23rd International Conference, FSE 2016, vol.9783, pp.163-184, 2016.

J. B. Almeida, M. Barbosa, G. Barthe, B. Grégoire, A. Koutsos et al., The last mile: High-assurance and high-speed cryptographic implementations, 2020 IEEE Symposium on Security and Privacy, vol.2020, pp.965-982, 2020.
URL : https://hal.archives-ouvertes.fr/hal-02974993

J. C. Almeida, M. Barbosa, G. Barthe, F. Dupressoir, and M. Emmi, Verifying constant-time implementations, 25th USENIX Security Symposium (USENIX Security 16), 2016.

A. W. Appel, Program Logics -for Certified Compilers, 2014.

A. W. Appel, Verification of a cryptographic primitive: SHA-256, ACM Trans. Program. Lang. Syst, vol.37, issue.2, p.31, 2015.

M. Barbosa, G. Barthe, K. Bhargavan, B. Blanchet, C. Cremers et al., SoK: Computer-aided cryptography, IEEE Symposium on Security and Privacy (SP)

G. Barthe, G. Betarte, J. D. Campo, C. Luna, and D. Pichardie, System-level non-interference for constant-time cryptography, ACM SIGSAC Conference on Computer and Communications Security, CCS'14, 2014.
URL : https://hal.archives-ouvertes.fr/hal-01101950

G. Barthe, S. Blazy, B. Grégoire, R. Hutin, V. Laporte et al., Formal verification of a constant-time preserving C compiler, Proc. ACM Program. Lang, vol.4, 2020.
URL : https://hal.archives-ouvertes.fr/hal-02975012

G. Barthe, D. Demange, and D. Pichardie, Formal Verification of an SSA-Based Middle-End for CompCert, ACM Trans. Program. Lang. Syst. (TOPLAS), vol.36, issue.1, p.4, 2014.
URL : https://hal.archives-ouvertes.fr/inria-00634702

G. Barthe, B. Grégoire, and V. Laporte, Secure compilation of side-channel countermeasures: The case of cryptographic "constant-time, 31st IEEE Computer Security Foundations Symposium, pp.328-343, 2018.
URL : https://hal.archives-ouvertes.fr/hal-01959560

L. Beringer, A. Petcher, K. Q. Ye, and A. W. Appel, Verified correctness and security of openssl HMAC, 24th USENIX Security Symposium, USENIX Security 15, pp.207-221, 2015.

S. Blazy, V. Laporte, A. Maroneze, and D. Pichardie, Formal verification of a C value analysis based on abstract interpretation, Proc. of the 20 th Static Analysis Symposium (SAS), 2013.
URL : https://hal.archives-ouvertes.fr/hal-00812515

S. Blazy, V. Laporte, and D. Pichardie, An abstract memory functor for verified C static analyzers, Proceedings of the 21 st ACM SIGPLAN International Conference on Functional Programming, pp.325-337, 2016.
URL : https://hal.archives-ouvertes.fr/hal-01339969

B. Bond, C. Hawblitzel, M. Kapritsos, K. R. Leino, J. R. Lorch et al., Vale: Verifying high-performance cryptographic assembly code, Proceedings of the 26th USENIX Conference on Security Symposium, SEC'17, pp.917-934, 2017.

F. Bourdoncle, Efficient chaotic iteration strategies with widenings, Formal Methods in Programming and their Applications, pp.128-141, 1993.

S. Cauligi, G. Soeller, B. Johannesmeyer, F. Brown, R. S. Wahby et al., Fact: a DSL for timing-sensitive computation, Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, pp.174-189, 2019.
URL : https://hal.archives-ouvertes.fr/hal-02404755

Y. Chen, C. Hsu, H. Lin, P. Schwabe, M. Tsai et al., Verifying curve25519 software, Proceedings of the 2014 ACM SIGSAC Conference on Computer and Communications Security, pp.299-309, 2014.

L. Daniel, S. Bardin, and T. Rezk, Binsec / rel: Efficient relational symbolic execution for constant-time at binary level, 2020 IEEE Symposium on Security and Privacy, vol.2020, pp.1021-1038, 2020.

V. Silva, M. Payer, and D. X. Song, The correctness-security gap in compiler optimization, 2015 IEEE Symposium on Security and Privacy Workshops, SPW 2015, pp.73-87, 2015.

A. Erbsen, J. Philipoom, J. Gross, R. Sloan, and A. Chlipala, Simple high-level code for cryptographic arithmetic -with proofs, without compromises, 2019 IEEE Symposium on Security and Privacy, vol.2019, pp.1202-1219, 2019.

A. Fromherz, N. Giannarakis, C. Hawblitzel, B. Parno, A. Rastogi et al., A verified, efficient embedding of a verifiable assembly language, Principles of Programming Languages, 2019.

Y. Fu, J. Liu, X. Shi, M. Tsai, B. Wang et al., Signed cryptographic program verification with typed cryptoline, Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security, pp.1591-1606, 2019.

V. T. Hoang, T. Krovetz, and P. Rogaway, Robust authenticated-encryption AEZ and the problem that it solves, Advances in Cryptology -EUROCRYPT 2015 -34th Annual International Conference on the Theory and Applications of Cryptographic Techniques, vol.9056, pp.15-44, 2015.

J. Jourdan, V. Laporte, S. Blazy, X. Leroy, and D. Pichardie, A formally-verified C static analyzer, Proc. of the 42 th Symp. on Princ. of Prog. Languages (POPL)
URL : https://hal.archives-ouvertes.fr/hal-01078386

V. Le, M. Afshari, and Z. Su, Compiler validation via equivalence modulo inputs, ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI '14, pp.216-226, 2014.

X. Leroy, Formal verification of a realistic compiler, Commun. ACM, vol.52, issue.7, pp.107-115, 2009.
URL : https://hal.archives-ouvertes.fr/inria-00415861

L. Mauborgne and X. , Trace partitioning in abstract interpretation based static analyzers, European Symposium on Programming (ESOP'05 ), vol.3444, pp.5-20, 2005.

D. Molnar, M. Piotrowski, D. Schultz, and D. Wagner, The program counter security model: Automatic detection and removal of control-flow side channel attacks, ICISC, vol.3935, pp.156-168, 2005.

A. Petcher and G. Morrisett, The foundational cryptography framework, Principles of Security and Trust -4th International Conference, POST 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, vol.9036, pp.53-72, 2015.

M. Polubelova, K. Bhargavan, J. Protzenko, B. Beurdouche, A. Fromherz et al., Hacl texttimes n: Verified generic SIMD crypto (for all your favorite platforms), IACR Cryptol. ePrint Arch, p.572, 2020.

J. Protzenko, J. K. Zinzindohoué, A. Rastogi, T. Ramananandro, P. Wang et al., , 2017.

J. Regehr, Y. Chen, P. Cuoq, E. Eide, C. Ellison et al., Test-case reduction for C compiler bugs, ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI '12, pp.335-346, 2012.

X. Rival and L. Mauborgne, The trace partitioning abstract domain, ACM Transactions on Programming Languages and Systems (TOPLAS), vol.29, issue.5, 2007.

B. Rodrigues, F. Pereira, and D. Aranha, Sparse representation of implicit flows with applications to side-channel detection, Proceedings of Compiler Construction, 2016.

C. Sun, V. Le, Q. Zhang, and Z. Su, Toward understanding compiler bugs in GCC and LLVM, Proceedings of the 25th International Symposium on Software Testing and Analysis, pp.294-305, 2016.

Y. Yarom, D. Genkin, and N. Heninger, Cachebleed: A timing attack on openssl constant time RSA, Cryptographic Hardware and Embedded Systems -CHES 2016 -18th International Conference, vol.9813, pp.346-367, 2016.

J. Zinzindohoué, K. Bhargavan, J. Protzenko, and B. Beurdouche, Hacl*: A verified modern cryptographic library, SIGSAC Conference on Computer and Communications Security, vol.10, p.2017