J. Andronick, B. Chetali, and O. Ly, Using Coq to verify Java card applet isolation properties, TPHOL. LNCS, vol.2758, pp.335-351, 2003.

J. Ansel, P. Marchenko, Ú. Erlingsson, E. Taylor, B. Chen et al., Language-independent sandboxing of just-in-time compilation and self-modifying code, pp.355-366, 2011.

F. Besson, S. Blazy, and P. Wilke, 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

F. Besson, S. Blazy, and P. Wilke, 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

F. Besson, S. Blazy, and P. Wilke, 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

F. Besson, T. De-grenier-de-latour, and T. P. Jensen, Interfaces for stack inspection, J. Funct. Program, vol.15, issue.2, pp.179-217, 2005.

C. Ellison and G. Ro?u, An executable formal semantics of C with applications, 2012.

A. C. Fox and M. O. Myreen, A trustworthy monadic formalization of the ARMv7 instruction set architecture, ITP. LNCS, vol.6172, pp.243-258, 2010.

R. Guanciale, H. Nemati, M. Dam, and C. Baumann, Provably secure memory isolation for linux on ARM, Journal of Computer Security, vol.24, issue.6, pp.793-837, 2016.

M. Guthaus, J. Ringenberg, D. Ernst, T. Austin, T. Mudge et al., MiBench: A free, commercially representative embedded benchmark suite, pp.3-14, 2001.

C. Hathhorn, C. Ellison, and G. Ro?u, Defining the undefinedness of C, pp.336-345, 2015.

, ISO: ISO C Standard, 1999.

J. Kang, Y. Kim, C. Hur, D. Dreyer, and V. Vafeiadis, Lightweight verification of separate compilation, pp.178-190, 2016.

R. Krebbers, An operational and axiomatic semantics for non-determinism and sequence points in C, 2014.

J. A. Kroll, G. Stewart, and A. W. Appel, Portable software fault isolation, CSF. pp, pp.18-32, 2014.

J. R. Larus and G. C. Hunt, The singularity system, Commun. ACM, vol.53, issue.8, pp.72-79, 2010.

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

X. Leroy, 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

X. Leroy, A. W. Appel, S. Blazy, and G. Stewart, The CompCert memory model, Program Logics for Certified Compilers, 2014.
URL : https://hal.archives-ouvertes.fr/hal-00905435

X. Leroy and F. Rouaix, 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.

S. Mccamant and G. Morrisett, Evaluating SFI for a CISC architecture, Proceedings of the 15th Conference on USENIX Security Symposium, vol.15, 2006.

G. Morrisett, G. Tan, J. Tassarotti, J. B. Tristan, and E. Gan, Rocksalt: Better, faster, stronger SFI for the x86, pp.395-404, 2012.

G. C. Necula, Proof-carrying code, POPL. pp, pp.106-119, 1997.

G. C. Necula and P. Lee, Safe kernel extensions without run-time checking, pp.229-243, 1996.

M. Norrish, C formalised in HOL, 1998.

L. V. Put, D. Chanet, B. D. Bus, B. D. Sutter, and K. D. Bosschere, Diablo: A reliable, retargetable and extensible link-time rewriting framework, IEEE International Symposium On Signal Processing And Information Technology, 2005.

G. Richards, C. Hammer, F. Z. Nardelli, S. Jagannathan, and J. Vitek, Flexible access control for Javascript, OOPSLA. pp, pp.305-322, 2013.
URL : https://hal.archives-ouvertes.fr/hal-00909080

D. Sehr, R. Muth, C. Biffle, V. Khimenko, E. Pasko et al., Adapting software fault isolation to contemporary CPU architectures, 19th USENIX Security Symposium, pp.1-12, 2010.

D. Sehr, R. Muth, C. Biffle, V. Khimenko, E. Pasko et al., Adapting software fault isolation to contemporary cpu architectures, Proceedings of the 19th USENIX Conference on Security, pp.1-1, 2010.

R. Shu, P. Wang, I. Gorski, S. A. Andow, B. Nadkarni et al., A study of security isolation techniques, ACM Comput. Surv, vol.49, issue.3, 2016.

L. Simon, D. Chisnall, and R. J. Anderson, What you get is what you C: controlling side effects in mainstream C compilers, EuroS&P. pp, pp.1-15, 2018.

R. Sinha, M. Costa, A. Lal, N. P. Lopes, S. Rajamani et al., A design and verification methodology for secure isolated regions, pp.665-681, 2016.

R. Wahbe, S. Lucco, T. E. Anderson, and S. L. Graham, Efficient software-based fault isolation, SOSP. pp, pp.203-216, 1993.

X. Wang, H. Chen, A. Cheung, Z. Jia, N. Zeldovich et al., Undefined behavior: What happened to my code ?, 2012.

B. Yee, D. Sehr, G. Dardyk, J. B. Chen, R. Muth et al., Native Client: A sandbox for portable, untrusted x86 native code, pp.79-93, 2009.

B. Yee, D. Sehr, G. Dardyk, J. B. Chen, R. Muth et al., Native Client: a sandbox for portable, untrusted x86 native code, Commun. ACM, vol.53, issue.1, pp.91-99, 2010.

L. Zhao, G. Li, B. D. Sutter, and J. Regehr, ARMor: fully verified software fault isolation, pp.289-298, 2011.