G. Balakrishnan and T. W. Reps, Analyzing Memory Accesses in x86 Executables, Compiler Construction, vol.2985, pp.5-23, 2004.

P. Biondi, R. Rigo, S. Zennou, and X. Mehrenberger, BinCAT: purrfecting binary static analysis, Symp. sur la sécurité des technologies de l'information et des communications, 2017.

D. Brumley, I. Jager, T. Avgerinos, and E. J. Schwartz, BAP: A Binary Analysis Platform, Computer Aided Verification, vol.6806, pp.463-469, 2011.

T. Dullien and S. Porst, Reil: A platform-independent intermediate representation of disassembled code for static code analysis, CanSecWest'09, 2009.

A. Haas, A. Rossberg, D. L. Schuff, B. L. Titzer, M. Holman et al., Bringing the Web Up to Speed with WebAssembly, Proc. of the 38th Conf. on Programming Language Design and Implementation, pp.185-200, 2017.

J. Jourdan, V. Laporte, S. Blazy, X. Leroy, and D. Pichardie, A FormallyVerified C Static Analyzer, Proc. of the 42Nd Symp. on Principles of Programming Languages, pp.247-259, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01078386

J. Kinder, Static Analysis of x86 Executables, 2010.

J. A. Kroll, G. Stewart, and A. W. Appel, Portable software fault isolation, Proc. of the 27th IEEE Computer Security Foundations Symp, pp.18-32, 2014.

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

B. Mihaila, Adaptable Static Analysis of Executables for proving the Absence of Vulnerabilities, 2015.

A. Miné, Abstract domains for bit-level machine integer and floating-point operations, Proc. of the Workshops on Automated Theory eXploration and on Invariant Generation, vol.17, pp.55-70, 2012.

G. Morrisett, G. Tan, J. Tassarotti, J. Tristan, and E. Gan, Rocksalt: Better, Faster, Stronger SFI for the x86, SIGPLAN Not, vol.47, issue.6, pp.395-404, 2012.

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

Y. Shoshitaishvili, R. Wang, C. Salls, N. Stephens, M. Polino et al., SoK: (State of) The Art of War: Offensive Techniques in Binary Analysis, IEEE Symp. on Security and Privacy, 2016.

R. Wahbe, S. Lucco, T. E. Anderson, and S. L. Graham, Efficient software-based fault isolation, SIGOPS Oper. Syst. Rev, vol.27, issue.5, pp.203-216, 1993.

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.
DOI : 10.1109/sp.2009.25
URL : http://www.muth.org/Robert/Papers/sosp_2009.pdf

S. , ? 0 = [s 0 , ? i ], s 0 ? gz , ? 0 , ?, ?, ? (0) , ? 0 with | ? i |= gz. By definition, ? 0 ? F, so we can construct Init

, with ? 1 , ? 1 ? Acc and ? 1 , ? 1 ? ? 2 , ? 2. By induction hypothesis, we also have S

). Since-i-safe-;-i-acc and S. , By case analysis on the rule that allows ? , we have: ? (FunAssign) The preconditions are the same as for (Assign)

?. Funstd, . Funldd, . Funcont, and F. Funindirectjump, FunCrash) Similar reasoning

, ? (FunStF) Here, the preconditions are either true for (StoreFrame) or (StoreCrash) because of Lemma 3

, ? (FunLdS) Here, the preconditions are either true for (LoadStack) or (LoadCrash) because of Lemma 3