Using Coq to verify Java card applet isolation properties, TPHOL. LNCS, vol.2758, pp.335-351, 2003. ,
Language-independent sandboxing of just-in-time compilation and self-modifying code, pp.355-366, 2011. ,
A precise and abstract memory model for C using symbolic values, APLAS. LNCS, vol.8858, pp.449-468, 2014. ,
URL : https://hal.archives-ouvertes.fr/hal-01093312
CompCertS: A memory-aware verified C compiler using pointer as integer semantics, ITP. LNCS, vol.10499, pp.81-97, 2017. ,
URL : https://hal.archives-ouvertes.fr/hal-01656875
A verified CompCert front-end for a memory model supporting pointer arithmetic and uninitialised data, Journal of Automated Reasoning, 2018. ,
URL : https://hal.archives-ouvertes.fr/hal-01656895
Interfaces for stack inspection, J. Funct. Program, vol.15, issue.2, pp.179-217, 2005. ,
An executable formal semantics of C with applications, 2012. ,
A trustworthy monadic formalization of the ARMv7 instruction set architecture, ITP. LNCS, vol.6172, pp.243-258, 2010. ,
Provably secure memory isolation for linux on ARM, Journal of Computer Security, vol.24, issue.6, pp.793-837, 2016. ,
MiBench: A free, commercially representative embedded benchmark suite, pp.3-14, 2001. ,
Defining the undefinedness of C, pp.336-345, 2015. ,
, ISO: ISO C Standard, 1999.
Lightweight verification of separate compilation, pp.178-190, 2016. ,
An operational and axiomatic semantics for non-determinism and sequence points in C, 2014. ,
Portable software fault isolation, CSF. pp, pp.18-32, 2014. ,
The singularity system, Commun. ACM, vol.53, issue.8, pp.72-79, 2010. ,
Formal verification of a realistic compiler, C. ACM, vol.52, issue.7, pp.107-115, 2009. ,
URL : https://hal.archives-ouvertes.fr/inria-00415861
A formally verified compiler back-end, Journal of Automated Reasoning, vol.43, issue.4, pp.363-446, 2009. ,
URL : https://hal.archives-ouvertes.fr/inria-00360768
The CompCert memory model, Program Logics for Certified Compilers, 2014. ,
URL : https://hal.archives-ouvertes.fr/hal-00905435
Security properties of typed applets, Security Issues for Mobile and Distributed Objects, vol.1603, pp.147-182, 1999. ,
URL : https://hal.archives-ouvertes.fr/hal-01499957
, The Coq development team: The Coq proof assistant reference manual, 2017.
Evaluating SFI for a CISC architecture, Proceedings of the 15th Conference on USENIX Security Symposium, vol.15, 2006. ,
Rocksalt: Better, faster, stronger SFI for the x86, pp.395-404, 2012. ,
Proof-carrying code, POPL. pp, pp.106-119, 1997. ,
Safe kernel extensions without run-time checking, pp.229-243, 1996. ,
C formalised in HOL, 1998. ,
Diablo: A reliable, retargetable and extensible link-time rewriting framework, IEEE International Symposium On Signal Processing And Information Technology, 2005. ,
Flexible access control for Javascript, OOPSLA. pp, pp.305-322, 2013. ,
URL : https://hal.archives-ouvertes.fr/hal-00909080
Adapting software fault isolation to contemporary CPU architectures, 19th USENIX Security Symposium, pp.1-12, 2010. ,
Adapting software fault isolation to contemporary cpu architectures, Proceedings of the 19th USENIX Conference on Security, pp.1-1, 2010. ,
A study of security isolation techniques, ACM Comput. Surv, vol.49, issue.3, 2016. ,
What you get is what you C: controlling side effects in mainstream C compilers, EuroS&P. pp, pp.1-15, 2018. ,
A design and verification methodology for secure isolated regions, pp.665-681, 2016. ,
Efficient software-based fault isolation, SOSP. pp, pp.203-216, 1993. ,
Undefined behavior: What happened to my code ?, 2012. ,
Native Client: A sandbox for portable, untrusted x86 native code, pp.79-93, 2009. ,
Native Client: a sandbox for portable, untrusted x86 native code, Commun. ACM, vol.53, issue.1, pp.91-99, 2010. ,
ARMor: fully verified software fault isolation, pp.289-298, 2011. ,