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. ,
Lucky thirteen: Breaking the TLS and DTLS record protocols, IEEE Symposium on Security and Privacy, SP 2013, pp.526-540, 2013. ,
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
Certified computer-aided cryptography: efficient provably secure machine code from high-level implementations, ACM CCS, 2013. ,
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. ,
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
Verifying constant-time implementations, 25th USENIX Security Symposium (USENIX Security 16), 2016. ,
Program Logics -for Certified Compilers, 2014. ,
Verification of a cryptographic primitive: SHA-256, ACM Trans. Program. Lang. Syst, vol.37, issue.2, p.31, 2015. ,
SoK: Computer-aided cryptography, IEEE Symposium on Security and Privacy (SP) ,
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
Formal verification of a constant-time preserving C compiler, Proc. ACM Program. Lang, vol.4, 2020. ,
URL : https://hal.archives-ouvertes.fr/hal-02975012
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
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
Verified correctness and security of openssl HMAC, 24th USENIX Security Symposium, USENIX Security 15, pp.207-221, 2015. ,
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
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
Vale: Verifying high-performance cryptographic assembly code, Proceedings of the 26th USENIX Conference on Security Symposium, SEC'17, pp.917-934, 2017. ,
Efficient chaotic iteration strategies with widenings, Formal Methods in Programming and their Applications, pp.128-141, 1993. ,
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
Verifying curve25519 software, Proceedings of the 2014 ACM SIGSAC Conference on Computer and Communications Security, pp.299-309, 2014. ,
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. ,
The correctness-security gap in compiler optimization, 2015 IEEE Symposium on Security and Privacy Workshops, SPW 2015, pp.73-87, 2015. ,
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 verified, efficient embedding of a verifiable assembly language, Principles of Programming Languages, 2019. ,
Signed cryptographic program verification with typed cryptoline, Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security, pp.1591-1606, 2019. ,
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. ,
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
Compiler validation via equivalence modulo inputs, ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI '14, pp.216-226, 2014. ,
Formal verification of a realistic compiler, Commun. ACM, vol.52, issue.7, pp.107-115, 2009. ,
URL : https://hal.archives-ouvertes.fr/inria-00415861
Trace partitioning in abstract interpretation based static analyzers, European Symposium on Programming (ESOP'05 ), vol.3444, pp.5-20, 2005. ,
The program counter security model: Automatic detection and removal of control-flow side channel attacks, ICISC, vol.3935, pp.156-168, 2005. ,
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. ,
Hacl texttimes n: Verified generic SIMD crypto (for all your favorite platforms), IACR Cryptol. ePrint Arch, p.572, 2020. ,
, , 2017.
Test-case reduction for C compiler bugs, ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI '12, pp.335-346, 2012. ,
The trace partitioning abstract domain, ACM Transactions on Programming Languages and Systems (TOPLAS), vol.29, issue.5, 2007. ,
Sparse representation of implicit flows with applications to side-channel detection, Proceedings of Compiler Construction, 2016. ,
Toward understanding compiler bugs in GCC and LLVM, Proceedings of the 25th International Symposium on Software Testing and Analysis, pp.294-305, 2016. ,
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. ,
Hacl*: A verified modern cryptographic library, SIGSAC Conference on Computer and Communications Security, vol.10, p.2017 ,