* Ansel et al. (2011) Jason Ansel, Petr Marchenko, Úlfar Erlingsson, Elijah Taylor, Brad Chen, Derek L. Schuff, David Sehr, Cliff Biffle, and Bennet Yee. 2011.  Language-independent sandboxing of just-in-time compilation and self-modifying code. In _Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2011, San Jose, CA, USA, June 4-8, 2011_. ACM.  https://doi.org/10.1145/1993498.1993540
  * Bartel and Doe (2018) Alexandre Bartel and John Doe. 2018.  Twenty years of escaping the Java sandbox. In _Phrack_.
  * Belay et al. (2012) Adam Belay, Andrea Bittau, Ali Mashtizadeh, David Terei, David Mazières, and Christos Kozyrakis. 2012.  Dune: Safe User-Level Access to Privileged CPU Features. In _Proceedings of the 10th USENIX Conference on Operating Systems Design and Implementation_ (Hollywood, CA, USA) _(OSDI’12)_. USENIX Association, USA, 335–348.
  * Besson et al. (2019) Frédéric Besson, Sandrine Blazy, Alexandre Dang, Thomas Jensen, and Pierre Wilke. 2019\.  Compiling sandboxes: Formally verified software fault isolation. In _Programming Languages and Systems - 28th European Symposium on Programming, ESOP 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings_ _(Lecture Notes in Computer Science, Vol. 11423)_. Springer.  https://doi.org/10.1007/978-3-030-17184-1_18
  * Besson et al. (2018) Frédéric Besson, Thomas Jensen, and Julien Lepiller. 2018\.  Modular software fault isolation as abstract interpretation. In _Static Analysis - 25th International Symposium, SAS 2018, Freiburg, Germany, August 29-31, 2018, Proceedings_ _(Lecture Notes in Computer Science, Vol. 11002)_. Springer.  https://doi.org/10.1007/978-3-319-99725-4_12
  * Bittau et al. (2008) Andrea Bittau, Petr Marchenko, Mark Handley, and Brad Karp. 2008.  Wedge: Splitting Applications into Reduced-Privilege Compartments. In _5th USENIX Symposium on Networked Systems Design & Implementation, NSDI 2008, April 16-18, 2008, San Francisco, CA, USA, Proceedings_, Jon Crowcroft and Michael Dahlin (Eds.). USENIX Association, 309–322.  http://www.usenix.org/events/nsdi08/tech/full_papers/bittau/bittau.pdf
  * Bosamiya et al. (2020) Jay Bosamiya, Benjamin Lim, and Bryan Parno. 2020.  WebAssembly as an Intermediate Language for Provably-Safe Software Sandboxing.  PriSC.
  * Burow et al. (2017) Nathan Burow, Scott A. Carr, Joseph Nash, Per Larsen, Michael Franz, Stefan Brunthaler, and Mathias Payer. 2017.  Control-Flow Integrity: Precision, Security, and Performance.  _Comput. Surveys_ 50 (April 2017), 16:1–16:33.  https://doi.org/10.1145/3054924
  * Bytecode Alliance (2020a) Bytecode Alliance. 2020a.  _Lucet_.  https://github.com/bytecodealliance/lucet
  * Bytecode Alliance (2020b) Bytecode Alliance. 2020b.  _WebAssembly Micro Runtime_.  https://github.com/bytecodealliance/wasm-micro-runtime
  * Castro et al. (2009) Miguel Castro, Manuel Costa, Jean-Philippe Martin, Marcus Peinado, Periklis Akritidis, Austin Donnelly, Paul Barham, and Richard Black. 2009.  Fast byte-granularity software fault isolation. In _Proceedings of the 22nd ACM Symposium on Operating Systems Principles 2009, SOSP 2009, Big Sky, Montana, USA, October 11-14, 2009_. ACM.  https://doi.org/10.1145/1629575.1629581
  * Chen et al. (2016) Y. Chen, S. Reymondjohnson, Z. Sun, and L. Lu. 2016.  Shreds: Fine-Grained Execution Units with Private Memory. In _2016 IEEE Symposium on Security and Privacy (SP)_. 56–71.  https://doi.org/10.1109/SP.2016.12
  * Chromium Team (2020) Chromium Team. 2020\.  Memory safety.  https://www.chromium.org/Home/chromium-security/memory-safety.
  * Erlingsson et al. (2006) Úlfar Erlingsson, Martín Abadi, Michael Vrable, Mihai Budiu, and George C Necula. 2006\.  XFI: Software guards for system address spaces. In _7th Symposium on Operating Systems Design and Implementation (OSDI ’06), November 6-8, Seattle, WA, USA_. USENIX Association, 75–88.
  * Fähndrich et al. (2006) Manuel Fähndrich, Mark Aiken, Chris Hawblitzel, Orion Hodson, Galen Hunt, James R Larus, and Steven Levi. 2006.  Language support for fast and reliable message-based communication in Singularity OS. In _Proceedings of the 2006 EuroSys Conference, Leuven, Belgium, April 18-21, 2006_. ACM.  https://doi.org/10.1145/1217935.1217953
  * Ford (2005) Bryan Ford. 2005\.  VXA: A Virtual Architecture for Durable Compressed Archives.. In _FAST_ , Vol. 5.
  * Ford and Cox (2008) Bryan Ford and Russ Cox. 2008.  Vx32: Lightweight User-level Sandboxing on the x86. In _2008 USENIX Annual Technical Conference, Boston, MA, USA, June 22-27, 2008. Proceedings_. USENIX Association.
  * Froyd (2020) Nathan Froyd. 2020\.  Securing Firefox with WebAssembly.  https://hacks.mozilla.org/2020/02/securing-firefox-with-webassembly/.
  * Gadepalli et al. (2020) Phani Kishore Gadepalli, Sean McBride, Gregor Peach, Ludmila Cherkasova, and Gabriel Parmer. 2020.  Sledge: a Serverless-first, Light-weight Wasm Runtime for the Edge. In _Middleware ’20: 21st International Middleware Conference, Delft, The Netherlands, December 7-11, 2020_. ACM.  https://doi.org/10.1145/3423211.3425680
  * Google Project Zero (2021) Google Project Zero 2021.  Introducing the In-the-Wild Series.  https://googleprojectzero.blogspot.com/2021/01/introducing-in-wild-series.html.
  * Goonasekera et al. (2015) Nuwan Goonasekera, William Caelli, and Colin Fidge. 2015\.  LibVM: an Architecture for Shared Library Sandboxing.  45, 12 (2015), 1597–1617.  https://doi.org/10.1002/spe.2294
  * Grimmer et al. (2015) Matthias Grimmer, Roland Schatz, Chris Seaton, Thomas Würthinger, and Hanspeter Mössenböck. 2015\.  Memory-safe Execution of C on a Java VM. In _Workshop on Programming Languages and Analysis for Security (PLAS)_.
  * Haas et al. (2017) Andreas Haas, Andreas Rossberg, Derek L. Schuff, Ben L. Titzer, Michael Holman, Dan Gohman, Luke Wagner, Alon Zakai, and Jf Bastien. 2017.  Bringing the Web up to Speed with WebAssembly. In _Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation_ (Barcelona, Spain). Association for Computing Machinery, 185–200.  https://doi.org/10.1145/3062341.3062363
  * Hansen (2019) Lars T Hansen. 2019\.  Cranelift: Performance parity with Baldr on x86-64.  https://bugzilla.mozilla.org/show_bug.cgi?id=1539399.
  * Hedayati et al. (2019) Mohammad Hedayati, Spyridoula Gravani, Ethan Johnson, John Criswell, Michael L Scott, Kai Shen, and Mike Marty. 2019\.  Hodor: Intra-process isolation for high-throughput data plane libraries. In _2019 USENIX Annual Technical Conference, USENIX ATC 2019, Renton, WA, USA, July 10-12, 2019_. USENIX Association.
  * Herder et al. (2009) Jorrit N Herder, Herbert Bos, Ben Gras, Philip Homburg, and Andrew S Tanenbaum. 2009.  Fault isolation for device drivers. In _Proceedings of the 2009 IEEE/IFIP International Conference on Dependable Systems and Networks, DSN 2009, Estoril, Lisbon, Portugal, June 29 - July 2, 2009_. IEEE Computer Society.  https://doi.org/10.1109/DSN.2009.5270357
  * Hunt and Larus (2007) Galen C Hunt and James R Larus. 2007.  Singularity: rethinking the software stack.  _SIGOPS Operating Systems Review_ 41, 2 (2007).
  * Intel (2020) Intel 2020.  Intel® 64 and IA-32 Architectures Software Developer’s Manual.
  * Jangda et al. (2019) Abhinav Jangda, Bobby Powers, Emery D Berger, and Arjun Guha. 2019.  Not so fast: Analyzing the performance of WebAssembly vs. native code. In _2019 USENIX Annual Technical Conference, USENIX ATC 2019, Renton, WA, USA, July 10-12, 2019_. USENIX Association.
  * Johnson (2021) Evan Johnson. 2021\.  _Update VeriWasm version_.  https://github.com/bytecodealliance/lucet/pull/684
  * Johnson et al. (2021) Evan Johnson, David Thien, Yousef Alhessi, Shravan Narayan, Fraser Brown, Sorin Lerner, Tyler McMullen, Stefan Savage, and Deian Stefan. 2021.  Доверя́й, но проверя́й: SFI safety for native-compiled Wasm. In _Network and Distributed System Security Symposium (NDSS)_. Internet Society.
  * Karger (1989) Paul A. Karger. 1989\.  Using Registers to Optimize Cross-Domain Call Performance. In _Proceedings of the Third International Conference on Architectural Support for Programming Languages and Operating Systems_ (Boston, Massachusetts, USA) _(ASPLOS III)_. Association for Computing Machinery, New York, NY, USA, 194–204.  https://doi.org/10.1145/70082.68201
  * Kolosick et al. (2021) Matthew Kolosick, Shravan Narayan, Evan Johnson, Conrad Watt, Michael LeMay, Deepak Garg, Ranjit Jhala, and Deian Stefan. 2021\.  Isolation Without Taxation: Near Zero Cost Transitions for SFI.  arXiv:2105.00033 [cs.CR]
  * Kroll et al. (2014) Joshua A Kroll, Gordon Stewart, and Andrew W Appel. 2014\.  Portable software fault isolation. In _2014 IEEE 27th Computer Security Foundations Symposium_. IEEE, 18–32.
  * Kuznetsov et al. (2014) Volodymyr Kuznetsov, Laszlo Szekeres, Mathias Payer, George Candea, R. Sekar, and Dawn Song. 2014.  Code-Pointer Integrity. In _11th USENIX Symposium on Operating Systems Design and Implementation (OSDI 14)_. 147–163.  https://www.usenix.org/conference/osdi14/technical-sessions/presentation/kuznetsov
  * Litton et al. (2016) James Litton, Anjo Vahldiek-Oberwagner, Eslam Elnikety, Deepak Garg, Bobby Bhattacharjee, and Peter Druschel. 2016.  Light-Weight Contexts: An OS Abstraction for Safety and Performance. In _Proceedings of the 12th USENIX Conference on Operating Systems Design and Implementation_ _(OSDI’16)_. USENIX Association, 49–64.
  * Lu et al. (2018) H.J. Lu, Michael Matz, Milind Girkar, Jan Hubička, Andreas Jaeger, and Mark Mitchell. 2018\.  _System V Application Binary InterfaceAMD64 Architecture Processor Supplement(With LP64 and ILP32 Programming Models)_.  Technical Report.  https://software.intel.com/content/dam/develop/external/us/en/documents/intro-to-intel-avx-183287.pdf
  * Lucco et al. (1995) Steve Lucco, Oliver Sharp, and Robert Wahbe. 1995\.  Omniware: A universal substrate for web programming. In _WWW_.
  * Maffeis et al. (2010) Sergio Maffeis, John C Mitchell, and Ankur Taly. 2010\.  Object capabilities and isolation of untrusted web applications. In _31st IEEE Symposium on Security and Privacy, S &P 2010, 16-19 May 2010, Berleley/Oakland, California, USA_. IEEE Computer Society, 125–140.  https://doi.org/10.1109/SP.2010.16
  * Matos and Boudol (2005) A.A. Matos and G. Boudol. 2005.  On Declassification and the Non-Disclosure Policy. In _18th IEEE Computer Security Foundations Workshop (CSFW’05)_. 226–240.  https://doi.org/10.1109/CSFW.2005.21
  * McCamant and Morrisett (2006) Stephen McCamant and Greg Morrisett. 2006.  Evaluating SFI for a CISC Architecture. In _Proceedings of the 15th USENIX Security Symposium, Vancouver, BC, Canada, July 31 - August 4, 2006_. USENIX Association.
  * McMullen (2020) Tyler McMullen. 2020\.  Lucet: A Compiler and Runtime for High-Concurrency Low-Latency Sandboxing. In _PriSC_.
  * Metrick et al. (2020) Kathleen Metrick, Jared Semrau, and Shambavi Sadayappan. 2020\.  Think Fast: Time Between Disclosure, Patch Release and Vulnerability Exploitation – Intelligence for Vulnerability Management, Part Two.  https://www.fireeye.com/blog/threat-research/2020/04/time-between-disclosure-patch-release-and-vulnerability-exploitation.html.
  * Mettler et al. (2010) Adrian Mettler, David A Wagner, and Tyler Close. 2010\.  Joe-E: A Security-Oriented Subset of Java.. In _Network and Distributed System Security Symposium (NDSS)_.
  * Miller (2019) Matt Miller. 2019\.  Trends, challenges, and strategic shifts in the software vulnerability mitigation landscape.  BlueHat.
  * Miller et al. (2008) M.S. Miller, M. Samuel, B. Laurie, I. Awad, and M. Stay. 2008.  Caja: Safe active content in sanitized JavaScript.  http://google-caja.googlecode.com/files/caja-spec-2008-06-07.pdf.
  * Morrisett et al. (1999a) Greg Morrisett, Karl Crary, Neal Glew, Dan Grossman, Richard Samuels, Frederick Smith, David Walker, Stephanie Weirich, and Steve Zdancewic. 1999a.  TALx86: A Realistic Typed Assembly Language.  _ACM SIGPLAN Workshop on Compiler Support for System Software_ (1999), 25–35.
  * Morrisett et al. (2002) Greg Morrisett, Karl Crary, Neal Glew, and David Walker. 2002\.  Stack-Based Typed Assembly Language.  _Journal of Functional Programming_ 12 (Jan. 2002), 43–88.  https://doi.org/10.1017/S0956796801004178 Publisher: Cambridge University Press.
  * Morrisett et al. (2012) Greg Morrisett, Gang Tan, Joseph Tassarotti, Jean-Baptiste Tristan, and Edward Gan. 2012.  RockSalt: Better, Faster, Stronger SFI for the x86. In _ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI ’12, Beijing, China - June 11 - 16, 2012_. ACM.  https://doi.org/10.1145/2254064.2254111
  * Morrisett et al. (1999b) Greg Morrisett, David Walker, Karl Crary, and Neal Glew. 1999b.  From System F to Typed Assembly Language.  _ACM Transactions on Programming Languages and Systems_ 21 (May 1999), 527–568.  https://doi.org/10.1145/319301.319345
  * Mozilla (2021) Mozilla. 2021\.  Firefox Public Data Report.  https://data.firefox.com/dashboard/hardware.
  * Nacl Issue 1607 (2011) Nacl Issue 1607 2011.  Issue 1607: Signal handling change allows inner sandbox escape on x86-32 Linux in Chrome.  https://bugs.chromium.org/p/nativeclient/issues/detail?id=1607.
  * Nacl Issue 1633 (2011) Nacl Issue 1633 2011.  Issue 1633: Inner sandbox escape on 64-bit Windows via KiUserExceptionDispatcher.  https://bugs.chromium.org/p/nativeclient/issues/detail?id=1633.
  * Nacl Issue 2919 (2012) Nacl Issue 2919 2012.  Issue 2919: Security: NaClSwitch() leaks NaClThreadContext pointer to x86-32 untrusted code.  https://bugs.chromium.org/p/nativeclient/issues/detail?id=2919.
  * Nacl Issue 775 (2010) Nacl Issue 775 2010.  Issue 775: Uninitialized sendmsg syscall arguments in sel_ldr.  https://bugs.chromium.org/p/nativeclient/issues/detail?id=775.
  * Narayan et al. (2020) Shravan Narayan, Craig Disselkoen, Tal Garfinkel, Nathan Froyd, Eric Rahm, Sorin Lerner, Hovav Shacham, and Deian Stefan. 2020\.  Retrofitting Fine Grain Isolation in the Firefox Renderer. In _29th USENIX Security Symposium, USENIX Security 2020, August 12-14, 2020_ , Srdjan Capkun and Franziska Roesner (Eds.). USENIX Association, 699–716.
  * Narayan et al. (2019) Shravan Narayan, Tal Garfinkel, Sorin Lerner, Hovav Shacham, and Deian Stefan. 2019.  Gobi: WebAssembly as a Practical Path to Library Sandboxing.  arXiv:1912.02285 [cs.CR]
  * Native Client team (2009) Native Client team. 2009\.  Native Client security contest archive.  https://developer.chrome.com/docs/native-client/community/security-contest/.
  * Niu and Tan (2014) Ben Niu and Gang Tan. 2014\.  RockJIT: Securing just-in-time compilation using modular control-flow integrity. In _Proceedings of the 2014 ACM SIGSAC Conference on Computer and Communications Security, Scottsdale, AZ, USA, November 3-7, 2014_. ACM.  https://doi.org/10.1145/2660267.2660281
  * Payer and Gross (2011) Mathias Payer and Thomas R. Gross. 2011.  Fine-Grained User-Space Security through Virtualization. In _Proceedings of the 7th ACM SIGPLAN/SIGOPS International Conference on Virtual Execution Environments_. Association for Computing Machinery, New York, NY, USA.  https://doi.org/10.1145/1952682.1952703
  * Qiang et al. (2017) Weizhong Qiang, Yong Cao, Weiqi Dai, Deqing Zou, Hai Jin, and Benxi Liu. 2017\.  Libsec: A Hardware Virtualization-Based Isolation for Shared Library. In _2017 IEEE 19th International Conference on High Performance Computing and Communications; IEEE 15th International Conference on Smart City; IEEE 3rd International Conference on Data Science and Systems (HPCC/SmartCity/DSS)_. 34–41.  https://doi.org/10.1109/HPCC-SmartCity-DSS.2017.5
  * Rydgard (2020) Henrik Rydgard. 2020\.  Windows (Fastcall) calling convention: Callee-saved XMM (FP) registers are not actually saved.  https://github.com/bytecodealliance/wasmtime/issues/1177.
  * Schrammel et al. (2020) David Schrammel, Samuel Weiser, Stefan Steinegger, Martin Schwarzl, Michael Schwarz, Stefan Mangard, and Daniel Gruss. 2020\.  Donky: Domain Keys – Efficient In-Process Isolation for RISC-V and x86. In _29th USENIX Security Symposium (USENIX Security 20)_. USENIX Association, 1677–1694.  https://www.usenix.org/conference/usenixsecurity20/presentation/schrammel
  * Sehr et al. (2010) David Sehr, Robert Muth, Karl Schimpf, Cliff Biffle, Victor Khimenko, Bennet Yee, Brad Chen, and Egor Pasko. 2010\.  Adapting Software Fault Isolation to Contemporary CPU Architectures. In _19th USENIX Security Symposium, Washington, DC, USA, August 11-13, 2010, Proceedings_. USENIX Association, 1–12.
  * Seltzer et al. (1996) Margo I Seltzer, Yasuhiro Endo, Christopher Small, and Keith A Smith. 1996.  Dealing with disaster: Surviving misbehaved kernel extensions. In _Proceedings of the Second USENIX Symposium on Operating Systems Design and Implementation (OSDI), Seattle, Washington, USA, October 28-31, 1996_. ACM.  https://doi.org/10.1145/238721.238779
  * Siefers et al. (2010) Joseph Siefers, Gang Tan, and Greg Morrisett. 2010.  Robusta: Taming the native beast of the JVM. In _Proceedings of the 17th ACM Conference on Computer and Communications Security, CCS 2010, Chicago, Illinois, USA, October 4-8, 2010_. ACM.  https://doi.org/10.1145/1866307.1866331
  * Skorstengaard et al. (2019) Lau Skorstengaard, Dominique Devriese, and Lars Birkedal. 2019\.  StkTokens: enforcing well-bracketed control flow and stack encapsulation using linear capabilities.  _Proceedings of the ACM on Programming Languages_ 3, POPL (Jan. 2019), 1–28.  https://doi.org/10.1145/3290332
  * Tan et al. (2017) Gang Tan et al. 2017\.  _Principles and implementation techniques of software-based fault isolation_.  Now Publishers.
  * The LLVM Foundation (2018) The LLVM Foundation. 2018\.  _Automatic variable initialization_.  https://reviews.llvm.org/rL349442
  * The LLVM Foundation (2021a) The LLVM Foundation. 2021a.  _Control Flow Integrity, Clang 12 documentation_.  https://clang.llvm.org/docs/ControlFlowIntegrity.html
  * The LLVM Foundation (2021b) The LLVM Foundation. 2021b.  _SafeStack, Clang 12 documentation_.  https://clang.llvm.org/docs/SafeStack.html
  * Tice et al. (2014) Caroline Tice, Tom Roeder, Peter Collingbourne, Stephen Checkoway, Úlfar Erlingsson, Luis Lozano, and Geoff Pike. 2014\.  Enforcing Forward-Edge Control-Flow Integrity in GCC & LLVM. In _Proceedings of the 23rd USENIX Security Symposium_ , Kevin Fu and Jaeyeon Jung (Eds.). 941–955.
  * Tsariounov (2021) Alex Tsariounov. 2021\.  _Shielding Linux Resources—Introduction_.  https://documentation.suse.com/sle-rt/15-SP1/html/SLE-RT-all/cha-shielding-intro.html
  * Vahldiek-Oberwagner et al. (2019) Anjo Vahldiek-Oberwagner, Eslam Elnikety, Nuno O Duarte, Michael Sammler, Peter Druschel, and Deepak Garg. 2019.  ERIM: Secure, Efficient In-process Isolation with Protection Keys (MPK). In _28th USENIX Security Symposium (USENIX Security 19)_. USENIX Association, 1221–1238.
  * Varda (2018) K. Varda. 2018.  WebAssembly on Cloudflare workers.  https://blog.cloudflare.com/webassembly-on-cloudflare-workers/.
  * Wahbe et al. (1993) Robert Wahbe, Steven Lucco, Thomas E. Anderson, and Susan L. Graham. 1993.  Efficient Software-Based Fault Isolation. In _Proceedings of the Fourteenth ACM Symposium on Operating Systems Principles_ (Asheville, North Carolina, USA) _(SOSP ’93)_. Association for Computing Machinery, 203–216.  https://doi.org/10.1145/168619.168635
  * Watson et al. (2015) R. N. M. Watson, J. Woodruff, P. G. Neumann, S. W. Moore, J. Anderson, D. Chisnall, N. Dave, B. Davis, K. Gudka, B. Laurie, S. J. Murdoch, R. Norton, M. Roe, S. Son, and M. Vadera. 2015.  CHERI: A Hybrid Capability-System Architecture for Scalable Software Compartmentalization. In _2015 IEEE Symposium on Security and Privacy_. 20–37.  https://doi.org/10.1109/SP.2015.9
  * Watt et al. (2019) Conrad Watt, Andreas Rossberg, and Jean Pichon-Pharabod. 2019\.  Weakening WebAssembly.  _Proc. ACM Program. Lang._ 3, OOPSLA, Article 133 (Oct. 2019), 28 pages.  https://doi.org/10.1145/3360559
  * WebAssembly Community Group (2021) WebAssembly Community Group. 2021\.  _Exception Handling_.  https://github.com/WebAssembly/exception-handling
  * Yang et al. (2011) Xuejun Yang, Yang Chen, Eric Eide, and John Regehr. 2011\.  Finding and understanding bugs in C compilers. In _PLDI_.
  * Yee et al. (2009) Bennet Yee, David Sehr, Gregory Dardyk, J. Bradley Chen, Robert Muth, Tavis Ormandy, Shiki Okasaka, Neha Narula, and Nicholas Fullagar. 2009.  Native Client: A Sandbox for Portable, Untrusted x86 Native Code. In _2009 30th IEEE Symposium on Security and Privacy_. 79–93.  https://doi.org/10.1109/SP.2009.25 ISSN: 2375-1207.
  * Zakai (2020) Alon Zakai. 2020\.  WasmBoxC: Simple, Easy, and Fast VM-less Sandboxing.  https://kripken.github.io/blog/wasm/2020/07/27/wasmboxc.html.
  * Zeng et al. (2011) Bin Zeng, Gang Tan, and Greg Morrisett. 2011.  Combining Control-Flow Integrity and Static Analysis for Efficient and Validated Data Sandboxing. In _Proceedings of the 18th ACM Conference on Computer and Communications Security_ (Chicago, Illinois, USA) _(CCS ’11)_. Association for Computing Machinery, New York, NY, USA, 29–40.  https://doi.org/10.1145/2046707.2046713
  * Zhao et al. (2011) Lu Zhao, Guodong Li, Bjorn De Sutter, and John Regehr. 2011\.  ARMor: fully verified software fault isolation. In _Proceedings of the 11th International Conference on Embedded Software, EMSOFT 2011, part of the Seventh Embedded Systems Week, ESWeek 2011, Taipei, Taiwan, October 9-14, 2011_. ACM.  https://doi.org/10.1145/2038642.2038687
  * Zhou et al. (2014) Yajin Zhou, Xiaoguang Wang, Yue Chen, and Zhi Wang. 2014\.  Armlock: Hardware-based fault isolation for arm. In _Proceedings of the 2014 ACM SIGSAC Conference on Computer and Communications Security, Scottsdale, AZ, USA, November 3-7, 2014_. ACM.  https://doi.org/10.1145/2660267.2660344

##  Appendix A Language Definitions

Figure 12 presents the syntax of our sandbox language model. For all programs
we define the regions $M$, $M_{p}$, $H_{p}$, $S_{p}$, $C_{p}$, and $I$.
$M=\mathbb{N}$ and represents the whole memory space. $M_{p}$, $H_{p}$, and
$S_{p}$ are the memory, heap, and stack of the application or library where
the heap and stack sit disjointly inside the memory. $C_{p}$ is set of
instruction indices such that $C(n)=(p,\\_)$. $I$ is the set of import
indices, the beginnings of application functions that the library is allowed
to jump to.

A note on calling convention: arguments are passed on the stack and the return
address is placed above the arguments.

|  | $pc,sp,n,\ell$ | $\in$ | $\mathbb{N}$
---|---|---|---|---
$\mathit{Priv}$ | $\ni$ | $p$ | $\mathrel{\vcentcolon\vcentcolon=}$ | $\mathtt{app}\mid\mathtt{lib}$
$\mathit{Val}$ | $\ni$ | $v$ | $\mathrel{\vcentcolon\vcentcolon=}$ | $n$
$\mathit{Reg}$ | $\ni$ | $r$ | $\mathrel{\vcentcolon\vcentcolon=}$ | $\mathtt{r}_{n}\mid sp\mid pc$
$\mathit{Check}$ | $\ni$ | $k$ | $\in$ | $\mathbb{N}\rightharpoonup\mathbb{N}$
$\mathit{Expr}$ | $\ni$ | $e$ | $\mathrel{\vcentcolon\vcentcolon=}$ | $r\mid v\mid e\oplus e$
$\mathit{Command}$ | $\ni$ | $c$ | $\mathrel{\vcentcolon\vcentcolon=}$ | ${r}\leftarrow\mathtt{pop}_{p}$
|  |  | $\mid$ | $\mathtt{push}_{p}\ {e}$
|  |  | $\mid$ | ${r}\leftarrow\mathtt{load}_{k}\ {e}$
|  |  | $\mid$ | $\mathtt{store}_{k}\ {e}\mathbin{\vcentcolon=}{e}$
|  |  | $\mid$ | ${r}\leftarrow\mathtt{mov}\ {e}$
|  |  | $\mid$ | $\mathtt{call}_{{k}}\ {e}$
|  |  | $\mid$ | $\mathtt{ret}_{{k}}$
|  |  | $\mid$ | $\mathtt{jmp}_{{k}}\ {e}$
|  |  | $\mid$ | $\mathtt{gatecall}_{n}\ {e}$
|  |  | $\mid$ | $\mathtt{gateret}$
$\mathit{Code}$ | $\ni$ | $C$ | $\mathrel{\vcentcolon\vcentcolon=}$ | $\mathbb{N}\rightharpoonup\mathit{Priv}\times\mathit{Command}$
$\mathit{RegVals}$ | $\ni$ | $R$ | $\mathrel{\vcentcolon\vcentcolon=}$ | $\mathit{Reg}\rightarrow\mathit{Val}$
$\mathit{Memory}$ | $\ni$ | $M$ | $\mathrel{\vcentcolon\vcentcolon=}$ | $\mathbb{N}\rightarrow\mathit{Val}$
$\mathit{State}$ | $\ni$ | $\Psi$ | $\mathrel{\vcentcolon\vcentcolon=}$ | $\mathtt{error}$
|  |  | $\mid$ | $\begin{array}[t]{lllll}\\{&pc&\mathrel{\vcentcolon}&\mathbb{N}\\\ &sp&\mathrel{\vcentcolon}&\mathbb{N}\\\ &R&\mathrel{\vcentcolon}&\mathit{RegVals}\\\ &M&\mathrel{\vcentcolon}&\mathit{Memory}\\\ &C&\mathrel{\vcentcolon}&\mathit{Code}&\\}\end{array}$

Figure 12. Syntax

Figure 13 and Figure 15 define the base small-step operational semantics. We
separate this into transitions
${\Psi}\llparenthesis{c}\rrparenthesis\mathrel{\rightarrow}\Psi^{\prime}$ and
error transitions
${\Psi}\llparenthesis{c}\rrparenthesis\mathrel{\rightarrow}\mathtt{error}$.

${\Psi}\llparenthesis{c}\rrparenthesis\mathrel{\rightarrow}\Psi^{\prime}$

$\displaystyle\displaystyle{\hbox{\hskip
88.61395pt\vbox{\hbox{\hskip-88.61395pt\hbox{\hbox{$\displaystyle\displaystyle\Psi.sp\in
S_{p_{s}}$}\hskip 20.00003pt\hbox{\hbox{$\displaystyle\displaystyle
p_{s}\sqsubseteq p$}\hskip
20.00003pt\hbox{\hskip-69.35149pt\hbox{\hbox{$\displaystyle\displaystyle
v=\Psi.M(\Psi.sp)$}\hskip 20.00003pt\hbox{\hbox{$\displaystyle\displaystyle
R^{\prime}=R[r\mapsto
v]$}}}}}}}\vbox{\hbox{\hskip-69.35149pt\hbox{\hbox{$\displaystyle\displaystyle
v=\Psi.M(\Psi.sp)$}\hskip 20.00003pt\hbox{\hbox{$\displaystyle\displaystyle
R^{\prime}=R[r\mapsto v]$}}}}\vbox{}}}}\over\hbox{\hskip
86.4568pt\vbox{\vbox{}\hbox{\hskip-86.45679pt\hbox{\hbox{$\displaystyle\displaystyle{\Psi}\llparenthesis{{r}\leftarrow\mathtt{pop}_{p}}\rrparenthesis\mathrel{\rightarrow}{\Psi}^{++}[sp\mathbin{\vcentcolon=}\Psi.sp-1,R\mathbin{\vcentcolon=}R^{\prime}]$}}}}}}$
$\displaystyle\displaystyle{\hbox{\hskip
111.51541pt\vbox{\hbox{\hskip-111.51541pt\hbox{\hbox{$\displaystyle\displaystyle
v=\mathcal{V}_{\Psi}({e})$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle
sp^{\prime}=\Psi.sp+1$}\hskip
20.00003pt\hbox{\hskip-82.55777pt\hbox{\hbox{$\displaystyle\displaystyle
M^{\prime}=\Psi.M[sp^{\prime}\mapsto v]$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle sp^{\prime}\in
S_{p_{s}}$}\hskip 20.00003pt\hbox{\hbox{$\displaystyle\displaystyle
p_{s}\sqsubseteq
p$}}}}}}}}\vbox{\hbox{\hskip-82.55777pt\hbox{\hbox{$\displaystyle\displaystyle
M^{\prime}=\Psi.M[sp^{\prime}\mapsto v]$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle sp^{\prime}\in
S_{p_{s}}$}\hskip 20.00003pt\hbox{\hbox{$\displaystyle\displaystyle
p_{s}\sqsubseteq p$}}}}}\vbox{}}}}\over\hbox{\hskip
76.28183pt\vbox{\vbox{}\hbox{\hskip-76.28181pt\hbox{\hbox{$\displaystyle\displaystyle{\Psi}\llparenthesis{\mathtt{push}_{p}\
{e}}\rrparenthesis\mathrel{\rightarrow}{\Psi}^{++}[sp\mathbin{\vcentcolon=}sp^{\prime},M\mathbin{\vcentcolon=}M^{\prime}]$}}}}}}$
$\displaystyle\displaystyle{\hbox{\hskip
93.25485pt\vbox{\hbox{\hskip-93.25485pt\hbox{\hbox{$\displaystyle\displaystyle
n=\mathcal{V}_{\Psi}({e})$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle n^{\prime}=k(n)$}\hskip
20.00003pt\hbox{\hskip-68.26328pt\hbox{\hbox{$\displaystyle\displaystyle
v=\Psi.M(n^{\prime})$}\hskip 20.00003pt\hbox{\hbox{$\displaystyle\displaystyle
R^{\prime}=\Psi.R[r\mapsto
v]$}}}}}}}\vbox{\hbox{\hskip-68.26328pt\hbox{\hbox{$\displaystyle\displaystyle
v=\Psi.M(n^{\prime})$}\hskip 20.00003pt\hbox{\hbox{$\displaystyle\displaystyle
R^{\prime}=\Psi.R[r\mapsto v]$}}}}\vbox{}}}}\over\hbox{\hskip
62.95331pt\vbox{\vbox{}\hbox{\hskip-62.95331pt\hbox{\hbox{$\displaystyle\displaystyle{\Psi}\llparenthesis{{r}\leftarrow\mathtt{load}_{k}\
{e}}\rrparenthesis\mathrel{\rightarrow}{\Psi}^{++}[R\mathbin{\vcentcolon=}R^{\prime}]$}}}}}}$
$\displaystyle\displaystyle{\hbox{\hskip
92.17587pt\vbox{\hbox{\hskip-92.17586pt\hbox{\hbox{$\displaystyle\displaystyle
n=\mathcal{V}_{\Psi}({e})$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle
v=\mathcal{V}_{\Psi}({e^{\prime}})$}\hskip
20.00003pt\hbox{\hskip-61.913pt\hbox{\hbox{$\displaystyle\displaystyle
n^{\prime}=k(n)$}\hskip 20.00003pt\hbox{\hbox{$\displaystyle\displaystyle
M^{\prime}=\Psi.M[n^{\prime}\mapsto
v]$}}}}}}}\vbox{\hbox{\hskip-61.913pt\hbox{\hbox{$\displaystyle\displaystyle
n^{\prime}=k(n)$}\hskip 20.00003pt\hbox{\hbox{$\displaystyle\displaystyle
M^{\prime}=\Psi.M[n^{\prime}\mapsto v]$}}}}\vbox{}}}}\over\hbox{\hskip
67.09773pt\vbox{\vbox{}\hbox{\hskip-67.09773pt\hbox{\hbox{$\displaystyle\displaystyle{\Psi}\llparenthesis{\mathtt{store}_{k}\
{e}\mathbin{\vcentcolon=}{e^{\prime}}}\rrparenthesis\mathrel{\rightarrow}{\Psi}^{++}[M\mathbin{\vcentcolon=}M^{\prime}]$}}}}}}$
$\displaystyle\displaystyle{\hbox{\hskip
60.13002pt\vbox{\hbox{\hskip-60.13002pt\hbox{\hbox{$\displaystyle\displaystyle
v=\mathcal{V}_{\Psi}({e})$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle R^{\prime}=\Psi.R[r\mapsto
v]$}}}}\vbox{}}}\over\hbox{\hskip
61.40749pt\vbox{\vbox{}\hbox{\hskip-61.40747pt\hbox{\hbox{$\displaystyle\displaystyle{\Psi}\llparenthesis{{r}\leftarrow\mathtt{mov}\
{e}}\rrparenthesis\mathrel{\rightarrow}{\Psi}^{++}[R\mathbin{\vcentcolon=}R^{\prime}]$}}}}}}$
$\displaystyle\displaystyle{\hbox{\hskip
138.06267pt\vbox{\hbox{\hskip-138.06267pt\hbox{\hbox{$\displaystyle\displaystyle
n=\mathcal{V}_{\Psi}({e})$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle n^{\prime}=k(n)$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle
sp^{\prime}=\Psi.sp+1$}\hskip
20.00003pt\hbox{\hskip-77.45706pt\hbox{\hbox{$\displaystyle\displaystyle
M^{\prime}=\Psi.M[sp^{\prime}\mapsto\Psi.pc+1]$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle sp^{\prime}\in
S_{p_{s}}$}}}}}}}}\vbox{\hbox{\hskip-77.45706pt\hbox{\hbox{$\displaystyle\displaystyle
M^{\prime}=\Psi.M[sp^{\prime}\mapsto\Psi.pc+1]$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle sp^{\prime}\in
S_{p_{s}}$}}}}\vbox{}}}}\over\hbox{\hskip
85.20834pt\vbox{\vbox{}\hbox{\hskip-85.20834pt\hbox{\hbox{$\displaystyle\displaystyle{\Psi}\llparenthesis{\mathtt{call}_{{k}}\
{e}}\rrparenthesis\mathrel{\rightarrow}\Psi[pc\mathbin{\vcentcolon=}n^{\prime},sp\mathbin{\vcentcolon=}sp^{\prime},M\mathbin{\vcentcolon=}M^{\prime}]$}}}}}}$
$\displaystyle\displaystyle{\hbox{\hskip
49.1232pt\vbox{\hbox{\hskip-49.12318pt\hbox{\hbox{$\displaystyle\displaystyle
n=\mathcal{V}_{\Psi}({e})$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle
n^{\prime}=k(n)$}}}}\vbox{}}}\over\hbox{\hskip
49.13019pt\vbox{\vbox{}\hbox{\hskip-49.13017pt\hbox{\hbox{$\displaystyle\displaystyle{\Psi}\llparenthesis{\mathtt{jmp}_{{k}}\
{e}}\rrparenthesis\mathrel{\rightarrow}\Psi[pc\mathbin{\vcentcolon=}n^{\prime}]$}}}}}}$
$\displaystyle\displaystyle{\hbox{\hskip
70.98663pt\vbox{\hbox{\hskip-70.98662pt\hbox{\hbox{$\displaystyle\displaystyle
n=\Psi.M(\Psi.sp)$}\hskip
20.00003pt\hbox{\hskip-51.0161pt\hbox{\hbox{$\displaystyle\displaystyle
n^{\prime}=k(n)$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Psi.sp\in
S_{p_{s}}$}}}}}}\vbox{\hbox{\hskip-51.0161pt\hbox{\hbox{$\displaystyle\displaystyle
n^{\prime}=k(n)$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Psi.sp\in
S_{p_{s}}$}}}}\vbox{}}}}\over\hbox{\hskip
71.39572pt\vbox{\vbox{}\hbox{\hskip-71.39572pt\hbox{\hbox{$\displaystyle\displaystyle{\Psi}\llparenthesis{\mathtt{ret}_{{k}}}\rrparenthesis\mathrel{\rightarrow}\Psi[pc\mathbin{\vcentcolon=}n^{\prime},sp\mathbin{\vcentcolon=}\Psi.sp-1]$}}}}}}$
$\displaystyle\displaystyle{\hbox{\hskip
20.02559pt\vbox{\hbox{\hskip-20.02557pt\hbox{\hbox{$\displaystyle\displaystyle
v=\mathcal{V}_{\Psi}({e})$}}}\vbox{}}}\over\hbox{\hskip
62.89441pt\vbox{\vbox{}\hbox{\hskip-62.8944pt\hbox{\hbox{$\displaystyle\displaystyle{\Psi}\llparenthesis{{sp}\leftarrow\mathtt{mov}\
{e}}\rrparenthesis\mathrel{\rightarrow}{\Psi}^{++}[sp\mathbin{\vcentcolon=}v]$}}}}}}$

Figure 13. Operational Semantics

${\Psi}\llparenthesis{c}\rrparenthesis\mathrel{\rightarrow}\mathtt{error}$

$\displaystyle\displaystyle{\hbox{\hskip
49.07704pt\vbox{\hbox{\hskip-49.07704pt\hbox{\hbox{$\displaystyle\displaystyle\Psi.sp\in
S_{p_{s}}$}\hskip 20.00003pt\hbox{\hbox{$\displaystyle\displaystyle
p_{s}\not\sqsubseteq p$}}}}\vbox{}}}\over\hbox{\hskip
42.87292pt\vbox{\vbox{}\hbox{\hskip-42.87291pt\hbox{\hbox{$\displaystyle\displaystyle{\Psi}\llparenthesis{{r}\leftarrow\mathtt{pop}_{p}}\rrparenthesis\mathrel{\rightarrow}\mathtt{error}$}}}}}}$
$\displaystyle\displaystyle{\hbox{\hskip
57.68813pt\vbox{\hbox{\hskip-57.68811pt\hbox{\hbox{$\displaystyle\displaystyle\Psi.sp+1\in
S_{p_{s}}$}\hskip 20.00003pt\hbox{\hbox{$\displaystyle\displaystyle
p_{s}\not\sqsubseteq p$}}}}\vbox{}}}\over\hbox{\hskip
41.02861pt\vbox{\vbox{}\hbox{\hskip-41.02861pt\hbox{\hbox{$\displaystyle\displaystyle{\Psi}\llparenthesis{\mathtt{push}_{p}\
{e}}\rrparenthesis\mathrel{\rightarrow}\mathtt{error}$}}}}}}$
$\displaystyle\displaystyle{\hbox{\hskip
62.99098pt\vbox{\hbox{\hskip-62.99098pt\hbox{\hbox{$\displaystyle\displaystyle
n=\mathcal{V}_{\Psi}({e})$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle k(n)\text{
undefined}$}}}}\vbox{}}}\over\hbox{\hskip
48.81035pt\vbox{\vbox{}\hbox{\hskip-48.81035pt\hbox{\hbox{$\displaystyle\displaystyle{\Psi}\llparenthesis{{r}\leftarrow\mathtt{load}_{k}\
{e}}\rrparenthesis\mathrel{\rightarrow}\mathtt{error}$}}}}}}$
$\displaystyle\displaystyle{\hbox{\hskip
62.99098pt\vbox{\hbox{\hskip-62.99098pt\hbox{\hbox{$\displaystyle\displaystyle
n=\mathcal{V}_{\Psi}({e})$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle k(n)\text{
undefined}$}}}}\vbox{}}}\over\hbox{\hskip
49.83327pt\vbox{\vbox{}\hbox{\hskip-49.83327pt\hbox{\hbox{$\displaystyle\displaystyle{\Psi}\llparenthesis{\mathtt{store}_{k}\
{e}\mathbin{\vcentcolon=}{e^{\prime}}}\rrparenthesis\mathrel{\rightarrow}\mathtt{error}$}}}}}}$
$\displaystyle\displaystyle{\hbox{\hskip
41.34442pt\vbox{\hbox{\hskip-41.3444pt\hbox{\hbox{$\displaystyle\displaystyle$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Psi.sp+1\notin
S_{p_{s}}$}}}}\vbox{}}}\over\hbox{\hskip
38.36012pt\vbox{\vbox{}\hbox{\hskip-38.36012pt\hbox{\hbox{$\displaystyle\displaystyle{\Psi}\llparenthesis{\mathtt{call}_{{k}}\
{e}}\rrparenthesis\mathrel{\rightarrow}\mathtt{error}$}}}}}}$
$\displaystyle\displaystyle{\hbox{\hskip
62.99098pt\vbox{\hbox{\hskip-62.99098pt\hbox{\hbox{$\displaystyle\displaystyle
n=\mathcal{V}_{\Psi}({e})$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle k(n)\text{
undefined}$}}}}\vbox{}}}\over\hbox{\hskip
38.36012pt\vbox{\vbox{}\hbox{\hskip-38.36012pt\hbox{\hbox{$\displaystyle\displaystyle{\Psi}\llparenthesis{\mathtt{call}_{{k}}\
{e}}\rrparenthesis\mathrel{\rightarrow}\mathtt{error}$}}}}}}$
$\displaystyle\displaystyle{\hbox{\hskip
32.73334pt\vbox{\hbox{\hskip-32.73334pt\hbox{\hbox{$\displaystyle\displaystyle$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Psi.sp\notin
S_{p_{s}}$}}}}\vbox{}}}\over\hbox{\hskip
32.15698pt\vbox{\vbox{}\hbox{\hskip-32.15698pt\hbox{\hbox{$\displaystyle\displaystyle{\Psi}\llparenthesis{\mathtt{ret}_{{k}}}\rrparenthesis\mathrel{\rightarrow}\mathtt{error}$}}}}}}$
$\displaystyle\displaystyle{\hbox{\hskip
78.04579pt\vbox{\hbox{\hskip-78.04578pt\hbox{\hbox{$\displaystyle\displaystyle
n=\Psi.M(\Psi.sp)$}\hskip 20.00003pt\hbox{\hbox{$\displaystyle\displaystyle
k(n)\text{ undefined}$}}}}\vbox{}}}\over\hbox{\hskip
32.15698pt\vbox{\vbox{}\hbox{\hskip-32.15698pt\hbox{\hbox{$\displaystyle\displaystyle{\Psi}\llparenthesis{\mathtt{ret}_{{k}}}\rrparenthesis\mathrel{\rightarrow}\mathtt{error}$}}}}}}$
$\displaystyle\displaystyle{\hbox{\hskip
62.99098pt\vbox{\hbox{\hskip-62.99098pt\hbox{\hbox{$\displaystyle\displaystyle
n=\mathcal{V}_{\Psi}({e})$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle k(n)\text{
undefined}$}}}}\vbox{}}}\over\hbox{\hskip
39.33237pt\vbox{\vbox{}\hbox{\hskip-39.33235pt\hbox{\hbox{$\displaystyle\displaystyle{\Psi}\llparenthesis{\mathtt{jmp}_{{k}}\
{e}}\rrparenthesis\mathrel{\rightarrow}\mathtt{error}$}}}}}}$

Figure 14. Operational Semantics

$\displaystyle{\hbox{$\displaystyle\displaystyle{\hbox{\hskip
37.02438pt\vbox{\hbox{\hskip-37.02437pt\hbox{\hbox{$\displaystyle\displaystyle
C(\Psi.pc)=(\\_,c)$}}}\vbox{}}}\over\hbox{\hskip
13.55269pt\vbox{\vbox{}\hbox{\hskip-13.55267pt\hbox{\hbox{$\displaystyle\displaystyle{\Psi}\llparenthesis{c}\rrparenthesis$}}}}}}$}}\penalty
50\hskip 20.00003pt plus 0.5fil minus
5.0pt{\hbox{$\displaystyle\displaystyle{\hbox{\hskip
35.79001pt\vbox{\hbox{\hskip-35.79pt\hbox{\hbox{$\displaystyle\displaystyle
C(\Psi.pc)=(p,c)$}}}\vbox{}}}\over\hbox{\hskip
14.96144pt\vbox{\vbox{}\hbox{\hskip-14.96143pt\hbox{\hbox{$\displaystyle\displaystyle{\Psi}\llparenthesis{c}\rrparenthesis_{p}$}}}}}}$}}\penalty
50\hskip 20.00003pt plus 0.5fil minus
5.0pt{\hbox{$\displaystyle\displaystyle{\hbox{\hskip
60.35612pt\vbox{\hbox{\hskip-52.62589pt\hbox{\hbox{$\displaystyle\displaystyle\Psi\mathrel{\mathrel{\rightarrow}^{\ast}}\Psi^{\prime}$}\hskip
20.00003pt\hbox{\hskip-60.35611pt\hbox{\hbox{$\displaystyle\displaystyle\neg\exists\Psi^{\prime\prime}.\leavevmode\nobreak\
\Psi^{\prime}\mathrel{\rightarrow}\Psi^{\prime\prime}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Psi^{\prime}\neq\mathtt{error}$}}}}}}\vbox{\hbox{\hskip-60.35611pt\hbox{\hbox{$\displaystyle\displaystyle\neg\exists\Psi^{\prime\prime}.\leavevmode\nobreak\
\Psi^{\prime}\mathrel{\rightarrow}\Psi^{\prime\prime}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Psi^{\prime}\neq\mathtt{error}$}}}}\vbox{}}}}\over\hbox{\hskip
11.60336pt\vbox{\vbox{}\hbox{\hskip-11.60335pt\hbox{\hbox{$\displaystyle\displaystyle\Psi\mathrel{\Downarrow}\Psi^{\prime}$}}}}}}$}}\penalty
50\hskip 20.00003pt plus 0.5fil minus
5.0pt\mathtt{lib}\sqsubseteq\mathtt{app}$
$\begin{array}[]{rcl}\mathcal{V}_{\Psi}({v})&\triangleq&v\\\
\mathcal{V}_{\Psi}({r})&\triangleq&\Psi.R(r)\\\
\mathcal{V}_{\Psi}({sp})&\triangleq&\Psi.sp\\\
\mathcal{V}_{\Psi}({pc})&\triangleq&\Psi.pc\\\ \mathcal{V}_{\Psi}({e\oplus
e^{\prime}})&\triangleq&\mathcal{V}_{\Psi}({e})\oplus\mathcal{V}_{\Psi}({e^{\prime}})\\\
\\\
{\Psi}^{++}&\triangleq&\begin{cases}\Psi[pc\mathbin{\vcentcolon=}\Psi.pc+1]&\text{when
}\pi_{1}(\Psi.C(\Psi.pc))=\pi_{1}(\Psi.C(\Psi.pc+1))\\\
\mathtt{error}&\text{otherwise}\end{cases}\end{array}$

Figure 15. Operational Semantics: Auxiliary Definitions

Figure 16 defines unguarded derived forms for memory operations.

$\begin{array}[]{rcl}{r}\leftarrow\mathtt{pop}&\triangleq&{r}\leftarrow\mathtt{pop}_{\top}\\\
\mathtt{push}\ {e}&\triangleq&\mathtt{push}_{\top}\ {e}\\\
{r}\leftarrow\mathtt{load}\ {e}&\triangleq&{r}\leftarrow\mathtt{load}_{id}\
{e}\\\ \mathtt{store}\
{e}\mathbin{\vcentcolon=}{e^{\prime}}&\triangleq&\mathtt{store}_{id}\
{e}\mathbin{\vcentcolon=}{e^{\prime}}\\\ \mathtt{jmp}\
{e}&\triangleq&\mathtt{jmp}_{{id}}\ {e}\\\ \mathtt{call}\
{e}&\triangleq&\mathtt{call}_{{id}}\ {e}\\\
\mathtt{ret}&\triangleq&\mathtt{ret}_{{id}}\\\ \end{array}$

Figure 16. Derived Forms

###  A.1. Sandbox Properties

$\displaystyle\displaystyle{\hbox{\hskip
76.37122pt\vbox{\hbox{\hskip-76.3712pt\hbox{\hbox{$\displaystyle\displaystyle\Psi_{1}\mathrel{\rightarrow}\Psi_{2}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle{\Psi_{1}}\llparenthesis{c_{1}}\rrparenthesis_{p_{1}}$}\hskip
20.00003pt\hbox{\hskip-49.46384pt\hbox{\hbox{$\displaystyle\displaystyle{\Psi_{2}}\llparenthesis{c_{2}}\rrparenthesis_{p_{2}}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle
p_{1}=p_{2}=p$}}}}}}}\vbox{\hbox{\hskip-49.46384pt\hbox{\hbox{$\displaystyle\displaystyle{\Psi_{2}}\llparenthesis{c_{2}}\rrparenthesis_{p_{2}}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle
p_{1}=p_{2}=p$}}}}\vbox{}}}}\over\hbox{\hskip
15.59344pt\vbox{\vbox{}\hbox{\hskip-15.59343pt\hbox{\hbox{$\displaystyle\displaystyle\Psi_{1}\mathrel{\xrightarrow{p}}\Psi_{2}$}}}}}}$
$\displaystyle\displaystyle{\hbox{\hskip
13.56343pt\vbox{\hbox{\hskip-13.56343pt\hbox{\hbox{$\displaystyle\displaystyle\Psi\mathrel{\xrightarrow{p}}\Psi^{\prime}$}}}\vbox{}}}\over\hbox{\hskip
14.1034pt\vbox{\vbox{}\hbox{\hskip-14.1034pt\hbox{\hbox{$\displaystyle\displaystyle\Psi\mathrel{\xrightarrow{\\!\square}}\Psi^{\prime}$}}}}}}$
$\displaystyle\displaystyle{\hbox{\hskip
16.6034pt\vbox{\hbox{\hskip-16.6034pt\hbox{\hbox{$\displaystyle\displaystyle\Psi\mathrel{\xrightarrow{\\!\text{wb}}}\Psi^{\prime}$}}}\vbox{}}}\over\hbox{\hskip
14.1034pt\vbox{\vbox{}\hbox{\hskip-14.1034pt\hbox{\hbox{$\displaystyle\displaystyle\Psi\mathrel{\xrightarrow{\\!\square}}\Psi^{\prime}$}}}}}}$
$\displaystyle\displaystyle{\hbox{\hskip
79.90375pt\vbox{\hbox{\hskip-79.90373pt\hbox{\hbox{$\displaystyle\displaystyle\Psi\mathrel{\rightarrow}\Psi_{1}\mathrel{\xrightarrow{\\!\square}\mathrel{\vphantom{\to}{}^{\ast}}}\Psi_{2}\mathrel{\rightarrow}\Psi^{\prime}$}\hskip
20.00003pt\hbox{\hskip-72.645pt\hbox{\hbox{$\displaystyle\displaystyle{\Psi}\llparenthesis{\mathtt{gatecall}_{n}\
{e}}\rrparenthesis$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle{\Psi_{2}}\llparenthesis{\mathtt{gateret}}\rrparenthesis$}}}}}}\vbox{\hbox{\hskip-72.645pt\hbox{\hbox{$\displaystyle\displaystyle{\Psi}\llparenthesis{\mathtt{gatecall}_{n}\
{e}}\rrparenthesis$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle{\Psi_{2}}\llparenthesis{\mathtt{gateret}}\rrparenthesis$}}}}\vbox{}}}}\over\hbox{\hskip
16.6034pt\vbox{\vbox{}\hbox{\hskip-16.6034pt\hbox{\hbox{$\displaystyle\displaystyle\Psi\mathrel{\xrightarrow{\\!\text{wb}}}\Psi^{\prime}$}}}}}}$

Figure 17. Well-Bracketed Transitions

####  A.1.1. Integrity

Integrity is all about maintaining application invariants across calls into
the sandbox. These invariants vary significantly from program to program, so
to capture this generality we define $\mathcal{I}$-Integrity and then
instantiate it in several specific instances.

###### Definition 0 ($\mathcal{I}$-Integrity).

Let
$\mathcal{I}:\mathit{Trace}\times\mathit{State}\times\mathit{State}\rightarrow\mathbb{P}$.
We say that an SFI transition systems has $\mathcal{I}$-integrity if
$\Psi_{0}\in\mathit{Program}$,
$\pi=\Psi_{0}\mathrel{\mathrel{\rightarrow}^{\ast}}\Psi_{1}$,
${\Psi_{1}}\llparenthesis{\\_}\rrparenthesis_{\mathtt{app}}$, and
$\Psi_{1}\mathrel{\xrightarrow{\\!\text{wb}}}\Psi_{2}$ imply that
$\mathcal{I}(\pi,\Psi_{1},\Psi_{2})$.

Informally, callee-save register integrity says that the values of callee-save
registers are restored by gated calls into the sandbox:

###### Definition 0 (Callee-Save Register Integrity).

Let $\mathbb{CSR}$ be the list of callee-save registers and define

$\mathcal{CSR}(\\_,\Psi_{1},\Psi_{2})\triangleq\Psi_{1}.R(\mathbb{CSR})=\Psi_{2}.R(\mathbb{CSR}).$

If an SFI transition system has $\mathcal{CSR}$-integrity then we say the
system has callee-save register integrity.

$\displaystyle\operatorname{return-address}_{p}$
$\displaystyle:\mathit{Trace}\rightarrow\wp({\mathbb{N}})$
$\displaystyle\operatorname{return-
address}_{p}(\Psi_{0}\mathrel{\mathrel{\rightarrow}^{\ast}}{\Psi}\llparenthesis{\mathtt{call}_{{k}}\
{e}}\rrparenthesis_{p}\mathrel{\rightarrow}\Psi^{\prime})$
$\displaystyle\triangleq\operatorname{return-
address}_{p}(\Psi_{0}\mathrel{\mathrel{\rightarrow}^{\ast}}\Psi)\cup\\{\Psi.sp+1\\}$
$\displaystyle\operatorname{return-
address}_{p}(\Psi_{0}\mathrel{\mathrel{\rightarrow}^{\ast}}{\Psi}\llparenthesis{\mathtt{ret}_{{k}}}\rrparenthesis_{p}\mathrel{\rightarrow}\Psi^{\prime})$
$\displaystyle\triangleq\operatorname{return-
address}_{p}(\Psi_{0}\mathrel{\mathrel{\rightarrow}^{\ast}}\Psi)-\\{\Psi.sp\\}$
$\displaystyle\operatorname{return-
address}_{p}(\Psi_{0}\mathrel{\mathrel{\rightarrow}^{\ast}}{\Psi}\llparenthesis{\mathtt{gatecall}_{n}\
{e}}\rrparenthesis_{p}\mathrel{\rightarrow}\Psi^{\prime})$
$\displaystyle\triangleq\operatorname{return-
address}_{p}(\Psi_{0}\mathrel{\mathrel{\rightarrow}^{\ast}}\Psi)\cup\\{\Psi.sp+1\\}$
$\displaystyle\operatorname{return-
address}_{p}(\Psi_{0}\mathrel{\mathrel{\rightarrow}^{\ast}}{\Psi}\llparenthesis{\mathtt{gateret}}\rrparenthesis_{p}\mathrel{\rightarrow}\Psi^{\prime})$
$\displaystyle\triangleq\operatorname{return-
address}_{p}(\Psi_{0}\mathrel{\mathrel{\rightarrow}^{\ast}}\Psi)-\\{\Psi.sp\\}$
$\displaystyle\operatorname{return-
address}_{p}(\Psi_{0}\mathrel{\mathrel{\rightarrow}^{\ast}}{\Psi}\llparenthesis{c}\rrparenthesis\mathrel{\rightarrow}\Psi^{\prime})$
$\displaystyle\triangleq\operatorname{return-
address}_{p}(\Psi_{0}\mathrel{\mathrel{\rightarrow}^{\ast}}\Psi)$
$\displaystyle\operatorname{return-
address}_{p}(\Psi_{0}\mathrel{\mathrel{\rightarrow}^{0}}\Psi_{0})$
$\displaystyle\triangleq\emptyset$

Figure 18. Call stack return address calculation

###### Definition 0 (Return Address Integrity).

Define

$\displaystyle\mathcal{RA}(\pi,\Psi_{1},\Psi_{2})\triangleq(\Psi_{1}.M(\operatorname{return-
address}_{\mathtt{app}}(\pi))$ $\displaystyle=\Psi_{2}.M(\operatorname{return-
address}_{\mathtt{app}}(\pi)))$
$\displaystyle{}\wedge(\Psi_{2}.sp=\Psi_{1}.sp)\wedge(\Psi_{2}.pc=\Psi_{1}.pc+1)$

If an SFI transition system has $\mathcal{RA}$-integrity then we say the
system has return address integrity.

####  A.1.2. Confidentiality

A confidentiality policy is defined by a partial function
$\mathbb{C}\in\mathit{State}\rightharpoonup(\mathbb{N}\mathrel{+}\mathit{Reg}\rightarrow\mathit{Priv})$.
The domain of $\mathbb{C}$ must include all $\Psi$ such that $\Psi$ is a
program state where the application is making a gated call into the library,
that is, where
$\Psi_{0}.C(\Psi.pc)=(\mathtt{app},\mathtt{gatecall}_{n^{\prime}}\ {e})$.
$\mathbb{C}$ captures which registers and memory slots are labelled
confidential ($\mathtt{app}$) or public ($\mathtt{lib}$) at a gated call into
the sandbox. In the following we use $f|_{X}$ for the restriction of the
function $f:A\rightarrow B$ to a subset $X\subseteq A$.

We say $\Psi=_{\mathbb{C}}\Psi^{\prime}$ when

  1. (1)

$\Psi.pc=\Psi^{\prime}.pc$

  2. (2)

$\Psi.sp=\Psi^{\prime}.sp$

  3. (3)

${\Psi}\llparenthesis{\mathtt{gatecall}_{n}\
{e}}\rrparenthesis_{\mathtt{app}}$ and
${\Psi^{\prime}}\llparenthesis{\mathtt{gatecall}_{n}\
{e}}\rrparenthesis_{\mathtt{app}}$

  4. (4)

$\Psi.R|_{\\{r\mid\mathbb{C}(\Psi)(r)=\mathtt{lib}\\}}=\Psi^{\prime}.R|_{\\{r\mid\mathbb{C}(\Psi^{\prime})(r)=\mathtt{lib}\\}}$

  5. (5)

$\Psi.M|_{\\{n\mid\mathbb{C}(\Psi)(n)=\mathtt{lib}\\}}=\Psi^{\prime}.M|_{\\{n\mid\mathbb{C}(\Psi^{\prime})(n)=\mathtt{lib}\\}}$

We then define two notions of observational equivalence.

###### Definition 0.

We say $\Psi=_{\mathtt{call}\ n}\Psi^{\prime}$ if

  1. (1)

$\Psi.M(H_{\mathtt{lib}})=\Psi^{\prime}.M(H_{\mathtt{lib}})$

  2. (2)

$\Psi.pc=\Psi^{\prime}.pc$

  3. (3)

$\Psi.sp=\Psi^{\prime}.sp$

  4. (4)

For all $i\in[1,n]$, there exists some $n^{\prime}$ such that
$n^{\prime}=\Psi.M(\Psi.sp-i)=\Psi^{\prime}.M(\Psi.sp-i)$.

Second, let $r_{ret}$ be the calling convention return register.

###### Definition 0.

We say $\Psi=_{\mathtt{ret}}\Psi^{\prime}$ if

  1. (1)

$\Psi.M(H_{\mathtt{lib}})=\Psi^{\prime}.M(H_{\mathtt{lib}})$

  2. (2)

$\Psi.pc=\Psi^{\prime}.pc$

  3. (3)

There exists some $n$ such that $n=\Psi.R(r_{ret})=\Psi^{\prime}.R(r_{ret})$.

###### Definition 0 (Disjoint Noninterference).

We say that an SFI transition system has the disjoint noninterference property
if, for all initial configurations and their confidentiality properties
$(\Psi_{0},\mathbb{C})\in\mathit{Program}$, traces
$\Psi_{0}\mathrel{\mathrel{\rightarrow}^{\ast}}\Psi_{1}\mathrel{\rightarrow}\Psi_{2}\mathrel{\xrightarrow{\mathtt{lib}}\mathrel{\vphantom{\to}{}^{\ast}}}\Psi_{3}\mathrel{\rightarrow}\Psi_{4}$,
where $\Psi_{1}$ is a gated call into the library
${\Psi_{1}}\llparenthesis{\mathtt{gatecall}_{n}\
{e}}\rrparenthesis_{\mathtt{app}}$, and
$\Psi_{3}\mathrel{\rightarrow}\Psi_{4}$ leaves the library and reenters the
application (${\Psi_{4}}\llparenthesis{\\_}\rrparenthesis_{\mathtt{app}}$),
and, for all $\Psi_{1}^{\prime}$ such that
$\Psi_{1}=_{\mathbb{C}}\Psi_{1}^{\prime}$, we have that
$\Psi_{1}^{\prime}\mathrel{\rightarrow}\Psi_{2}^{\prime}\mathrel{\xrightarrow{\mathtt{lib}}\mathrel{\vphantom{\to}{}^{\ast}}}\Psi_{3}^{\prime}\mathrel{\rightarrow}\Psi_{4}^{\prime}$,
${\Psi_{4}^{\prime}}\llparenthesis{\\_}\rrparenthesis_{\mathtt{app}}$,
$\Psi_{4}.pc=\Psi_{4}^{\prime}.pc$, and

  1. (1)

$\Psi_{3}$ is a gated call to the application
(${\Psi_{3}}\llparenthesis{\mathtt{gatecall}_{m}\ {e}}\rrparenthesis$ and
${\Psi_{3}^{\prime}}\llparenthesis{\mathtt{gatecall}_{m}\ {e}}\rrparenthesis$)
and $\Psi_{4}=_{\mathtt{call}\ m}\Psi_{4}^{\prime}$ or

  2. (2)

$\Psi_{3}$ is a gated return to the application
(${\Psi_{3}}\llparenthesis{\mathtt{gateret}}\rrparenthesis$ and
${\Psi_{3}^{\prime}}\llparenthesis{\mathtt{gateret}}\rrparenthesis$) and
$\Psi_{4}=_{\mathtt{ret}}\Psi_{4}^{\prime}$.

##  Appendix B NaCl

NaCl context in application
---
$ctx-0$ | library stack pointer
$\ldots$ |
$ctx^{\ast}$ | $ctx$
NaCl context in library
$ctx-0$ | application stack pointer
$ctx-1$ | $\mathbb{CSR}_{0}$
$ctx-2$ | $\mathbb{CSR}_{1}$
$\ldots$ | …
$ctx-\operatorname{len}(\mathbb{CSR})$ | $\mathbb{CSR}_{\operatorname{len}(\mathbb{CSR})-1}$
$\ldots$ |
$ctx^{\ast}$ | $ctx$

Figure 19. Transition Context Layout

$\operatorname{nacl-springboard}(n,e)\triangleq$ |
---|---
| ${r_{0}}\leftarrow\mathtt{load}\ {ctx^{\ast}}$ |
| ${r_{1}}\leftarrow\mathtt{load}\ {r_{0}}$ |  // $r_{1}$ holds the library stack pointer
$j\in(\operatorname{len}(\mathbb{CSR}),0]$ | $\overline{\mathtt{store}\ {r_{0}}\mathbin{\vcentcolon=}{\mathbb{CSR}_{j}};{r_{0}}\leftarrow\mathtt{mov}\ {r_{0}+1}}$ | // save callee-save registers
| ${r_{1}}\leftarrow\mathtt{mov}\ {r_{1}+n}$ |  // set $r_{1}$ to the new top of the library stack
| ${sp}\leftarrow\mathtt{mov}\ {sp-1}$ | // move the stack pointer to the first argument
$j\in[0,n)$ | $\overline{{r_{2}}\leftarrow\mathtt{pop};\mathtt{store}_{M_{\mathtt{lib}}}\ {r_{1}}\mathbin{\vcentcolon=}{r_{2}};{r_{1}}\leftarrow\mathtt{mov}\ {r_{1}-1}}$ | // copy arguments to library stack
| ${r_{2}}\leftarrow\mathtt{mov}\ {sp+(n+1)};\mathtt{store}\ {r_{0}}\mathbin{\vcentcolon=}{r_{2}}$ | // save stack pointer
| ${sp}\leftarrow\mathtt{mov}\ {r_{1}+n}$ | // set new stack pointer
| $\mathtt{store}\ {ctx^{\ast}}\mathbin{\vcentcolon=}{r_{0}}$ |  // update $ctx$
$r\in\mathbb{R}$ | $\overline{{r}\leftarrow\mathtt{mov}\ {0}}$ | // clear registers
| $\mathtt{jmp}\ {e}$ |

$\operatorname{nacl-trampoline}\triangleq$ |
---|---
| ${r_{0}}\leftarrow\mathtt{load}\ {ctx^{\ast}}$ |
$j\in[0,\operatorname{len}(\mathbb{CSR}))$ | $\overline{{r_{0}}\leftarrow\mathtt{mov}\ {r_{0}-1};{\mathbb{CSR}_{j}}\leftarrow\mathtt{load}\ {r_{0}}}$ | // restore callee-save registers
| ${r_{0}}\leftarrow\mathtt{load}\ {ctx^{\ast}}$ |
| ${r_{1}}\leftarrow\mathtt{load}\ {r_{0}}$ |  // $r_{1}$ holds the application stack pointer
| ${r_{0}}\leftarrow\mathtt{mov}\ {r_{0}-\operatorname{len}(\mathbb{CSR})};\mathtt{store}\ {r_{0}}\mathbin{\vcentcolon=}{sp}$ | // save library stack pointer
| $\mathtt{store}\ {ctx^{\ast}}\mathbin{\vcentcolon=}{r_{0}}$ |  // update $ctx$
| ${sp}\leftarrow\mathtt{mov}\ {r_{1}}$ | // switch to application stack
| $\mathtt{ret}$ |

$\operatorname{nacl-cb-springboard}(n,e)\triangleq$ |
---|---
| ${r_{0}}\leftarrow\mathtt{load}\ {ctx^{\ast}}$ |
| ${r_{1}}\leftarrow\mathtt{load}\ {r_{0}}$ |  // $r_{1}$ holds the application stack pointer
| ${r_{0}}\leftarrow\mathtt{mov}\ {r_{0}+1};\mathtt{store}\ {r_{0}}\mathbin{\vcentcolon=}{sp}$ | // save stack pointer
| $\mathtt{store}\ {ctx^{\ast}}\mathbin{\vcentcolon=}{r_{0}}$ |  // update $ctx$
| ${sp}\leftarrow\mathtt{mov}\ {sp-1}$ | // move the stack pointer to the first argument
| ${r_{1}}\leftarrow\mathtt{mov}\ {r_{1}+n}$ |  // set $r_{1}$ to the new top of the library stack
$j\in[0,n)$ | $\overline{{r_{2}}\leftarrow\mathtt{pop}_{M_{\mathtt{lib}}};\mathtt{store}\ {r_{1}}\mathbin{\vcentcolon=}{r_{2}};{r_{1}}\leftarrow\mathtt{mov}\ {r_{1}-1}}$ | // copy arguments to application stack
| ${sp}\leftarrow\mathtt{mov}\ {r_{1}+n}$ | // set new stack pointer
| $\mathtt{jmp}_{{I}}\ {e}$ |

$\operatorname{nacl-cb-trampoline}\triangleq$ |
---|---
| ${r_{0}}\leftarrow\mathtt{load}\ {ctx^{\ast}}$ |
| ${r_{1}}\leftarrow\mathtt{load}\ {r_{0}}$ |  // $r_{1}$ holds the library stack pointer
| ${r_{0}}\leftarrow\mathtt{mov}\ {r_{0}-1};\mathtt{store}\ {ctx^{\ast}}\mathbin{\vcentcolon=}{r_{0}}$ |  // update $ctx$
| ${sp}\leftarrow\mathtt{mov}\ {r_{1}}$ | // switch to library stack
$r\in\mathbb{R}$ | $\overline{{r}\leftarrow\mathtt{mov}\ {0}}$ | // clear registers
| $\mathtt{ret}_{{C_{\mathtt{lib}}}}$ |

###  B.1. Programs

A NaCl program $\Psi$ is defined by the following conditions:

  1. (1)

All memory operations in the sandboxed library are guarded:

$\displaystyle\forall n.$
$\displaystyle\Psi.C(n)=(\mathtt{lib},{r}\leftarrow\mathtt{pop}_{p})\Longrightarrow
p=\mathtt{lib}$ $\displaystyle\Psi.C(n)=(\mathtt{lib},\mathtt{push}_{p}\
{e})\Longrightarrow p=\mathtt{lib}$
$\displaystyle\Psi.C(n)=(\mathtt{lib},{r}\leftarrow\mathtt{load}_{k}\
{e})\Longrightarrow\operatorname{cod}({k})\subseteq M_{\mathtt{lib}}$
$\displaystyle\Psi.C(n)=(\mathtt{lib},\mathtt{store}_{k}\
{e}\mathbin{\vcentcolon=}{e^{\prime}})\Longrightarrow\operatorname{cod}({k})\subseteq
M_{\mathtt{lib}}.$

  2. (2)

The application does not write $\mathtt{app}$ data to the sandbox memory.

  3. (3)

Gated calls are the only way to move between application and library code:

$\displaystyle\forall n.$ $\displaystyle\Psi.C(n)=(p,\mathtt{call}_{{k}}\
{e})\Longrightarrow\operatorname{cod}({k})\subseteq C_{p}$
$\displaystyle\Psi.C(n)=(p,\mathtt{ret}_{{k}})\Longrightarrow\operatorname{cod}({k})\subseteq
C_{p}$ $\displaystyle\Psi.C(n)=(p,\mathtt{jmp}_{{k}}\
{e})\Longrightarrow\operatorname{cod}({k})\subseteq C_{p}$

  4. (4)

The program starts in the application: $\Psi.pc=0$ and
$\Psi.C(0)=(\mathtt{app},\\_)$.

  5. (5)

$ctx^{\ast}$ and $ctx$ start initialized to the library stack:

$\displaystyle ctx^{\ast}\in H_{\mathtt{app}}$ $\displaystyle
ctx=\Psi.M(ctx^{\ast})\in H_{\mathtt{app}}$
$\displaystyle\Psi.M(ctx)=S_{\mathtt{lib}}[0]-1.$

  6. (6)

When calling into the library NaCl considers all registers except the stack
pointer and program counter confidential. It further labels sandbox memory and
the $n^{\prime}$ arguments in the application stack as public with the
remainder of application memory labeled as confidential.

$\displaystyle\mathbb{C}(\Psi)(r)$
$\displaystyle=\begin{cases}\mathtt{lib}&\text{when }r=sp\\\
\mathtt{lib}&\text{when }r=pc\\\ \mathtt{app}&\text{otherwise}\end{cases}$
$\displaystyle\mathbb{C}(\Psi)(n)$
$\displaystyle=\begin{cases}\mathtt{lib}&\text{when }n\in M_{\mathtt{lib}}\\\
\mathtt{lib}&\text{when }n\in(\Psi.sp-n^{\prime},\Psi.sp]\text{ where
}{\Psi}\llparenthesis{\mathtt{gatecall}_{\mathit{n^{\prime}}}\
{e}}\rrparenthesis_{\mathtt{app}}\\\ \mathtt{app}&\text{when }n\in
M_{\mathtt{app}}\wedge n\notin(\Psi.sp-n^{\prime},\Psi.sp]\text{ where
}{\Psi}\llparenthesis{\mathtt{gatecall}_{\mathit{n^{\prime}}}\
{e}}\rrparenthesis_{\mathtt{app}}\end{cases}$

###  B.2. Properties

Throughout the following we will use the shorthand
$ctx_{\Psi}\triangleq\Psi.M(ctx^{\ast})$.

###### Proposition 0.

NaCl has the disjoint noninterference property.

###### Proof.

Follows immediately from the fact that all reads and writes are guarded to be
within $M_{\mathtt{lib}}$, all values in $M_{\mathtt{lib}}$ have label
$\mathtt{lib}$, and all jumps remain within the library code. ∎

###### Lemma 0.

The trampoline context is in $H_{\mathtt{app}}$.

###### Lemma 0.

$ctx\geq ctx_{0}$.

###### Lemma 0.

If ${\Psi_{1}}\llparenthesis{c}\rrparenthesis_{\mathtt{lib}}$ and
$\Psi_{1}\mathrel{\xrightarrow{p}\mathrel{\vphantom{\to}{}^{\ast}}}\Psi_{2}$,
then $\Psi^{\prime\prime}.M_{\mathtt{app}}=\Psi^{\prime}.M_{\mathtt{app}}$.

###### Proof.

There are two cases for $p$: $p=\mathtt{app}$ and $p=\mathtt{lib}$. If
$p=\mathtt{app}$, then $\Psi_{2}=\Psi_{1}$ and therefore trivially
$\Psi_{2}.M_{\mathtt{app}}=\Psi_{1}.M_{\mathtt{app}}$. If $p=\mathtt{lib}$,
then for all $\Psi$ such that
$\Psi_{1}\mathrel{\mathrel{\rightarrow}^{\ast}}\Psi\mathrel{\mathrel{\rightarrow}^{+}}\Psi_{2}$,
$\Psi.C(\Psi.pc)=(\mathtt{lib},\\_)$. By the structure of a NaCl program, this
ensures that $\Psi_{2}.M_{\mathtt{app}}=\Psi_{1}.M_{\mathtt{app}}$. ∎

###### Lemma 0.

If
$\Psi\mathrel{\xrightarrow{p}\mathrel{\vphantom{\to}{}^{\ast}}}\Psi^{\prime}$
then $\Psi.p=\Psi^{\prime}.p$.

###### Lemma 0.

If $\Psi\mathrel{\xrightarrow{\\!\text{wb}}}\Psi^{\prime}$ where
$\Psi\mathrel{\mathrel{\rightarrow}^{\ast}}\Psi^{\prime\prime}\mathrel{\rightarrow}\Psi^{\prime}$,
then $\Psi^{\prime\prime}.p\neq\Psi.p$ and $\Psi^{\prime}.p=\Psi.p$.

###### Proof.

We proceed by simultaneous induction on the well-bracketed transition
$\Psi\mathrel{\xrightarrow{\\!\text{wb}}}\Psi^{\prime}$ and the length of
$\Psi_{0}\mathrel{\mathrel{\rightarrow}^{\ast}}\Psi\mathrel{\xrightarrow{\\!\text{wb}}}\Psi^{\prime}$.

  * Case

No callbacks

We have that ${\Psi}\llparenthesis{\mathtt{gatecall}_{n}\ {e}}\rrparenthesis$
and there exist $\Psi_{1}$, $\Psi_{2}$, and $p$ such that
$\Psi\mathrel{\rightarrow}\Psi_{1}\mathrel{\xrightarrow{p}\mathrel{\vphantom{\to}{}^{\ast}}}\Psi_{2}\mathrel{\rightarrow}\Psi^{\prime}$
where ${\Psi_{2}}\llparenthesis{\mathtt{gateret}}\rrparenthesis$. Here
$\Psi^{\prime\prime}=\Psi_{2}$. By inspection of the reduction for
$\mathtt{gatecall}_{n}\ {e}$ we know that $\Psi_{1}.p\neq\Psi.p$ and therefore
by Lemma 5 $\Psi^{\prime\prime}.p\neq\Psi.p$. By inspection of the reduction
for $\mathtt{gateret}$, $\Psi^{\prime}.p=\Psi.p$.

  * Case

Callbacks

We have that ${\Psi}\llparenthesis{\mathtt{gatecall}_{n}\ {e}}\rrparenthesis$
and there exist $\Psi_{1}$, $\Psi_{2}$ such that
$\Psi\mathrel{\rightarrow}\Psi_{1}\mathrel{\xrightarrow{\\!\square}\mathrel{\vphantom{\to}{}^{\ast}}}\Psi_{2}\mathrel{\rightarrow}\Psi^{\prime}$
where ${\Psi_{2}}\llparenthesis{\mathtt{gateret}}\rrparenthesis$. Here
$\Psi^{\prime\prime}=\Psi_{2}$. By inspection of the reduction for
$\mathtt{gatecall}_{n}\ {e}$ we know that $\Psi_{1}.p\neq\Psi.p$. We now show,
by induction on
$\Psi_{1}\mathrel{\xrightarrow{\\!\square}\mathrel{\vphantom{\to}{}^{\ast}}}\Psi_{2}$,
that $\Psi_{2}.p=\Psi_{1}.p\neq\Psi.p$.

###### Proof.

If there are no steps then clearly $\Psi_{2}.p=\Psi_{1}.p\neq\Psi.p$. There
are two possible cases for
$\Psi_{1}\mathrel{\xrightarrow{\\!\square}\mathrel{\vphantom{\to}{}^{\ast}}}\Psi_{3}\mathrel{\xrightarrow{\\!\square}}\Psi_{4}$.
When $\Psi_{3}\mathrel{\xrightarrow{p}}\Psi_{4}$, Lemma 5 gives us that
$\Psi_{4}.p=\Psi_{3}.p=\Psi_{1}.p\neq\Psi.p$. When
$\Psi_{3}\mathrel{\xrightarrow{\\!\text{wb}}}\Psi_{4}$, our outer inductive
hypothesis gives us that $\Psi_{4}.p=\Psi_{3}.p=\Psi_{1}.p\neq\Psi.p$. ∎

Lastly, by inspection of the reduction for $\mathtt{gateret}$,
$\Psi^{\prime}.p=\Psi.p$.

∎

###### Lemma 0.

If
$\Psi\mathrel{\xrightarrow{\\!\square}\mathrel{\vphantom{\to}{}^{\ast}}}\Psi^{\prime}$,
then $\Psi^{\prime}.p=\Psi.p$.

###### Proof.

By induction, Lemma 5, and Lemma 6. ∎

###### Lemma 0 (Context Integrity).

Let $\Psi_{0}\in\mathit{Program}$,
$\Psi_{0}\mathrel{\mathrel{\rightarrow}^{\ast}}\Psi$, and
$\Psi\mathrel{\xrightarrow{\\!\text{wb}}}\Psi^{\prime}$. Then

  1. (1)

if $\Psi.p=\mathtt{app}$, then
$\Psi.M([ctx_{\Psi_{0}},ctx_{\Psi}))=\Psi^{\prime}.M([ctx_{\Psi_{0}},ctx_{\Psi^{\prime}}))$
and $ctx_{\Psi}=ctx_{\Psi^{\prime}}$,

  2. (2)

if $\Psi.p=\mathtt{lib}$, then
$\Psi.M([ctx_{\Psi_{0}},ctx_{\Psi}])=\Psi^{\prime}.M([ctx_{\Psi_{0}},ctx_{\Psi^{\prime}}])$
and $ctx_{\Psi}=ctx_{\Psi^{\prime}}$.

###### Proof.

We proceed by mutual, simultaneous induction on the well-bracketed transition
$\Psi_{1}\mathrel{\xrightarrow{\\!\text{wb}}}\Psi_{2}$ and the length of
$\Psi_{0}\mathrel{\mathrel{\rightarrow}^{\ast}}\Psi\mathrel{\xrightarrow{\\!\text{wb}}}\Psi^{\prime}$.

First we consider the case where
${\Psi}\llparenthesis{c}\rrparenthesis_{\mathtt{app}}$.

  * Case

No callbacks

We have that ${\Psi}\llparenthesis{\mathtt{gatecall}_{n}\ {e}}\rrparenthesis$
and there exist $\Psi_{1}$, $\Psi_{2}$, and $p$ such that
$\Psi\mathrel{\rightarrow}\Psi_{1}\mathrel{\xrightarrow{p}\mathrel{\vphantom{\to}{}^{\ast}}}\Psi_{2}\mathrel{\rightarrow}\Psi^{\prime}$
where ${\Psi_{2}}\llparenthesis{\mathtt{gateret}}\rrparenthesis$. By Lemma 4
we have that $\Psi_{1}.M_{\mathtt{app}}=\Psi_{2}.M_{\mathtt{app}}$. By
assumption we have that ${\Psi}\llparenthesis{\mathtt{gatecall}_{n}\
{e}}\rrparenthesis_{\mathtt{app}}$ and therefore by Lemma 6 we have that
${\Psi_{2}}\llparenthesis{\mathtt{gateret}}\rrparenthesis_{\mathtt{lib}}$. By
Lemma 2, Lemma 3, and inspection of the reduction rules for
$\mathtt{gatecall}_{n}\ {e}$ and $\mathtt{gateret}$ we have that
$\Psi.M([ctx_{\Psi_{0}},ctx_{\Psi}))=\Psi^{\prime}.M([ctx_{\Psi_{0}},ctx_{\Psi^{\prime}}))$
and $ctx_{\Psi}=ctx_{\Psi^{\prime}}$.

  * Case

Callbacks

We have that ${\Psi}\llparenthesis{\mathtt{gatecall}_{n}\ {e}}\rrparenthesis$
and there exist $\Psi_{1}$, $\Psi_{2}$ such that
$\Psi\mathrel{\rightarrow}\Psi_{1}\mathrel{\xrightarrow{\\!\square}\mathrel{\vphantom{\to}{}^{\ast}}}\Psi_{2}\mathrel{\rightarrow}\Psi^{\prime}$
where ${\Psi_{2}}\llparenthesis{\mathtt{gateret}}\rrparenthesis$. By
inspection of the reduction rule for $\mathtt{gatecall}_{n}\ {e}$ we have that
$ctx_{\Psi_{1}}=ctx_{\Psi}+\operatorname{len}(\mathbb{CSR})$. We now show, by
induction on
$\Psi_{1}\mathrel{\xrightarrow{\\!\square}\mathrel{\vphantom{\to}{}^{\ast}}}\Psi_{2}$,
that $ctx_{\Psi_{2}}=ctx_{\Psi_{1}}$ and
$\Psi_{1}.M([ctx_{\Psi_{0}},ctx_{\Psi_{1}}])=\Psi_{2}.M([ctx_{\Psi_{0}},ctx_{\Psi_{2}}])$.

###### Proof.

If there are no steps then clearly $ctx_{\Psi_{2}}=ctx_{\Psi_{1}}$ and all of
$\Psi_{1}.M_{\mathtt{app}}=\Psi_{2}.M_{\mathtt{app}}$. There are two possible
cases for
$\Psi_{1}\mathrel{\xrightarrow{\\!\square}\mathrel{\vphantom{\to}{}^{\ast}}}\Psi_{3}\mathrel{\xrightarrow{\\!\square}}\Psi_{4}$,
and notice that in both $\Psi_{3}.p=\Psi_{1}.p=\mathtt{lib}$ (by Lemma 7).
When $\Psi_{3}\mathrel{\xrightarrow{p}}\Psi_{4}$, Lemma 4 gives us that
$\Psi_{3}.M_{\mathtt{app}}=\Psi_{4}.M_{\mathtt{app}}$ and then Lemma 2 gives
us that $ctx_{\Psi_{4}}=ctx_{\Psi_{3}}=ctx_{\Psi_{1}}$. When
$\Psi_{3}\mathrel{\xrightarrow{\\!\text{wb}}}\Psi_{4}$, case 2 of our
inductive hypothesis gives us that
$\Psi_{1}.M([ctx_{\Psi_{0}},ctx_{\Psi_{1}}])=\Psi_{3}.M([ctx_{\Psi_{0}},ctx_{\Psi_{3}}])=\Psi_{4}.M([ctx_{\Psi_{0}},ctx_{\Psi_{4}}])$
and $ctx_{\Psi_{4}}=ctx_{\Psi_{3}}=ctx_{\Psi_{1}}$. ∎

Finally, by Lemma 7 we get that $\Psi_{2}=\mathtt{lib}$ and then inspection of
the reduction rule for $\mathtt{gateret}$ gives us that
$\Psi.M([ctx_{\Psi_{0}},ctx_{\Psi}))=\Psi^{\prime}.M([ctx_{\Psi_{0}},ctx_{\Psi^{\prime}}))$
and $ctx_{\Psi}=ctx_{\Psi^{\prime}}$.

Second we consider the case where
${\Psi}\llparenthesis{c}\rrparenthesis_{\mathtt{lib}}$.

  * Case

No callbacks

We have that ${\Psi}\llparenthesis{\mathtt{gatecall}_{n}\ {e}}\rrparenthesis$
and there exist $\Psi_{1}$, $\Psi_{2}$, and $p$ such that
$\Psi\mathrel{\rightarrow}\Psi_{1}\mathrel{\xrightarrow{p}\mathrel{\vphantom{\to}{}^{\ast}}}\Psi_{2}\mathrel{\rightarrow}\Psi^{\prime}$
where ${\Psi_{2}}\llparenthesis{\mathtt{gateret}}\rrparenthesis$. By the
structure of a NaCl program we have that $ctx_{\Psi_{1}}=ctx_{\Psi_{2}}$ and
$\Psi_{1}.M([ctx_{\Psi_{0}},ctx_{\Psi_{1}}])=\Psi_{2}.M([ctx_{\Psi_{0}},ctx_{\Psi_{2}}])$.
By assumption we have that ${\Psi}\llparenthesis{\mathtt{gatecall}_{n}\
{e}}\rrparenthesis_{\mathtt{lib}}$ and therefore by Lemma 6 we have that
${\Psi_{2}}\llparenthesis{\mathtt{gateret}}\rrparenthesis_{\mathtt{app}}$. By
Lemma 3 and inspection of the reduction rules for $\mathtt{gatecall}_{n}\ {e}$
and $\mathtt{gateret}$ we have that
$\Psi.M([ctx_{\Psi_{0}},ctx_{\Psi}))=\Psi^{\prime}.M([ctx_{\Psi_{0}},ctx_{\Psi^{\prime}}))$
and $ctx_{\Psi}=ctx_{\Psi^{\prime}}$.

  * Case

Callbacks

We have that ${\Psi}\llparenthesis{\mathtt{gatecall}_{n}\ {e}}\rrparenthesis$
and there exist $\Psi_{1}$, $\Psi_{2}$ such that
$\Psi\mathrel{\rightarrow}\Psi_{1}\mathrel{\xrightarrow{\\!\square}\mathrel{\vphantom{\to}{}^{\ast}}}\Psi_{2}\mathrel{\rightarrow}\Psi^{\prime}$
where ${\Psi_{2}}\llparenthesis{\mathtt{gateret}}\rrparenthesis$. By
inspection of the reduction rule for $\mathtt{gatecall}_{n}\ {e}$ we have that
$ctx_{\Psi_{1}}=ctx_{\Psi}+1$. We now show, by induction on
$\Psi_{1}\mathrel{\xrightarrow{\\!\square}\mathrel{\vphantom{\to}{}^{\ast}}}\Psi_{2}$,
that $ctx_{\Psi_{2}}=ctx_{\Psi_{1}}$ and
$\Psi_{1}.M([ctx_{\Psi_{0}},ctx_{\Psi_{1}}))=\Psi_{2}.M([ctx_{\Psi_{0}},ctx_{\Psi_{2}}))$.

###### Proof.

If there are no steps then clearly $ctx_{\Psi_{2}}=ctx_{\Psi_{1}}$ and all of
$\Psi_{1}.M_{\mathtt{app}}=\Psi_{2}.M_{\mathtt{app}}$. There are two possible
cases for
$\Psi_{1}\mathrel{\xrightarrow{\\!\square}\mathrel{\vphantom{\to}{}^{\ast}}}\Psi_{3}\mathrel{\xrightarrow{\\!\square}}\Psi_{4}$,
and notice that in both $\Psi_{3}.p=\Psi_{1}.p=\mathtt{app}$ (by Lemma 7).
When $\Psi_{3}\mathrel{\xrightarrow{p}}\Psi_{4}$, the structure of a NaCl
program gives us that $ctx_{\Psi_{1}}=ctx_{\Psi_{2}}$ and
$\Psi_{1}.M([ctx_{\Psi_{0}},ctx_{\Psi_{1}}])=\Psi_{2}.M([ctx_{\Psi_{0}},ctx_{\Psi_{2}}])$.
When $\Psi_{3}\mathrel{\xrightarrow{\\!\text{wb}}}\Psi_{4}$, case 1 of our
inductive hypothesis gives us that
$\Psi_{1}.M([ctx_{\Psi_{0}},ctx_{\Psi_{1}}))=\Psi_{3}.M([ctx_{\Psi_{0}},ctx_{\Psi_{3}}))=\Psi_{4}.M([ctx_{\Psi_{0}},ctx_{\Psi_{4}}))$
and $ctx_{\Psi_{4}}=ctx_{\Psi_{3}}=ctx_{\Psi_{1}}$. ∎

Finally, by Lemma 7 we get that $\Psi_{2}=\mathtt{app}$ and then inspection of
the reduction rule for $\mathtt{gateret}$ gives us that
$\Psi.M([ctx_{\Psi_{0}},ctx_{\Psi}])=\Psi^{\prime}.M([ctx_{\Psi_{0}},ctx_{\Psi^{\prime}}])$
and $ctx_{\Psi}=ctx_{\Psi^{\prime}}$.

∎

###### Proposition 0.

NaCl has callee-save register integrity.

###### Proof.

Follows from Lemma 8, Lemma 6, and inspection of the reduction rules for
$\mathtt{gatecall}_{n}\ {e}$ and $\mathtt{gateret}$. ∎

###### Lemma 0.

Let $\Psi_{0}\in\mathit{Program}$,
$\pi=\Psi_{0}\mathrel{\mathrel{\rightarrow}^{\ast}}\Psi$, and
$\Psi\mathrel{\xrightarrow{\\!\text{wb}}}\Psi^{\prime}$, then
$\Psi^{\prime}.M(\operatorname{return-
address}_{\mathtt{app}}(\pi))=\Psi.M(\operatorname{return-
address}_{\mathtt{app}}(\pi))$.

###### Proof.

First we consider the case where
${\Psi}\llparenthesis{c}\rrparenthesis_{\mathtt{app}}$.

  * Case

No callbacks

We have that ${\Psi}\llparenthesis{\mathtt{gatecall}_{n}\ {e}}\rrparenthesis$
and there exist $\Psi_{1}$, $\Psi_{2}$, and $p$ such that
$\Psi\mathrel{\rightarrow}\Psi_{1}\mathrel{\xrightarrow{p}\mathrel{\vphantom{\to}{}^{\ast}}}\Psi_{2}\mathrel{\rightarrow}\Psi^{\prime}$
where ${\Psi_{2}}\llparenthesis{\mathtt{gateret}}\rrparenthesis$. By
inspection of the reduction rule for $\mathtt{gatecall}_{n}\ {e}$ we see that
$\Psi_{1}.M(\Psi.sp+1)=\Psi.pc+1$. This is adding to the top of the stack, so
by the structure of a NaCl program we have that
$\Psi_{1}.M(\operatorname{return-
address}_{\mathtt{app}}(\pi))=\Psi.M(\operatorname{return-
address}_{\mathtt{app}}(\pi))$. By Lemma 4 we have that
$\Psi_{1}.M_{\mathtt{app}}=\Psi_{2}.M_{\mathtt{app}}$ and therefore Lemma 2
gives us that $ctx_{\Psi_{2}}=ctx_{\Psi_{1}}$ and
$\Psi_{2}.M(\operatorname{return-
address}_{\mathtt{app}}(\pi))=\Psi_{1}.M(\operatorname{return-
address}_{\mathtt{app}}(\pi))$. If we inspect the trampoline code we see that,
right before we execute the $\mathtt{ret}$, we have set $sp$ to
$\Psi_{2}.M(ctx_{\Psi_{2}})=\Psi_{1}.M(ctx_{\Psi_{1}})=\Psi.sp+1$. Thus, after
returning the only part of the application stack that we modify is
$\Psi.sp+1$. This, and the fact that $\Psi_{2}.M(\operatorname{return-
address}_{\mathtt{app}}(\pi))=\Psi.M(\operatorname{return-
address}_{\mathtt{app}}(\pi))$ gives us that $\Psi.M(\operatorname{return-
address}_{\mathtt{app}}(\pi))=\Psi^{\prime}.M(\operatorname{return-
address}_{\mathtt{app}}(\pi))$.

  * Case

Callbacks

We have that ${\Psi}\llparenthesis{\mathtt{gatecall}_{n}\ {e}}\rrparenthesis$
and there exist $\Psi_{1}$, $\Psi_{2}$ such that
$\Psi\mathrel{\rightarrow}\Psi_{1}\mathrel{\xrightarrow{\\!\square}\mathrel{\vphantom{\to}{}^{\ast}}}\Psi_{2}\mathrel{\rightarrow}\Psi^{\prime}$
where ${\Psi_{2}}\llparenthesis{\mathtt{gateret}}\rrparenthesis$. By
inspection of the reduction rule for $\mathtt{gatecall}_{n}\ {e}$ we see that
$\Psi_{1}.M(\Psi.sp+1)=\Psi.pc+1$. This is adding to the top of the stack, so
by the structure of a NaCl program we have that
$\Psi_{1}.M(\operatorname{return-
address}_{\mathtt{app}}(\pi))=\Psi.M(\operatorname{return-
address}_{\mathtt{app}}(\pi))$. We now show, by induction on
$\Psi_{1}\mathrel{\xrightarrow{\\!\square}\mathrel{\vphantom{\to}{}^{\ast}}}\Psi_{2}$
that $\Psi_{2}.M(ctx_{\Psi_{2}})=\Psi.sp+1$ and
$\Psi_{2}.M(\operatorname{return-
address}_{\mathtt{app}}(\pi))=\Psi_{1}.M(\operatorname{return-
address}_{\mathtt{app}}(\pi))$.

###### Proof.

If there are no steps then $\Psi_{2}=\Psi_{1}$ and both goals hold
immediately. There are two possible cases for
$\Psi_{1}\mathrel{\xrightarrow{\\!\square}\mathrel{\vphantom{\to}{}^{\ast}}}\Psi_{3}\mathrel{\xrightarrow{\\!\square}}\Psi_{4}$
and notice that in both $\Psi_{3}.p=\Psi_{1}.p=\mathtt{lib}$ (by Lemma 7). If
$\Psi_{3}\mathrel{\xrightarrow{p}}\Psi_{4}$ then Lemma 4 gives us that
$\Psi_{4}.M_{\mathtt{app}}=\Psi_{3}.M_{\mathtt{app}}$ and our goal holds (as
all of $\operatorname{return-address}_{\mathtt{app}}(\pi)$ is in
$S_{\mathtt{app}}$). If
$\Psi_{3}\mathrel{\xrightarrow{\\!\text{wb}}}\Psi_{4}$, then Lemma 8 gives us
that $ctx_{\Psi_{3}}=ctx_{\Psi_{4}}$ and
$\Psi_{3}.M([ctx_{\Psi_{0}},ctx_{\Psi_{3}}])=\Psi_{4}.M([ctx_{\Psi_{0}},ctx_{\Psi_{4}}])$
and therefore that $\Psi_{4}.M(ctx_{\Psi_{4}})=\Psi.sp+1$.
$\operatorname{return-
address}_{\mathtt{app}}(\Psi_{0}\mathrel{\mathrel{\rightarrow}^{\ast}}\Psi_{3})=\operatorname{return-
address}_{\mathtt{app}}(\pi)\uplus\Psi.sp+1$, so our inductive hypothesis
gives us that $\Psi_{4}.M(\operatorname{return-
address}_{\mathtt{app}}(\pi))=\Psi_{3}.M(\operatorname{return-
address}_{\mathtt{app}}(\pi))$. ∎

Second we consider the case where
${\Psi}\llparenthesis{c}\rrparenthesis_{\mathtt{lib}}$.

  * Case

No callbacks

We have that ${\Psi}\llparenthesis{\mathtt{gatecall}_{n}\ {e}}\rrparenthesis$
and there exist $\Psi_{1}$, $\Psi_{2}$, and $p$ such that
$\Psi\mathrel{\rightarrow}\Psi_{1}\mathrel{\xrightarrow{p}\mathrel{\vphantom{\to}{}^{\ast}}}\Psi_{2}\mathrel{\rightarrow}\Psi^{\prime}$
where ${\Psi_{2}}\llparenthesis{\mathtt{gateret}}\rrparenthesis$. By
inspection of the reduction rule for $\mathtt{gatecall}_{n}\ {e}$ we see that
$\Psi_{1}.M(\operatorname{return-
address}_{\mathtt{app}}(\pi))=\Psi.M(\operatorname{return-
address}_{\mathtt{app}}(\pi))$. By the structure of a NaCl program we have
that any call stack elements that are added during the callback will be popped
before the $\mathtt{gateret}$. Thus, $\Psi_{2}.M(\operatorname{return-
address}_{\mathtt{app}}(\pi))=\Psi_{1}.M(\operatorname{return-
address}_{\mathtt{app}}(\pi))$. Inspection of the reduction rule for
$\mathtt{gateret}$ then gives us that $\Psi^{\prime}.M(\operatorname{return-
address}_{\mathtt{app}}(\pi))=\Psi_{2}.M(\operatorname{return-
address}_{\mathtt{app}}(\pi))=\Psi.M(\operatorname{return-
address}_{\mathtt{app}}(\pi))$.

  * Case

Callbacks

We have that ${\Psi}\llparenthesis{\mathtt{gatecall}_{n}\ {e}}\rrparenthesis$
and there exist $\Psi_{1}$, $\Psi_{2}$ such that
$\Psi\mathrel{\rightarrow}\Psi_{1}\mathrel{\xrightarrow{\\!\square}\mathrel{\vphantom{\to}{}^{\ast}}}\Psi_{2}\mathrel{\rightarrow}\Psi^{\prime}$
where ${\Psi_{2}}\llparenthesis{\mathtt{gateret}}\rrparenthesis$. By
inspection of the reduction rule for $\mathtt{gatecall}_{n}\ {e}$ we see that
$\Psi_{1}.M(\operatorname{return-
address}_{\mathtt{app}}(\pi))=\Psi.M(\operatorname{return-
address}_{\mathtt{app}}(\pi))$. We now show, by induction on
$\Psi_{1}\mathrel{\xrightarrow{\\!\square}\mathrel{\vphantom{\to}{}^{\ast}}}\Psi_{2}$
that $\Psi_{2}.M(\operatorname{return-
address}_{\mathtt{app}}(\pi))=\Psi_{1}.M(\operatorname{return-
address}_{\mathtt{app}}(\pi))$.

###### Proof.

If there are no steps then $\Psi_{2}=\Psi_{1}$ and the goal holds immediately.
There are two possible cases for
$\Psi_{1}\mathrel{\xrightarrow{\\!\square}\mathrel{\vphantom{\to}{}^{\ast}}}\Psi_{3}\mathrel{\xrightarrow{\\!\square}}\Psi_{4}$
and notice that in both $\Psi_{3}.p=\Psi_{1}.p=\mathtt{app}$ (by Lemma 7). If
$\Psi_{3}\mathrel{\xrightarrow{p}}\Psi_{4}$ then the structure of a NaCl
program gives us that any call stack elements that are added during the
callback will be popped before the $\mathtt{gateret}$, and therefore our
inductive invariant is maintained. If
$\Psi_{3}\mathrel{\xrightarrow{\\!\text{wb}}}\Psi_{4}$, then notice that
$\operatorname{return-
address}_{\mathtt{app}}(\Psi_{0}\mathrel{\mathrel{\rightarrow}^{\ast}}\Psi_{3})=\operatorname{return-
address}_{\mathtt{app}}(\pi)$, so our inductive hypothesis gives us that
$\Psi_{4}.M(\operatorname{return-
address}_{\mathtt{app}}(\pi))=\Psi_{3}.M(\operatorname{return-
address}_{\mathtt{app}}(\pi))$. ∎

Inspection of the reduction rule for $\mathtt{gateret}$ then gives us that
$\Psi^{\prime}.M(\operatorname{return-
address}_{\mathtt{app}}(\pi))=\Psi_{2}.M(\operatorname{return-
address}_{\mathtt{app}}(\pi))=\Psi.M(\operatorname{return-
address}_{\mathtt{app}}(\pi))$.

∎

###### Proposition 0.

NaCl has return address integrity.

###### Proof.

We have that $\Psi_{0}\in\mathit{Program}$,
$\pi=\Psi_{0}\mathrel{\mathrel{\rightarrow}^{\ast}}\Psi$,
$\Psi.p=\mathtt{app}$, and
$\Psi\mathrel{\xrightarrow{\\!\text{wb}}}\Psi^{\prime}$ and wish to show that
$\Psi.M(\operatorname{return-
address}_{\mathtt{app}}(\pi))=\Psi^{\prime}.M(\operatorname{return-
address}_{\mathtt{app}}(\pi))$, $\Psi^{\prime}.sp=\Psi.sp$, and
$\Psi^{\prime}.pc=\Psi.pc+1$.

Lemma 10 gives us that $\Psi.M(\operatorname{return-
address}_{\mathtt{app}}(\pi))=\Psi^{\prime}.M(\operatorname{return-
address}_{\mathtt{app}}(\pi))$. We proceed by simultaneous induction on the
well-bracketed transition
$\Psi\mathrel{\xrightarrow{\\!\text{wb}}}\Psi^{\prime}$ and the length of
$\Psi_{0}\mathrel{\mathrel{\rightarrow}^{\ast}}\Psi\mathrel{\xrightarrow{\\!\text{wb}}}\Psi^{\prime}$
to show that $\Psi^{\prime}.sp=\Psi.sp$, and $\Psi^{\prime}.pc=\Psi.pc+1$.

  * Case

No callbacks

We have that ${\Psi}\llparenthesis{\mathtt{gatecall}_{n}\ {e}}\rrparenthesis$
and there exist $\Psi_{1}$, $\Psi_{2}$, and $p$ such that
$\Psi\mathrel{\rightarrow}\Psi_{1}\mathrel{\xrightarrow{p}\mathrel{\vphantom{\to}{}^{\ast}}}\Psi_{2}\mathrel{\rightarrow}\Psi^{\prime}$
where ${\Psi_{2}}\llparenthesis{\mathtt{gateret}}\rrparenthesis$. By
inspection of the reduction rule for $\mathtt{gatecall}_{n}\ {e}$ we see that
$\Psi_{1}.M(\Psi.sp+1)=\Psi.pc+1$ and $\Psi_{1}.M(ctx_{\Psi_{1}})=\Psi.sp+1$.
By Lemma 4 we have that $\Psi_{1}.M_{\mathtt{app}}=\Psi_{2}.M_{\mathtt{app}}$
and therefore Lemma 2 gives us that $ctx_{\Psi_{2}}=ctx_{\Psi_{1}}$. If we
inspect the trampoline code we see that, right before we execute the
$\mathtt{ret}$, we have set $sp$ to
$\Psi_{2}.M(ctx_{\Psi_{2}})=\Psi_{1}.M(ctx_{\Psi_{1}})=\Psi.sp+1$. Thus, after
returning we have that $\Psi^{\prime}.pc=\Psi.pc+1$,
$\Psi^{\prime}.sp=\Psi.sp$.

  * Case

Callbacks

We have that ${\Psi}\llparenthesis{\mathtt{gatecall}_{n}\ {e}}\rrparenthesis$
and there exist $\Psi_{1}$, $\Psi_{2}$ such that
$\Psi\mathrel{\rightarrow}\Psi_{1}\mathrel{\xrightarrow{\\!\square}\mathrel{\vphantom{\to}{}^{\ast}}}\Psi_{2}\mathrel{\rightarrow}\Psi^{\prime}$
where ${\Psi_{2}}\llparenthesis{\mathtt{gateret}}\rrparenthesis$. By
inspection of the reduction rule for $\mathtt{gatecall}_{n}\ {e}$ we see that
$\Psi_{1}.M(\Psi.sp+1)=\Psi.pc+1$ and $\Psi_{1}.M(ctx_{\Psi_{1}})=\Psi.sp+1$.
We now show, by induction on
$\Psi_{1}\mathrel{\xrightarrow{\\!\square}\mathrel{\vphantom{\to}{}^{\ast}}}\Psi_{2}$
that $\Psi_{2}.M(\Psi.sp+1)=\Psi.pc+1$ and
$\Psi_{2}.M(ctx_{\Psi_{2}})=\Psi.sp+1$.

###### Proof.

If there are no steps then $\Psi_{2}=\Psi_{1}$ and both hold immediately.
There are two possible cases for
$\Psi_{1}\mathrel{\xrightarrow{\\!\square}\mathrel{\vphantom{\to}{}^{\ast}}}\Psi_{3}\mathrel{\xrightarrow{\\!\square}}\Psi_{4}$
and notice that in both $\Psi_{3}.p=\Psi_{1}.p=\mathtt{lib}$ (by Lemma 7). If
$\Psi_{3}\mathrel{\xrightarrow{p}}\Psi_{4}$ then Lemma 4 gives us that
$\Psi_{4}.M_{\mathtt{app}}=\Psi_{3}.M_{\mathtt{app}}$ and both hold (as the
invariants are on $M_{\mathtt{app}}$). If
$\Psi_{3}\mathrel{\xrightarrow{\\!\text{wb}}}\Psi_{4}$, then Lemma 8 gives us
that $ctx_{\Psi_{3}}=ctx_{\Psi_{4}}$ and
$\Psi_{3}.M([ctx_{\Psi_{0}},ctx_{\Psi_{3}}])=\Psi_{4}.M([ctx_{\Psi_{0}},ctx_{\Psi_{4}}])$
and therefore that $\Psi_{4}.M(ctx_{\Psi_{4}})=\Psi.sp+1$.
$\operatorname{return-
address}_{\mathtt{app}}(\Psi_{0}\mathrel{\mathrel{\rightarrow}^{\ast}}\Psi_{3})=\operatorname{return-
address}_{\mathtt{app}}(\pi)\uplus\Psi.sp+1$ so Lemma 10 gives us that
$\Psi_{4}.M(\Psi.sp+1)=\Psi_{3}.M(\Psi.sp+1)=\Psi.pc+1$. ∎

Finally, if we inspect the trampoline code we see that, right before we
execute the $\mathtt{ret}$, we have set $sp$ to
$\Psi_{2}.M(ctx_{\Psi_{2}})=\Psi.sp+1$. Thus, after returning we have that
$\Psi^{\prime}.pc=\Psi.pc+1$, $\Psi^{\prime}.sp=\Psi.sp$.

∎

##  Appendix C Overlay Semantics

Figure 21, Figure 22, and Figure 23 define the overlay monitor operational
semantics. The semantics are parameterized by a confidentiality policy
$\mathbb{C}$.

$\mathit{Val}$ | $\ni$ | ${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{v}}$ | $\mathrel{\vcentcolon\vcentcolon=}$ | ${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\langle}}{n},{p}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\rangle}}$
---|---|---|---|---
$\mathit{Frame}$ | $\ni$ | ${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathit{SF}}}$ | $\mathrel{\vcentcolon\vcentcolon=}$ | $\begin{array}[t]{lllll}\\{&\mathit{base}&\mathrel{\vcentcolon}&\mathbb{N}\\\ &\mathit{ret\mbox{-}addr\mbox{-}loc}&\mathrel{\vcentcolon}&\mathbb{N}\\\ &\mathit{csr\mbox{-}vals}&\mathrel{\vcentcolon}&\wp({\mathit{Reg}\times\mathbb{N}})&\\}\end{array}$
$\mathit{Function}$ | $\ni$ | ${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{F}}$ | $\mathrel{\vcentcolon\vcentcolon=}$ | $\begin{array}[t]{lllll}\\{&\mathit{instrs}&\mathrel{\vcentcolon}&\mathbb{N}\rightharpoonup\mathit{Command}\\\ &\mathit{entry}&\mathrel{\vcentcolon}&\mathbb{N}\\\ &\mathit{type}&\mathrel{\vcentcolon}&\mathbb{N}&\\}\end{array}$
$\mathit{oState}$ | $\ni$ | ${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}$ | $\mathrel{\vcentcolon\vcentcolon=}$ | ${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathtt{oerror}}}$
|  |  | $\mid$ | $\begin{array}[t]{lllll}\\{&\Psi&\mathrel{\vcentcolon}&\mathit{State}\\\ &\mathit{funcs}&\mathrel{\vcentcolon}&\mathbb{N}\rightharpoonup\mathit{Function}\\\ &\mathit{stack}&\mathrel{\vcentcolon}&[\mathit{Frame}]&\\}\end{array}$

Figure 20. Overlay Extended Syntax

${\Psi}\llparenthesis{c}\rrparenthesis\mathrel{\leadsto}\Psi^{\prime}$

$\displaystyle\displaystyle{\hbox{\hskip
230.26208pt\vbox{\hbox{\hskip-230.26207pt\hbox{\hbox{$\displaystyle\displaystyle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\langle}}{n},{p_{e}}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\rangle}}={\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathcal{V}}}_{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}}({e})$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle n^{\prime}=k(n)$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle
sp^{\prime}={\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}.sp+1$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle
M^{\prime}={\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}.M[sp^{\prime}\mapsto{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}.pc+1]$}\hskip
20.00003pt\hbox{\hskip-131.89838pt\hbox{\hbox{$\displaystyle\displaystyle\operatorname{typechecks}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}},n^{\prime},sp^{\prime})$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathit{SF}}}=\operatorname{new-
frame}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}},n^{\prime},sp^{\prime})$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle
p_{e}\sqsubseteq\mathtt{lib}$}}}}}}}}}}\vbox{\hbox{\hskip-131.89838pt\hbox{\hbox{$\displaystyle\displaystyle\operatorname{typechecks}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}},n^{\prime},sp^{\prime})$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathit{SF}}}=\operatorname{new-
frame}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}},n^{\prime},sp^{\prime})$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle
p_{e}\sqsubseteq\mathtt{lib}$}}}}}\vbox{}}}}\over\hbox{\hskip
141.63899pt\vbox{\vbox{}\hbox{\hskip-141.63898pt\hbox{\hbox{$\displaystyle\displaystyle{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}}\llparenthesis{\mathtt{call}_{{k}}\
{e}}\rrparenthesis_{\mathtt{lib}}\mathrel{\leadsto}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}[\mathit{stack}\mathbin{\vcentcolon=}[{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathit{SF}}}]\mathbin{{+}\mspace{-8.0mu}{+}}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}.\mathit{stack},pc\mathbin{\vcentcolon=}n^{\prime},sp\mathbin{\vcentcolon=}sp^{\prime},M\mathbin{\vcentcolon=}M^{\prime}]$}}}}}}$
$\displaystyle\displaystyle{\hbox{\hskip
176.06148pt\vbox{\hbox{\hskip-176.06146pt\hbox{\hbox{$\displaystyle\displaystyle\operatorname{is-
ret-addr-
loc}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}},{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}.sp)$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\langle}}{n}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\rangle}}={\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}.M({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}.sp)$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle n^{\prime}=k(n)$}\hskip
20.00003pt\hbox{\hskip-80.88124pt\hbox{\hbox{$\displaystyle\displaystyle\operatorname{csr-
restored}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}})$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi^{\prime}}}=\operatorname{pop-
frame}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}})$}}}}}}}}\vbox{\hbox{\hskip-80.88124pt\hbox{\hbox{$\displaystyle\displaystyle\operatorname{csr-
restored}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}})$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi^{\prime}}}=\operatorname{pop-
frame}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}})$}}}}\vbox{}}}}\over\hbox{\hskip
77.22125pt\vbox{\vbox{}\hbox{\hskip-77.22125pt\hbox{\hbox{$\displaystyle\displaystyle{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}}\llparenthesis{\mathtt{ret}_{{k}}}\rrparenthesis_{\mathtt{lib}}\mathrel{\leadsto}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi^{\prime}}}[pc\mathbin{\vcentcolon=}n^{\prime},sp\mathbin{\vcentcolon=}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}.sp-1]$}}}}}}$
$\displaystyle\displaystyle{\hbox{\hskip
223.37732pt\vbox{\hbox{\hskip-223.37732pt\hbox{\hbox{$\displaystyle\displaystyle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\langle}}{n^{\prime}}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\rangle}}={\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathcal{V}}}_{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}}({e})$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle
sp^{\prime}={\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}.sp+1$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle
M^{\prime}={\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}.M[sp^{\prime}\mapsto{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}.pc+1]$}\hskip
20.00003pt\hbox{\hskip-184.40428pt\hbox{\hbox{$\displaystyle\displaystyle
n^{\prime}\in I$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\operatorname{typechecks}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}},n^{\prime},sp^{\prime})$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\operatorname{args-
secure}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}},sp^{\prime},n)$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathit{SF}}}=\operatorname{new-
frame}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}},n^{\prime},sp^{\prime})$}}}}}}}}}}\vbox{\hbox{\hskip-184.40428pt\hbox{\hbox{$\displaystyle\displaystyle
n^{\prime}\in I$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\operatorname{typechecks}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}},n^{\prime},sp^{\prime})$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\operatorname{args-
secure}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}},sp^{\prime},n)$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathit{SF}}}=\operatorname{new-
frame}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}},n^{\prime},sp^{\prime})$}}}}}}\vbox{}}}}\over\hbox{\hskip
150.9405pt\vbox{\vbox{}\hbox{\hskip-150.94049pt\hbox{\hbox{$\displaystyle\displaystyle{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}}\llparenthesis{\mathtt{gatecall}_{n}\
{e}}\rrparenthesis_{\mathtt{lib}}\mathrel{\leadsto}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}[\mathit{stack}\mathbin{\vcentcolon=}[{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathit{SF}}}]\mathbin{{+}\mspace{-8.0mu}{+}}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}.\mathit{stack},pc\mathbin{\vcentcolon=}n^{\prime},sp\mathbin{\vcentcolon=}sp^{\prime},M\mathbin{\vcentcolon=}M^{\prime}]$}}}}}}$
$\displaystyle\displaystyle{\hbox{\hskip
174.50034pt\vbox{\hbox{\hskip-174.50032pt\hbox{\hbox{$\displaystyle\displaystyle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi^{\prime}}}=\operatorname{classify}_{\mathbb{C}}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}})$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\langle}}{n^{\prime}}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\rangle}}={\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathcal{V}}}_{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi^{\prime}}}}({e})$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle
sp^{\prime}={\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi^{\prime}}}.sp+1$}\hskip
20.00003pt\hbox{\hskip-115.05322pt\hbox{\hbox{$\displaystyle\displaystyle
M^{\prime}={\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi^{\prime}}}.M[sp^{\prime}\mapsto{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi^{\prime}}}.pc+1]$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathit{SF}}}=\operatorname{new-
frame}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi^{\prime}}},n^{\prime},sp^{\prime})$}}}}}}}}\vbox{\hbox{\hskip-115.05322pt\hbox{\hbox{$\displaystyle\displaystyle
M^{\prime}={\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi^{\prime}}}.M[sp^{\prime}\mapsto{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi^{\prime}}}.pc+1]$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathit{SF}}}=\operatorname{new-
frame}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi^{\prime}}},n^{\prime},sp^{\prime})$}}}}\vbox{}}}}\over\hbox{\hskip
153.88051pt\vbox{\vbox{}\hbox{\hskip-153.8805pt\hbox{\hbox{$\displaystyle\displaystyle{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}}\llparenthesis{\mathtt{gatecall}_{n}\
{e}}\rrparenthesis_{\mathtt{app}}\mathrel{\leadsto}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi^{\prime}}}[\mathit{stack}\mathbin{\vcentcolon=}[{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathit{SF}}}]\mathbin{{+}\mspace{-8.0mu}{+}}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi^{\prime}}}.\mathit{stack},pc\mathbin{\vcentcolon=}n^{\prime},sp\mathbin{\vcentcolon=}sp^{\prime},M\mathbin{\vcentcolon=}M^{\prime}]$}}}}}}$
$\displaystyle\displaystyle{\hbox{\hskip
75.22696pt\vbox{\hbox{\hskip-75.22696pt\hbox{\hbox{$\displaystyle\displaystyle{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}}\llparenthesis{\mathtt{ret}}\rrparenthesis\mathrel{\leadsto}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi^{\prime}}}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle p^{\prime}\sqsubseteq
p$}\hskip
20.00003pt\hbox{\hskip-35.06136pt\hbox{\hbox{$\displaystyle\displaystyle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\langle}}{n},{p^{\prime}}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\rangle}}={\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}.R(r_{ret})$}}}}}}\vbox{\hbox{\hskip-35.06136pt\hbox{\hbox{$\displaystyle\displaystyle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\langle}}{n},{p^{\prime}}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\rangle}}={\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}.R(r_{ret})$}}}\vbox{}}}}\over\hbox{\hskip
37.19269pt\vbox{\vbox{}\hbox{\hskip-37.19267pt\hbox{\hbox{$\displaystyle\displaystyle{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}}\llparenthesis{\mathtt{gateret}}\rrparenthesis_{p}\mathrel{\leadsto}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi^{\prime}}}$}}}}}}$
$\displaystyle\displaystyle{\hbox{\hskip
131.24753pt\vbox{\hbox{\hskip-131.24753pt\hbox{\hbox{$\displaystyle\displaystyle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{v}}={\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathcal{V}}}_{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}}({e})$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle
sp^{\prime}={\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}.sp+1$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle sp^{\prime}\in S_{p}$}\hskip
20.00003pt\hbox{\hskip-77.65958pt\hbox{\hbox{$\displaystyle\displaystyle
M^{\prime}={\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}.M[sp^{\prime}\mapsto{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{v}}]$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\operatorname{writeable}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}},sp^{\prime})$}}}}}}}}\vbox{\hbox{\hskip-77.65958pt\hbox{\hbox{$\displaystyle\displaystyle
M^{\prime}={\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}.M[sp^{\prime}\mapsto{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{v}}]$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\operatorname{writeable}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}},sp^{\prime})$}}}}\vbox{}}}}\over\hbox{\hskip
78.22626pt\vbox{\vbox{}\hbox{\hskip-78.22624pt\hbox{\hbox{$\displaystyle\displaystyle{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}}\llparenthesis{\mathtt{push}_{p}\
{e}}\rrparenthesis\mathrel{\leadsto}{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}}^{++}[sp\mathbin{\vcentcolon=}sp^{\prime},M\mathbin{\vcentcolon=}M^{\prime}]$}}}}}}$
$\displaystyle\displaystyle{\hbox{\hskip
149.02917pt\vbox{\hbox{\hskip-149.02917pt\hbox{\hbox{$\displaystyle\displaystyle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\langle}}{n},{p_{e}}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\rangle}}={\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathcal{V}}}_{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}}({e})$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{v}}={\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\langle}}{\\_},{p_{e^{\prime}}}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\rangle}}={\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathcal{V}}}_{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}}({e^{\prime}})$}\hskip
20.00003pt\hbox{\hskip-129.25078pt\hbox{\hbox{$\displaystyle\displaystyle
M^{\prime}={\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}.M[n^{\prime}\mapsto{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{v}}]$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\operatorname{writeable}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}},n^{\prime})$}\hskip
20.00003pt\hbox{\hskip-90.61516pt\hbox{\hbox{$\displaystyle\displaystyle
n^{\prime}=k(n)$}\hskip 20.00003pt\hbox{\hbox{$\displaystyle\displaystyle
p_{e}\sqsubseteq p$}\hskip 20.00003pt\hbox{\hbox{$\displaystyle\displaystyle
p_{e^{\prime}}\not\sqsubseteq p\Longrightarrow n^{\prime}\notin
H_{\mathtt{lib}}$}}}}}}}}}}}\vbox{\hbox{\hskip-129.25078pt\hbox{\hbox{$\displaystyle\displaystyle
M^{\prime}={\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}.M[n^{\prime}\mapsto{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{v}}]$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\operatorname{writeable}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}},n^{\prime})$}\hskip
20.00003pt\hbox{\hskip-90.61516pt\hbox{\hbox{$\displaystyle\displaystyle
n^{\prime}=k(n)$}\hskip 20.00003pt\hbox{\hbox{$\displaystyle\displaystyle
p_{e}\sqsubseteq p$}\hskip 20.00003pt\hbox{\hbox{$\displaystyle\displaystyle
p_{e^{\prime}}\not\sqsubseteq p\Longrightarrow n^{\prime}\notin
H_{\mathtt{lib}}$}}}}}}}}\vbox{\hbox{\hskip-90.61516pt\hbox{\hbox{$\displaystyle\displaystyle
n^{\prime}=k(n)$}\hskip 20.00003pt\hbox{\hbox{$\displaystyle\displaystyle
p_{e}\sqsubseteq p$}\hskip 20.00003pt\hbox{\hbox{$\displaystyle\displaystyle
p_{e^{\prime}}\not\sqsubseteq p\Longrightarrow n^{\prime}\notin
H_{\mathtt{lib}}$}}}}}\vbox{}}}}}\over\hbox{\hskip
70.45091pt\vbox{\vbox{}\hbox{\hskip-70.45091pt\hbox{\hbox{$\displaystyle\displaystyle{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}}\llparenthesis{\mathtt{store}_{k}\
{e}\mathbin{\vcentcolon=}{e^{\prime}}}\rrparenthesis_{p}\mathrel{\leadsto}{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}}^{++}[M\mathbin{\vcentcolon=}M^{\prime}]$}}}}}}$
$\displaystyle\displaystyle{\hbox{\hskip
128.41916pt\vbox{\hbox{\hskip-128.41916pt\hbox{\hbox{$\displaystyle\displaystyle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\langle}}{n},{p_{e}}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\rangle}}={\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathcal{V}}}_{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}}({e})$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle n^{\prime}=k(n)$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle p_{e}\sqsubseteq p$}\hskip
20.00003pt\hbox{\hskip-80.26082pt\hbox{\hbox{$\displaystyle\displaystyle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{v}}={\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\langle}}{\\_},{p_{n^{\prime}}}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\rangle}}={\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}.M(n^{\prime})$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle
R^{\prime}={\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}.R[r\mapsto{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{v}}]$}}}}}}}}\vbox{\hbox{\hskip-80.26082pt\hbox{\hbox{$\displaystyle\displaystyle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{v}}={\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\langle}}{\\_},{p_{n^{\prime}}}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\rangle}}={\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}.M(n^{\prime})$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle
R^{\prime}={\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}.R[r\mapsto{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{v}}]$}}}}\vbox{}}}}\over\hbox{\hskip
66.30649pt\vbox{\vbox{}\hbox{\hskip-66.30649pt\hbox{\hbox{$\displaystyle\displaystyle{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}}\llparenthesis{{r}\leftarrow\mathtt{load}_{k}\
{e}}\rrparenthesis_{p}\mathrel{\leadsto}{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}}^{++}[R\mathbin{\vcentcolon=}R^{\prime}]$}}}}}}$
$\displaystyle\displaystyle{\hbox{\hskip
49.19113pt\vbox{\hbox{\hskip-49.19112pt\hbox{\hbox{$\displaystyle\displaystyle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\langle}}{v},{p_{e}}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\rangle}}={\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathcal{V}}}_{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}}({e})$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle p_{e}\sqsubseteq
p$}}}}\vbox{}}}\over\hbox{\hskip
66.24759pt\vbox{\vbox{}\hbox{\hskip-66.24757pt\hbox{\hbox{$\displaystyle\displaystyle{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}}\llparenthesis{{sp}\leftarrow\mathtt{mov}\
{e}}\rrparenthesis_{p}\mathrel{\leadsto}{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}}^{++}[sp\mathbin{\vcentcolon=}v]$}}}}}}$
$\displaystyle\displaystyle{\hbox{\hskip
104.01323pt\vbox{\hbox{\hskip-104.01323pt\hbox{\hbox{$\displaystyle\displaystyle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\langle}}{n},{p_{e}}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\rangle}}={\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathcal{V}}}_{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}}({e})$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle n^{\prime}=k(n)$}\hskip
20.00003pt\hbox{\hskip-74.6745pt\hbox{\hbox{$\displaystyle\displaystyle
p_{e}\sqsubseteq p$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\operatorname{in-same-
func}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}},{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}.pc,n^{\prime})$}}}}}}}\vbox{\hbox{\hskip-74.6745pt\hbox{\hbox{$\displaystyle\displaystyle
p_{e}\sqsubseteq p$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\operatorname{in-same-
func}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}},{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}.pc,n^{\prime})$}}}}\vbox{}}}}\over\hbox{\hskip
52.48337pt\vbox{\vbox{}\hbox{\hskip-52.48335pt\hbox{\hbox{$\displaystyle\displaystyle{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}}\llparenthesis{\mathtt{jmp}_{{k}}\
{e}}\rrparenthesis_{p}\mathrel{\leadsto}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}[pc\mathbin{\vcentcolon=}n^{\prime}]$}}}}}}$
$\displaystyle\displaystyle{\hbox{\hskip
85.42464pt\vbox{\hbox{\hskip-85.42464pt\hbox{\hbox{$\displaystyle\displaystyle
p_{r}\not\sqsubseteq p^{\prime}\Longrightarrow p_{r}\sqsubseteq p$}\hskip
20.00003pt\hbox{\hskip-82.15373pt\hbox{\hbox{$\displaystyle\displaystyle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\langle}}{n},{p_{r}}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\rangle}}={\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}.R(r)$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle
R^{\prime}={\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}.R[r\mathbin{\vcentcolon=}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\langle}}{n},{p^{\prime}}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\rangle}}]$}}}}}}\vbox{\hbox{\hskip-82.15373pt\hbox{\hbox{$\displaystyle\displaystyle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\langle}}{n},{p_{r}}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\rangle}}={\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}.R(r)$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle
R^{\prime}={\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}.R[r\mathbin{\vcentcolon=}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\langle}}{n},{p^{\prime}}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\rangle}}]$}}}}\vbox{}}}}\over\hbox{\hskip
72.19797pt\vbox{\vbox{}\hbox{\hskip-72.19797pt\hbox{\hbox{$\displaystyle\displaystyle{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}}\llparenthesis{{r}\leftarrow\mathtt{movlabel}_{p^{\prime}}}\rrparenthesis_{p}\mathrel{\leadsto}{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}}^{++}[R\mathbin{\vcentcolon=}R^{\prime}]$}}}}}}$
$\displaystyle\displaystyle{\hbox{\hskip
152.17773pt\vbox{\hbox{\hskip-152.17773pt\hbox{\hbox{$\displaystyle\displaystyle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\langle}}{n},{p_{e}}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\rangle}}={\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathcal{V}}}_{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}}({e})$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\langle}}{m},{p_{m}}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\rangle}}={\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}.M(n)$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle p_{e}\sqsubseteq p$}\hskip
20.00003pt\hbox{\hskip-91.87671pt\hbox{\hbox{$\displaystyle\displaystyle
M^{\prime}={\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}.M[n\mathbin{\vcentcolon=}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\langle}}{m},{p^{\prime}}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\rangle}}]$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle p_{m}\not\sqsubseteq
p^{\prime}\Longrightarrow p_{m}\sqsubseteq
p$}}}}}}}}\vbox{\hbox{\hskip-91.87671pt\hbox{\hbox{$\displaystyle\displaystyle
M^{\prime}={\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}.M[n\mathbin{\vcentcolon=}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\langle}}{m},{p^{\prime}}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\rangle}}]$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle p_{m}\not\sqsubseteq
p^{\prime}\Longrightarrow p_{m}\sqsubseteq p$}}}}\vbox{}}}}\over\hbox{\hskip
72.7946pt\vbox{\vbox{}\hbox{\hskip-72.7946pt\hbox{\hbox{$\displaystyle\displaystyle{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}}\llparenthesis{\mathtt{storelabel}_{p^{\prime}}\
{e}}\rrparenthesis_{p}\mathrel{\leadsto}{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}}^{++}[M\mathbin{\vcentcolon=}M^{\prime}]$}}}}}}$
$\displaystyle\displaystyle{\hbox{\hskip
69.88713pt\vbox{\hbox{\hskip-69.88712pt\hbox{\hbox{$\displaystyle\displaystyle{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}.\Psi}\llparenthesis{c}\rrparenthesis\mathrel{\rightarrow}\Psi^{\prime}$}\hskip
20.00003pt\hbox{\hskip-66.68439pt\hbox{\hbox{$\displaystyle\displaystyle\operatorname{in-
same-
func}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}},{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}.\Psi.pc,\Psi^{\prime}.pc)$}}}}}\vbox{\hbox{\hskip-66.68439pt\hbox{\hbox{$\displaystyle\displaystyle\operatorname{in-
same-
func}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}},{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}.\Psi.pc,\Psi^{\prime}.pc)$}}}\vbox{}}}}\over\hbox{\hskip
38.4894pt\vbox{\vbox{}\hbox{\hskip-38.4894pt\hbox{\hbox{$\displaystyle\displaystyle{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}}\llparenthesis{c}\rrparenthesis\mathrel{\leadsto}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}[\Psi\mathbin{\vcentcolon=}\Psi^{\prime}]$}}}}}}$

Figure 21. Overlay Operational Semantics

$\displaystyle\displaystyle{\hbox{\hskip
95.34163pt\vbox{\hbox{\hskip-95.34163pt\hbox{\hbox{$\displaystyle\displaystyle[{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathit{SF}}}]\mathbin{{+}\mspace{-8.0mu}{+}}\\_={\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}.\mathit{stack}$}\hskip
20.00003pt\hbox{\hskip-89.93304pt\hbox{\hbox{$\displaystyle\displaystyle n\in
S_{p}\Longrightarrow
n\geq{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathit{SF}}}.\mathit{base}\wedge
n\neq{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathit{SF}}}.\mathit{ret\mbox{-}addr\mbox{-}loc}$}}}}}\vbox{\hbox{\hskip-89.93304pt\hbox{\hbox{$\displaystyle\displaystyle
n\in S_{p}\Longrightarrow
n\geq{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathit{SF}}}.\mathit{base}\wedge
n\neq{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathit{SF}}}.\mathit{ret\mbox{-}addr\mbox{-}loc}$}}}\vbox{}}}}\over\hbox{\hskip
32.73732pt\vbox{\vbox{}\hbox{\hskip-32.73732pt\hbox{\hbox{$\displaystyle\displaystyle\operatorname{writeable}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}},n)$}}}}}}$
$\displaystyle\displaystyle{\hbox{\hskip
149.0974pt\vbox{\hbox{\hskip-149.09738pt\hbox{\hbox{$\displaystyle\displaystyle
F={\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}.\mathit{funcs}(\mathit{target})$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle
F.\mathit{entry}=\mathit{target}$}\hskip
20.00003pt\hbox{\hskip-107.13889pt\hbox{\hbox{$\displaystyle\displaystyle
sp\in S_{p}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle[{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathit{SF}}}]\mathbin{{+}\mspace{-8.0mu}{+}}\\_={\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}.\mathit{stack}$}\hskip
20.00003pt\hbox{\hskip-62.06085pt\hbox{\hbox{$\displaystyle\displaystyle
sp\geq{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathit{SF}}}.\mathit{ret\mbox{-}addr\mbox{-}loc}+{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{F}}.\mathit{type}$}}}}}}}}}\vbox{\hbox{\hskip-107.13889pt\hbox{\hbox{$\displaystyle\displaystyle
sp\in S_{p}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle[{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathit{SF}}}]\mathbin{{+}\mspace{-8.0mu}{+}}\\_={\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}.\mathit{stack}$}\hskip
20.00003pt\hbox{\hskip-62.06085pt\hbox{\hbox{$\displaystyle\displaystyle
sp\geq{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathit{SF}}}.\mathit{ret\mbox{-}addr\mbox{-}loc}+{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{F}}.\mathit{type}$}}}}}}\vbox{\hbox{\hskip-62.06085pt\hbox{\hbox{$\displaystyle\displaystyle
sp\geq{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathit{SF}}}.\mathit{ret\mbox{-}addr\mbox{-}loc}+{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{F}}.\mathit{type}$}}}\vbox{}}}}}\over\hbox{\hskip
52.40111pt\vbox{\vbox{}\hbox{\hskip-52.40111pt\hbox{\hbox{$\displaystyle\displaystyle\operatorname{typechecks}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}},\mathit{target},sp)$}}}}}}$
$\displaystyle\displaystyle{\hbox{\hskip
81.75713pt\vbox{\hbox{\hskip-81.75711pt\hbox{\hbox{$\displaystyle\displaystyle[{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathit{SF}}}]\mathbin{{+}\mspace{-8.0mu}{+}}\\_={\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}.\mathit{stack}$}\hskip
20.00003pt\hbox{\hskip-62.764pt\hbox{\hbox{$\displaystyle\displaystyle\mathit{ret\mbox{-}addr\mbox{-}loc}={\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathit{SF}}}.\mathit{ret\mbox{-}addr\mbox{-}loc}$}}}}}\vbox{\hbox{\hskip-62.764pt\hbox{\hbox{$\displaystyle\displaystyle\mathit{ret\mbox{-}addr\mbox{-}loc}={\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathit{SF}}}.\mathit{ret\mbox{-}addr\mbox{-}loc}$}}}\vbox{}}}}\over\hbox{\hskip
65.36122pt\vbox{\vbox{}\hbox{\hskip-65.36122pt\hbox{\hbox{$\displaystyle\displaystyle\operatorname{is-
ret-addr-
loc}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}},\mathit{ret\mbox{-}addr\mbox{-}loc})$}}}}}}$
$\displaystyle\displaystyle{\hbox{\hskip
87.06348pt\vbox{\hbox{\hskip-87.06346pt\hbox{\hbox{$\displaystyle\displaystyle[{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathit{SF}}}]\mathbin{{+}\mspace{-8.0mu}{+}}\\_={\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}.\mathit{stack}$}\hskip
20.00003pt\hbox{\hskip-73.37672pt\hbox{\hbox{$\displaystyle\displaystyle\forall(r,n)\in{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathit{SF}}}.\mathit{csr\mbox{-}vals}.\leavevmode\nobreak\
{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}.R(r)=n$}}}}}\vbox{\hbox{\hskip-73.37672pt\hbox{\hbox{$\displaystyle\displaystyle\forall(r,n)\in{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathit{SF}}}.\mathit{csr\mbox{-}vals}.\leavevmode\nobreak\
{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}.R(r)=n$}}}\vbox{}}}}\over\hbox{\hskip
32.87505pt\vbox{\vbox{}\hbox{\hskip-32.87503pt\hbox{\hbox{$\displaystyle\displaystyle\operatorname{csr-
restored}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}})$}}}}}}$
$\displaystyle\displaystyle{\hbox{\hskip
88.0225pt\vbox{\hbox{\hskip-88.0225pt\hbox{\hbox{$\displaystyle\displaystyle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{F}}\in\operatorname{cod}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}.\mathit{funcs}})$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle
n,n^{\prime}\in\operatorname{dom}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{F}}.\mathit{instrs}})$}}}}\vbox{}}}\over\hbox{\hskip
46.3835pt\vbox{\vbox{}\hbox{\hskip-46.38348pt\hbox{\hbox{$\displaystyle\displaystyle\operatorname{in-
same-
func}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}},n,n^{\prime})$}}}}}}$
$\displaystyle\displaystyle{\hbox{\hskip
82.16794pt\vbox{\hbox{\hskip-82.16792pt\hbox{\hbox{$\displaystyle\displaystyle\forall{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{F}}\in\operatorname{cod}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}.\mathit{funcs}}).\leavevmode\nobreak\
n\notin\operatorname{dom}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{F}}.\mathit{instrs}})$}}}\vbox{}}}\over\hbox{\hskip
46.3835pt\vbox{\vbox{}\hbox{\hskip-46.38348pt\hbox{\hbox{$\displaystyle\displaystyle\operatorname{in-
same-
func}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}},n,n^{\prime})$}}}}}}$
$\displaystyle\displaystyle{\hbox{\hskip
72.95135pt\vbox{\hbox{\hskip-72.95135pt\hbox{\hbox{$\displaystyle\displaystyle\forall
i\in[1,n].\leavevmode\nobreak\
{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}.M(sp-i)={\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\langle}}{\\_},{\mathtt{lib}}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\rangle}}$}}}\vbox{}}}\over\hbox{\hskip
43.77722pt\vbox{\vbox{}\hbox{\hskip-43.77722pt\hbox{\hbox{$\displaystyle\displaystyle\operatorname{args-
secure}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}},sp,n)$}}}}}}$

Figure 22. Overlay Operational Semantics: Auxiliary Judgments

$\begin{array}[]{rcl}\operatorname{new-
frame}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}},\mathit{target},\mathit{ret\mbox{-}addr\mbox{-}loc})&\triangleq&\begin{array}[t]{lllll}\\{&\mathit{base}&=&\mathit{ret\mbox{-}addr\mbox{-}loc}-{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}.\mathit{funcs}(\mathit{target}).\mathit{type}\\\
&\mathit{ret\mbox{-}addr\mbox{-}loc}&=&\mathit{ret\mbox{-}addr\mbox{-}loc}\\\
&\mathit{csr\mbox{-}vals}&=&\\{(r,{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}.R(r))\\}_{r\in\mathbb{CSR}}&\\}\end{array}\\\
\\\ \operatorname{pop-
frame}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}})&\triangleq&{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}[\mathit{stack}\mathbin{\vcentcolon=}S]\quad\text{where
}[{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathit{SF}}}]\mathbin{{+}\mspace{-8.0mu}{+}}S={\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}.\mathit{stack}\\\
\\\
{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}}^{++}&\triangleq&\begin{cases}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}[\Psi\mathbin{\vcentcolon=}{\Psi}^{++}]&\operatorname{in-
same-
func}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}},{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}.pc,{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}.pc+1)\\\
{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathtt{oerror}}}&\text{otherwise}\end{cases}\\\
\\\
\operatorname{classify}_{\mathbb{C}}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}})&\triangleq&{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}[M\mathbin{\vcentcolon=}M^{\prime},R\mathbin{\vcentcolon=}R^{\prime}]\\\
&&\text{where
}M^{\prime}(n)={\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\langle}}{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\langle}}{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}.M(n)}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\rangle}}},{\mathbb{C}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}.\Psi)(n)}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\rangle}}\\\
&&\phantom{\text{where
}}R^{\prime}(r)={\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\langle}}{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\langle}}{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}.R(r)}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\rangle}}},{\mathbb{C}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}.\Psi)(r)}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\rangle}}\\\
\\\
{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathcal{V}}}_{\Psi}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{v}}})&\triangleq&{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{v}}\\\
{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathcal{V}}}_{\Psi}({r})&\triangleq&\Psi.R(r)\\\
{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathcal{V}}}_{\Psi}({sp})&\triangleq&{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\langle}}{\Psi.sp},{\mathtt{lib}}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\rangle}}\\\
{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathcal{V}}}_{\Psi}({pc})&\triangleq&{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\langle}}{\Psi.pc},{\mathtt{lib}}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\rangle}}\\\
{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathcal{V}}}_{\Psi}({e\oplus
e^{\prime}})&\triangleq&{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\langle}}{v\oplus
v^{\prime}},{p\sqcup
p^{\prime}}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\rangle}}\\\
&&\text{where
}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\langle}}{v},{p}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\rangle}}={\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathcal{V}}}_{\Psi}({e})\\\
&&\phantom{\text{where
}}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\langle}}{v^{\prime}},{p^{\prime}}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\rangle}}={\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathcal{V}}}_{\Psi}({e^{\prime}})\\\
\\\
{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\langle}}{n}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\rangle}}&\triangleq&{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\langle}}{n},{\\_}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\rangle}}\\\
\\\ \mathtt{app}\sqcup p&\triangleq&\mathtt{app}\\\
p\sqcup\mathtt{app}&\triangleq&\mathtt{app}\\\
\mathtt{lib}\sqcup\mathtt{lib}&\triangleq&\mathtt{lib}\\\ \end{array}$

Figure 23. Overlay Operational Semantics: Auxiliary Definitions

###### Lemma 0 (Overlay is a refinement).

For any
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}\mathrel{\leadsto}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi^{\prime}}}$,
if
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi^{\prime}}}\neq{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathtt{oerror}}}$,
then
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}.\Psi\mathrel{\rightarrow}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi^{\prime}}}.\Psi$

###### Lemma 0 (Overlay is equivalent on application reduction).

For any
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}$,
if
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}.\Psi\mathrel{\xrightarrow{\mathtt{app}}}\Psi^{\prime}$,
then
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}\mathrel{\leadsto}\\{\Psi\mathbin{\vcentcolon=}\Psi^{\prime},\mathit{funcs}\mathbin{\vcentcolon=}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}.\mathit{funcs},\mathit{stack}\mathbin{\vcentcolon=}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}.\mathit{stack}\\}$.

###### Theorem 3 (Overlay Integrity Soundness).

If
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi_{0}}}\in\mathit{Program}$,
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi_{0}}}\mathrel{\mathrel{\leadsto}^{n}}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi_{1}}}$,
${{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi_{1}}}}\llparenthesis{\\_}\rrparenthesis_{\mathtt{app}}$,
and
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi_{1}}}\mathrel{\mathrel{\leadsto}^{\ast}}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi_{2}}}$
such that
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi_{1}}}.\Psi\mathrel{\xrightarrow{\\!\text{wb}}}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi_{2}}}.\Psi$
with
$\pi={\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi_{0}}}.\Psi\mathrel{\mathrel{\rightarrow}^{n}}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi_{1}}}.\Psi$,
then

  1. (1)

$\mathcal{CSR}(\pi,{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi_{1}}}.\Psi,{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi_{2}}}.\Psi)$

  2. (2)

$\mathcal{RA}(\pi,{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi_{1}}}.\Psi,{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi_{2}}}.\Psi)$

###### Proof.

By induction over the definition of a well-bracketed step and nested induction
over the logical call stack. The last step follows by the fact that
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi_{2}}}\neq{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathtt{oerror}}}$,
and therefore the restoration checks in the overlay monitor passed. ∎

###### Theorem 4 (Overlay Confidentiality Soundness).

If
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi_{0}}}\in\mathit{Program}$,
${{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi_{1}}}}\llparenthesis{\\_}\rrparenthesis_{\mathtt{lib}}$,
${{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi_{3}}}}\llparenthesis{\\_}\rrparenthesis_{\mathtt{app}}$,
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi_{0}}}.\Psi\mathrel{\mathrel{\rightarrow}^{\ast}}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi_{1}}}.\Psi\mathrel{\xrightarrow{\mathtt{lib}}\mathrel{\vphantom{\to}{}^{n}}}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi_{2}}}.\Psi\mathrel{\rightarrow}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi_{3}}}.\Psi$,
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi_{1}}}\mathrel{\mathrel{\leadsto}^{n+1}}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi_{3}}}$,
and
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi_{1}}}=_{\mathtt{lib}}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi_{1}^{\prime}}}$,
then
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi_{1}^{\prime}}}.\Psi\mathrel{\xrightarrow{\mathtt{lib}}\mathrel{\vphantom{\to}{}^{n}}}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi_{2}^{\prime}}}.\Psi\mathrel{\rightarrow}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi_{3}^{\prime}}}.\Psi$,
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi_{1}^{\prime}}}\mathrel{\mathrel{\leadsto}^{n+1}}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi_{3}^{\prime}}}$
${{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi_{3}^{\prime}}}}\llparenthesis{\\_}\rrparenthesis_{\mathtt{app}}$,
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi_{3}}}.pc={\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi_{3}^{\prime}}}.pc$,
and

  1. (1)

${{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi_{2}}}}\llparenthesis{\mathtt{gatecall}_{n^{\prime}}\
{e}}\rrparenthesis$,
${{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi_{2}^{\prime}}}}\llparenthesis{\mathtt{gatecall}_{n^{\prime}}\
{e}}\rrparenthesis$, and
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi_{3}}}=_{\mathtt{call}\
n^{\prime}}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi_{3}^{\prime}}}$
or

  2. (2)

${{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi_{2}}}}\llparenthesis{\mathtt{gateret}}\rrparenthesis$,
${{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi_{2}^{\prime}}}}\llparenthesis{\mathtt{gateret}}\rrparenthesis$,
and
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi_{3}}}=_{\mathtt{ret}}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi_{3}^{\prime}}}$,

###### Proof.

Proof is standard for an IFC enforcement system. ∎

##  Appendix D WebAssembly

$\displaystyle\displaystyle{\hbox{\hskip
30.27039pt\vbox{\hbox{\hskip-30.27039pt\hbox{\hbox{$\displaystyle\displaystyle{\Psi}\llparenthesis{\mathtt{call}\
{i}}\rrparenthesis\mathrel{\rightarrow}\Psi^{\prime}$}}}\vbox{}}}\over\hbox{\hskip
61.75563pt\vbox{\vbox{}\hbox{\hskip-61.75563pt\hbox{\hbox{$\displaystyle\displaystyle{\Psi}\llparenthesis{\mathtt{gatecall}_{n}\
{i}}\rrparenthesis_{\mathtt{app}}\mathrel{\rightarrow}\Psi^{\prime}[p\mathbin{\vcentcolon=}\mathtt{lib}]$}}}}}}$
$\displaystyle\displaystyle{\hbox{\hskip
31.72093pt\vbox{\hbox{\hskip-31.72093pt\hbox{\hbox{$\displaystyle\displaystyle{\Psi}\llparenthesis{\mathtt{call}_{{I}}\
{i}}\rrparenthesis\mathrel{\rightarrow}\Psi^{\prime}$}}}\vbox{}}}\over\hbox{\hskip
62.85564pt\vbox{\vbox{}\hbox{\hskip-62.85562pt\hbox{\hbox{$\displaystyle\displaystyle{\Psi}\llparenthesis{\mathtt{gatecall}_{n}\
{i}}\rrparenthesis_{\mathtt{lib}}\mathrel{\rightarrow}\Psi^{\prime}[p\mathbin{\vcentcolon=}\mathtt{app}]$}}}}}}$
$\displaystyle\displaystyle{\hbox{\hskip
52.1568pt\vbox{\hbox{\hskip-52.15678pt\hbox{\hbox{$\displaystyle\displaystyle{\Psi}\llparenthesis{\mathtt{ret}}\rrparenthesis\mathrel{\rightarrow}\Psi^{\prime}$}\hskip
20.00003pt\hbox{\hskip-34.96791pt\hbox{\hbox{$\displaystyle\displaystyle
p^{\prime}=\mathtt{lib}\Leftrightarrow
p=\mathtt{app}$}}}}}\vbox{\hbox{\hskip-34.96791pt\hbox{\hbox{$\displaystyle\displaystyle
p^{\prime}=\mathtt{lib}\Leftrightarrow
p=\mathtt{app}$}}}\vbox{}}}}\over\hbox{\hskip
53.87505pt\vbox{\vbox{}\hbox{\hskip-53.87503pt\hbox{\hbox{$\displaystyle\displaystyle{\Psi}\llparenthesis{\mathtt{gateret}}\rrparenthesis_{p}\mathrel{\rightarrow}\Psi^{\prime}[p\mathbin{\vcentcolon=}\mathtt{app}]$}}}}}}$

Figure 24. WebAssembly Trampoline and Springboard | current block spill slots
---|---
| …
| function locals
| …
$sp\longrightarrow$ | saved $\mathbb{CSR}$
| …
| return address
| arguments
| …
Figure 25. WebAssembly Stack Frame

WebAssemblyFunction | WF | $\mathrel{\vcentcolon\vcentcolon=}$ | $\begin{array}[t]{lllll}\\{&|args|&\mathrel{\vcentcolon}&\mathbb{N}\\\ &|locals|&\mathrel{\vcentcolon}&\mathbb{N}\\\ &entry&\mathrel{\vcentcolon}&\textit{Block}\\\ &exits&\mathrel{\vcentcolon}&\wp({\textit{Block}})\\\ &blocks&\mathrel{\vcentcolon}&\wp({\textit{Block}})&\\}\end{array}$
---|---|---|---