D. Ahman, C. Hri?cu, K. Maillard, G. Martínez, G. Plotkin et al., Dijkstra Monads for Free, 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL). ACM, pp.515-529, 2017.
DOI : 10.1145/3009837.3009878
URL : https://hal.archives-ouvertes.fr/hal-01424794

J. Bacelar-almeida, M. Barbosa, G. Barthe, and F. Dupressoir, Verifiable side-channel security of cryptographic implementations: constant-time MEE-CBC, IACR Cryptology ePrint Archive, vol.2015, p.1241, 1241.

J. Bacelar-almeida, M. Barbosa, G. Barthe, F. Dupressoir, and M. Emmi, Verifying Constant-Time Implementations, USENIX Security Symposium, pp.53-70, 2016.

W. Andrew and . Appel, Verification of a cryptographic primitive: SHA-256, ACM Transactions on Programming Languages and Systems (TOPLAS), vol.37, issue.7, 2015.

G. Barthe, G. Betarte, J. Campo, C. Luna, and D. Pichardie, System-level Non-interference for Constant-time Cryptography, Proceedings of the 2014 ACM SIGSAC Conference on Computer and Communications Security, CCS '14, pp.1267-1279, 2014.
DOI : 10.1007/s00145-009-9049-y
URL : https://hal.archives-ouvertes.fr/hal-01101950

G. Barthe, B. Grégoire, S. Heraud, and S. Z. Béguelin, Computer-Aided Security Proofs for the Working Cryptographer, Annual Cryptology Conference, pp.71-90, 2011.
DOI : 10.1007/978-3-642-22792-9_5
URL : https://hal.archives-ouvertes.fr/hal-01112075

D. Benjamin, 2016. poly1305-x86.pl produces incorrect output. https://mta. openssl.org/pipermail/openssl-dev, 2016.

L. Beringer, A. Petcher, K. Q. Ye, and A. W. Appel, Verified Correctness and Security of OpenSSL HMAC, USENIX Security Symposium, pp.207-221, 2015.

J. Daniel and . Bernstein, The Poly1305-AES Message-Authentication Code, Fast Software Encryption (FSE), pp.32-49, 2005.

J. Daniel and . Bernstein, Curve25519: new Diffie-Hellman speed records, Public Key Cryptography-PKC 2006, pp.207-228, 2006.

J. Daniel and . Bernstein, ChaCha, a variant of Salsa20, 2008.

J. Daniel, N. Bernstein, T. Duif, P. Lange, B. Schwabe et al., High-speed high-security signatures, Journal of Cryptographic Engineering, pp.1-13

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 (LATINCRYPT, pp.159-176, 2012.

J. Daniel, P. Bernstein, and . Schwabe, NEON crypto, International Workshop on Cryptographic Hardware and Embedded Systems, pp.320-339, 2012.

J. Daniel, B. Bernstein, W. Van-gastel, T. Janssen, P. Lange et al., TweetNaCl: A crypto library in 100 tweets, International Conference on Cryptology and Information Security in Latin America (LATINCRYPT, pp.64-83, 2014.

K. Bhargavan, A. Delignat-lavaud, C. Fournet, C. Hritcu, J. Protzenko et al., Verified Low-Level Programming Embedded in F*, ACM SIGPLAN International Conference on Functional Programming (ICFP), 2017.

K. Bhargavan, C. Fournet, M. Kohlweiss, A. Pironti, and P. Strub, Implementing TLS with Verified Cryptographic Security, 2013 IEEE Symposium on Security and Privacy, pp.445-462, 2013.
DOI : 10.1109/SP.2013.37
URL : https://hal.archives-ouvertes.fr/hal-00863373

H. Böck, Wrong results with Poly1305 functions. https://mta.openssl. org/pipermail/openssl-dev, 2016.

B. Bond, C. Hawblitzel, M. Kapritsos, K. Rustan, M. Leino et al., Vale: Verifying High-Performance Cryptographic Assembly Code, Proceedings of the USENIX Security Symposium, 2017.

B. Billy, M. Brumley, D. Barbosa, F. Page, and . Vercauteren, Practical realisation and elimination of an ECC-related software bug attack, Topics in Cryptology?CT-RSA 2012, pp.171-186, 2012.

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, CCS '14, pp.299-309, 2014.
DOI : 10.1145/363235.363259
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.564.7481

H. Quynh and . Dang, The Keyed-Hash Message Authentication Code (HMAC). NIST FIPS-198-1, 2008.

A. Delignat-lavaud, C. Fournet, M. Kohlweiss, J. Protzenko, A. Rastogi et al., Implementing and Proving the TLS 1.3 Record Layer, 2017 IEEE Symposium on Security and Privacy (SP), pp.463-482, 2017.
DOI : 10.1109/SP.2017.58

M. Goll and S. Gueron, Vectorization on ChaCha Stream Cipher, 2014 11th International Conference on Information Technology: New Generations, pp.612-615, 2014.
DOI : 10.1109/ITNG.2014.33
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.434.7229

C. Hawblitzel, J. Howell, R. Jacob, A. Lorch, B. Narayan et al., Ironclad apps: End-to-end security via automated full-system verification, 11th USENIX Symposium on Operating Systems Design and Implementation (OSDI 14, pp.165-181, 2014.

G. Klein, K. Elphinstone, G. Heiser-andronick, D. Cock, P. Derrin et al., seL4, Proceedings of the ACM SIGOPS 22nd symposium on Operating systems principles, SOSP '09, pp.207-220, 2009.
DOI : 10.1145/1629575.1629596

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

E. Nascimento, ?. Chmielewski, D. Oswald, and P. Schwabe, Attacking embedded ECC implementations through cmov side channels, Selected Areas in Cryptology ? SAC 2016 (Lecture Notes in Computer Science), 2016.

P. Strub, N. Swamy, C. Fournet, and J. Chen, Self- Certification: Bootstrapping Certified Typecheckers in F* with Coq, ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL, pp.571-584, 2012.
DOI : 10.1145/2103621.2103723
URL : https://hal.archives-ouvertes.fr/inria-00628775

N. Swamy, C. Hri?cu, C. Keller, A. Rastogi, A. Delignat-lavaud et al., Dependent Types and Multi-Monadic Effects in F*, ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pp.256-270
DOI : 10.1145/2837614.2837655
URL : https://hal.archives-ouvertes.fr/hal-01265793

A. Tomb, Automated Verification of Real-World Cryptographic Implementations, IEEE Security & Privacy, vol.14, issue.6, pp.26-33, 2016.
DOI : 10.1109/MSP.2016.125

J. Karim-zinzindohoue, E. Bartzia, and K. Bhargavan, A Verified Extensible Library of Elliptic Curves, 2016 IEEE 29th Computer Security Foundations Symposium (CSF), pp.296-309, 2016.
DOI : 10.1109/CSF.2016.28