, HOL4
Verifying constant-time implementations, USENIX Security 16. USENIX, pp.53-70, 2016. ,
Learning is change in knowledge: Knowledge-based security for dynamic policies, CSF 2012, pp.308-322, 2012. ,
Cryptographic Enforcement of Language-Based Information Erasure ,
, IEEE, pp.334-348, 2015.
Gradual Release: Unifying Declassification, Encryption and Key Release Policies, pp.207-221, 2007. ,
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
Securing Compilation Against Memory Probing, PLAS'18, pp.29-40, 2018. ,
URL : https://hal.archives-ouvertes.fr/hal-01901765
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
Language-Based Information Erasure, CSFW'05, pp.241-254, 2005. ,
, End-to-End Enforcement of Erasure and Declassification, CSF'08, pp.98-111, 2008.
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.
The Correctness-Security Gap in Compiler Optimization, SPW '15, pp.73-87, 2015. ,
Just Forget It: The Semantics and Enforcement of Information Erasure, ESOP'08, pp.239-253, 2008. ,
, When Constant-Time Source Yields Variable-Time Binary: Exploiting Curve25519-donna Built with MSVC 2015, vol.10052, pp.573-582, 2016.
Differential Power Analysis, CRYPTO '99, ser, vol.1666, pp.388-397, 1999. ,
Cakeml: a verified implementation of ML, POPL '14, pp.179-192, 2014. ,
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.
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.
Translation validation, Tools and Algorithms for Construction and Analysis of Systems, ser. LNCS, vol.1384, pp.151-166, 1998. ,
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
Declassification: Dimensions and principles, Journal of Computer Security, vol.17, issue.5, pp.517-548, 2009. ,
Translation validation for a verified os kernel, PLDI 2013, 2013. ,
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.
Undefined Behavior: What Happened to My Code?, in APSYS, vol.12, 2012. ,
Finding and understanding bugs in C compilers, PLDI 2011. ACM, pp.283-294, 2011. ,
Dead Store Elimination (Still) Considered Harmful, Proceedings of the 26th USENIX Conference on Security Symposium, ser. SEC'17. USENIX Association, pp.1025-1040, 2017. ,