, Control-flow Integrity Principles, Implementations, and Applications, vol.13, pp.1094-9224, 2009.
, ACCESS_ONCE() and compiler bugs, 2014.
, Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, pp.1807-1823, 2017.
, The Last Mile: High-Assurance and High-Speed Cryptographic Implementations, 2019.
« Verifying Constant-Time Implementations, USENIX Security 16, USENIX, pp.53-70, 2016. ,
« Language-independent Sandboxing of Just-in-time Compilation and Self-modifying Code, SIGPLAN Not, vol.46, pp.362-1340, 2011. ,
« Learning is Change in Knowledge: Knowledge-Based Security for Dynamic Policies, CSF 2012, pp.308-322, 2012. ,
Unifying Declassification, Encryption and Key Release Policies, SP'07, pp.207-221, 2007. ,
« Formally Bounding the Side-Channel Leakage in Unknown-Message Attacks, pp.517-532, 2008. ,
« Formal Verification of an SSA-Based Middle-End for CompCert, ACM Trans. Program. Lang. Syst, vol.36, issue.1, 2014. ,
« Secure Compilation of Side-Channel Countermeasures: The Case of Cryptographic "Constant-Time" », pp.328-343, 2018. ,
, Foundations of Security Analysis and Design VII: FOSAD 2012/2013 Tutorial Lectures, pp.146-166, 2014.
« Formal Analysis of 5G Authentication, 2018. ,
, Cache-timing attacks on AES, 2005.
Interactive theorem proving and program development, p.3540208542, 2004. ,
URL : https://hal.archives-ouvertes.fr/hal-00344237
, A Precise and Abstract Memory Model for C Using Symbolic Values, vol.8858, pp.449-468, 2014.
URL : https://hal.archives-ouvertes.fr/hal-01093312
Verified CompCert Front-End for a Memory Model Supporting Pointer Arithmetic and Uninitialised Data, Journal of Automated Reasoning, pp.1573-0670, 2018. ,
URL : https://hal.archives-ouvertes.fr/hal-01656895
A Memory-Aware Verified C Compiler Using Pointer as Integer Semantics, LNCS, vol.10499, pp.81-97, 2017. ,
URL : https://hal.archives-ouvertes.fr/hal-02401182
, Modular Software Fault Isolation as Abstract Interpretation », in: Static Analysis, pp.978-981, 2018.
, Format String Attacks, vol.101, 2000.
, Proceedings of the ACM SIGOPS 22Nd Symposium on Operating Systems Principles, SOSP '09, pp.45-58, 2009.
« Towards sound approaches to counteract power-analysis attacks, pp.398-412, 1999. ,
, CSF'08, pp.98-111, 2008.
« Language-Based Information Erasure, CSFW'05, pp.241-254, 2005. ,
, , 2005.
Secrecy and Verifiability against a Corrupted Voting Device, 32nd IEEE Computer Security Foundations Symposium (CSF'19), 2019. ,
URL : https://hal.archives-ouvertes.fr/hal-02126077
Automatic adaptive detection and prevention of buffer-overflow attacks, Proceedings of the 7th USENIX Security Symposium, pp.63-78, 1998. ,
, Compiler removal of code to clear buffers, 2013.
« The Correctness-Security Gap in Compiler Optimization, SPW '15, pp.73-87, 2015. ,
Beware of Compiler Optimizations, 2006. ,
« Securing a Compiler Transformation, LNCS, vol.9837, pp.170-188, 2016. ,
« Securing the SSA Transform, LNCS, vol.10422, pp.88-105, 2017. ,
Threshold Implementations in the Robust Probing Model, Cryptology ePrint Archive, 1005. ,
, The Matter of Heartbleed, pp.475-488, 2014.
« An executable formal semantics of C with applications, 2012. ,
Software Guards for System Address Spaces, Proceedings of the 7th Symposium on Operating Systems Design and Implementation, OSDI '06, pp.75-88, 2006. ,
Hardware support for efficient virtualization, 2006. ,
Lightweight User-level Sandboxing on the x86, USENIX 2008 Annual Technical Conference, ATC'08, pp.293-306, 2008. ,
, 1982 IEEE Symposium on Security and Privacy, pp.11-11, 1982.
, Proceedings of the First International Workshop on Cryptographic Hardware and Embedded Systems, CHES '99, pp.158-172, 1999.
, 2013 International Conference on Availability, Reliability and Security, pp.390-397, 2013.
A free, commercially representative embedded benchmark suite, IEEE, pp.3-14, 2001. ,
, Lest We Remember: Cold Boot Attacks on Encryption Keys, 2008.
« Defining the Undefinedness of C, pp.336-345, 2015. ,
, Just Forget It: The Semantics and Enforcement of Information Erasure », in: ESOP'08, pp.239-253, 2008.
, Private Circuits: Securing Hardware against Probing Attacks, pp.978-981, 2003.
, , 1999.
, Resistance Against Implementation Attacks: A Comparative Study of the AES Proposals, 1999.
, On the Derivation of Secure Components, pp.242-247, 1989.
BakerSFIeld: Bringing software fault isolation to x64, 2009. ,
« Lightweight verification of separate compilation, pp.178-190, 2016. ,
, Proceedings of the 16th Annual International Cryptology Conference on Advances in Cryptology, CRYPTO '96, pp.104-113, 1996.
, Proceedings of the 19th Annual International Cryptology Conference on Advances in Cryptology, CRYPTO '99, pp.388-397, 1999.
, 40th IEEE Symposium on Security and Privacy (S&P'19), 2019.
« A Provably Secure And Efficient Countermeasure Against Timing Attacks, IACR Cryptology ePrint Archive, p.89, 2009. ,
, Robbert Krebbers, « An operational and axiomatic semantics for non-determinism and sequence points in C, 2014.
, Proceedings of the 2014 IEEE 27th Computer Security Foundations Symposium, CSF '14, pp.18-32, 2014.
A Verified Implementation of ML, Principles of Programming Languages (POPL), pp.179-191, 2014. ,
What Every C Programmer Should Know About Undefined Behaviour, 2011. ,
An Automatic Program Verifier for Functional Correctness, pp.348-370, 2010. ,
Automated Soundness Proofs for Dataflow Analyses and Transformations Via Local Rules, Proc. of the 32nd Symposium on Principles of Programming Languages, pp.364-377, 2005. ,
, Journal of Automated Reasoning, vol.43, pp.363-446, 2009.
« Formal Certification of a Compiler Back-end or: Programming a Compiler with a Proof Assistant, POPL'06, pp.42-54, 2006. ,
« Formal Verification of a Realistic Compiler, Commun. ACM, vol.52, pp.1-0782, 2009. ,
« Formal verification of a C-like memory model and its uses for verifying program transformations, Journal of Automated Reasoning, vol.41, p.1, 2008. ,
, Program Logics for Certified Compilers, p.9781107048010, 2014.
, Buffer Overflow and Format String Overflow Vulnerabilities, vol.33, 2003.
Reading Kernel Memory from User Space, 27th USENIX Security Symposium (USENIX Security 18), 2018. ,
Preserving information flow properties under refinement, Proceedings 2001 IEEE Symposium on Security and Privacy. S P, pp.78-91, 2001. ,
« Evaluating SFI for a CISC architecture, 15th USENIX Security Symposium, pp.209-224, 2006. ,
« An Empirical Study of the Reliability of UNIX Utilities, Commun. ACM, vol.33, pp.32-44, 1990. ,
« A Mechanically Verified Language Implementation, Journal of Automated Reasoning, vol.5, pp.461-492, 1989. ,
Better, Faster, Stronger SFI for the x86, pp.978-979, 2012. ,
Better, Faster, Stronger SFI for the x86 », in: SIGPLAN Not, vol.47, pp.362-1340, 2012. ,
, Tools and Algorithms for the Construction and Analysis of Systems, pp.337-340, 2008.
, Proof-Carrying Code, pp.106-119, 1997.
, Safe Kernel Extensions Without Run-Time Checking, pp.229-243, 1996.
, Principles of Program Analysis, p.3540654100, 1999.
, Proceedings of the 8th International Conference on Information and Communications Security, ICICS'06, pp.529-545, 2006.
Isabelle/HOL -A Proof Assistant for Higher-Order Logic, 2002. ,
, , 1998.
, Optimizer Removes Code Necesseray for Security, 2002.
, Tools and Algorithms for Construction and Analysis of Systems, vol.1384, pp.151-166, 1998.
« Power Analysis Attacks and Countermeasures, IEEE Design & Test of Computers, vol.24, pp.535-543, 2007. ,
« Masking against side-channel attacks: A formal security proof, LNCS, vol.7881, pp.142-159, 2013. ,
A reliable, retargetable and extensible link-time rewriting framework, IEEE International Symposium On Signal Processing And Information Technology, 2005. ,
« 50 Ways to Leak Your Data: An Exploration of Apps' Circumvention of the Android Permissions System, 28th USENIX Security Symposium (USENIX Security 19), pp.978-979, 2019. ,
« Validating Register Allocation and Spilling, Compiler Construction, 19th International Conference, CC 2010, vol.6011, pp.224-243, 2010. ,
, Return-Oriented Programming: Systems, Languages, and Applications, vol.15, pp.1-34, 2012.
Dimensions and principles, Journal of Computer Security, vol.17, pp.517-548, 2009. ,
,
, Proceedings of the 2006 The Cryptographers' Track at the RSA Conference on Topics in Cryptology, pp.208-225, 2006.
Dangerous Optimizations and the Loss of Causality, 2010. ,
« Maintaining Information Flow Security Under Refinement and Transformation, vol.4691, pp.143-157, 2006. ,
, Proceedings of the 19th USENIX Conference on Security, USENIX Security'10, pp.1-1, 2010.
« Adapting Software Fault Isolation to Contemporary CPU Architectures, 19th USENIX Security Symposium, USENIX Association, pp.1-12, 2010. ,
, Overview of Intel Software Guard Extensions Enclave Life Cycle, 2016.
« A Study of Security Isolation Techniques, ACM Comput. Surv, vol.49, issue.3, pp.360-0300, 2016. ,
, Proceedings of the 17th ACM Conference on Computer and Communications Security, CCS '10, pp.201-211, 2010.
Through Amnesia: A Software-Based Solution to the Cold Boot Attack on Disk Encryption, 2011. ,
, What You Get is What You C: Controlling Side Effects in Mainstream C Compilers, pp.1-15, 2018.
, What You Get is What You C: Controlling Side Effects in Mainstream C Compilers, pp.1-15, 2018.
« A Design and Verification Methodology for Secure Isolated Regions, pp.665-681, 2016. ,
Abstract MiSFIT: A Tool for Constructing Safe Extensible C++ Systems, 1997. ,
, , 2002.
« Bringing Java's Wild Native World Under Control, ACM Trans. Inf. Syst. Secur, vol.16, issue.3, pp.1094-9224, 2013. ,
Exploiting format strings vulnerabilities, 2001. ,
, The Coq development team, The Coq proof assistant reference manual, Version, 2017.
Linux bug in cfs, 2007. ,
« Efficient Software-based Fault Isolation, SIGOPS Oper. Syst. Rev, vol.27, pp.163-5980, 1993. ,
« Undefined behavior: what happened to my code?, APSys '12, p.9, 2012. ,
« Dead Store Elimination (Still) Considered Harmful, Proceedings of the 26th USENIX Conference on Security Symposium, SEC'17, USENIX Association, pp.1025-1040, 2017. ,
Untrusted x86 Native Code, « Native Client: A Sandbox for Portable, vol.53, pp.1-0782, 2010. ,
« Combining Control-flow Integrity and Static Analysis for Efficient and Validated Data Sandboxing, Proceedings of the 18th ACM Conference on Computer and Communications Security, CCS '11, pp.29-40, 2011. ,
« Formalizing the LLVM Intermediate Representation for Verified Program Transformations », in: SIGPLAN Not, vol.47, pp.362-1340, 2012. ,
, Proceedings of the Ninth ACM International Conference on Embedded Software, EM-SOFT '11, pp.289-298, 2011.
Information-Flow Preservation in Compiler Optimisations, 32nd IEEE Computer Security Foundations Symposium, pp.230-242, 2019. ,
URL : https://hal.archives-ouvertes.fr/hal-02180303
, Proceedings of the 13th Workshop on Programming Languages and Analysis for Security, pp.29-40, 2018.
, Compiling Sandboxes: Formally Verified Software Fault Isolation, pp.499-524, 2019.
URL : https://hal.archives-ouvertes.fr/hal-02316189