Artifact of "Endangered by the Language But Saved by the Compiler: Robust Safety via Semantic Back-Translation"

Appendix of Endangered by the Language But Saved by the Compiler: Robust Safety via Semantic Back-Translation NIKLAS MÜCK,MPI-SWS, Germany AÏNA LINN GEORGES,MPI-SWS, Germany DEREK DREYER,MPI-SWS, Germany DEEPAK GARG,MPI-SWS, Germany MICHAEL SAMMLER,Institute of Science and Technology Austria (ISTA), Austria A Definition of UNIV This section presents the details of the definition of UNIV that overapproximates all Cap programs. UNIV is defined as a semantic DimSum module based on preand postconditions, similar to SIM . The definition is a little more involved than the definition of SIM because our target language Cap is less abstract and has a separate stack. It is inspired by prior work on universal contracts for capability machines [3,4,1,2]. First, we need to define a notion of shadow stacks shd ∈ShadowStack that consist of shadow frames sf ∈ShadowFrame (Fig. 1). These shadows stacks are necessary since the operational semantic of Cap can reuse stack frames and thus just the depth of a stack frame does not uniquely identify it. Thus, the shadow stacks associate ghost identifiers 𝜄∈GhostId with the (physical) stack. This association is encoded by the shd ∼s relation that states that the shadow stack shd and physical stack s agree. We use the ghost ids in capProp for defining points-to predicates for the stack. Additionally, we need to ensure that UNIV does not break well-bracketed control flow, i.e., does not skip stack frames without returning. For that we define a stepping relation of valid internal operations to a (shadow) stack → that a program with address space A can do. In particular, it can only return if the return and continue exectuing if the return address is within A (see shd-ret). We write →*as the reflexive transitive closure of the relation. Next, we define a set of (pure) Cap language invariants LangInv that are necessary to ensure capability safety of Cap : There must be no dangling pointers, the stack is directed, and the heap contains no stack pointers. With that we can finally define UNIV in Fig. 2. Similar to the definition of SIM , inv 𝐿,shd UNIV(s,m) contains the state interpretations that tie the separation logic to the current physical state of the stack and heap. Note that the state interpretation of the stack is parametrized over the current shadow stack for the mapping of physical stack ids and ghost ids. Again it contains the global view of low capabilities and ensures that they are transitively low.  𝐿 a set of already allocated capabilities that are not low. (This set is used in the semantic back-translation proof). It can be chosen in the precondition of UNIV and is preserved in the postcondition. The preUNIV and postUNIV enforce that all registers only contain low values and the inv UNIV and LangInv hold for the current state passed by the Jump -event. The UNIV keeps as state the last Authors’ Contact Information: Niklas Mück, MPI-SWS, Saarland Informatics Campus, Germany, [email protected]; Aïna Linn Georges, MPI-SWS, Saarland Informatics Campus, Germany, [email protected]; Derek Dreyer, MPI-SWS, Saarland Informatics Campus, Germany, [email protected]; Deepak Garg, MPI-SWS, Saarland Informatics Campus, Germany, [email protected]; Michael Sammler, Institute of Science and Technology Austria (ISTA), Klosterneuburg, Austria, [email protected]. 2018. ACM 2475-1421/2018/1-ART1 https://doi.org/ Proc. ACM Program. Lang., Vol. 1, No. CONF, Article 1. Publication date: January 2018. 1:2 Niklas Mück, Aïna Linn Georges, Derek Dreyer, Deepak Garg, and Michael Sammler ShadowFrame ∋sf ≜ B × P(Z) × Word ×HeapCap ×option(GhostId) ShadowStack ∋shd ≜(L (ShadowFrame),P(GhostId)) shd ∼s≜shd.1=s.1∧shd.2=dom(s.2) ∧ shd.3=s.3∧shd.4=s.4 shd-call ret.a−1∈A (shd,I) →A(shd + + (false,∅,sp,ret,None),I⊎{𝜄}) shd-ret ret.a∈A (shd + + (_,_,_,ret,_),I) →A(shd,I) shd-alloc (shd + + (false,∅,sp,ret,None),I) →A(shd + + (true,d,sp,ret,Some(𝜄)),I⊎{𝜄}) LangInv(r,m,s)≜NoDanglingPointer(r,m,s) ∧ Directed(s) ∧ NoStkPointer(m) Fig. 1. Language Invariants of Cap inv 𝐿,shd UNIV(s,m)≜SIshd stk (s) ∗ SIheap(m) ∗ ∃𝐿⊎ 𝐿. LowAuth(𝐿) ∗ ∗ c∈𝐿 ∃w.c↦→m/sw∗lowshd(w) preA?,E! UNIV (e,shd,call_stk)⇀(shd′,call_stk′, 𝐿)≜∃r,m,s.inv 𝐿,shd′ UNIV (s,m) ∗ ∗ w∈r lowshd′(w) ∗LangInv(r,m,s) ∗ e=Jump?(r,m,s)∗shd′∼s∗pc(r).a∈ A?∗ 𝐿⊆I(shd′) ∗ ∃A⊎ A?.shd →*Ashd′∗ ∃shdpre ret.shd′=shdpre + + (_,_,_,ret,_) ∗ ret.a∉A? ∗call_stk′=shd′ ?:: call_stk ∨∃shdpre.shd →*Ashdpre ∗shdpre =shd′ + + (_,_,sp(r),pc(r),_) ∗call_stk =shdpre!::call_stk′ postA?,E! UNIV (e,shd′,call_stk′)↽(shd,call_stk, 𝐿)≜∃r,m,s.inv 𝐿,shd′ UNIV (s,m) ∗ ∗ w∈r lowshd′(w) ∗LangInv(r,m,s) ∗ e=Jump!(r,m,s)∗shd′∼s∗pc(r).a∉A? shd →*A?shd′∗ ∃shdpre ret.shd′=shdpre + + (_,_,_,ret,_) ∗ ret.a∈ A? ∗call_stk′=shd′ !:: call_stk ∨∃shdpre.shd →*Ashdpre ∗shdpre =shd′ + + (_,_,sp(r),pc(r),_) ∗call_stk =shdpre?::call_stk′ Fig. 2. Definition of UNIV shd it saw. In the pre-condition it is given a shd′∼s and then assumes that it was derived by only valid operations →*A by on an external address space A⊎ A? . In the post-condition it proves accordingly that the new shd′ was derived by the old one only by operations within A? . Jumps that were emitted by the ret -instruction, do a non-local operation on the stack that is therefore not captured by →* and treated separately in the preUNIV and postUNIV . Additionally, it is ensured that the sp and pc stored on the stack are correctly loaded back into the registers. In order to more Proc. ACM Program. Lang., Vol. 1, No. CONF, Article 1. Publication date: January 2018. Appendix of Endangered by the Language But Saved by the Compiler: Robust Safety via Semantic Back-Translation 1:3 continently assert that well-bracketedness implies that the shd at the time of a call is restored at the time of a return, UNIV keeps a list of open calls call_stk in its state together with the information where the call came from. References [1] Aïna Linn Georges, Armaël Guéneau, Thomas Van Strydonck, Amin Timany, Alix Trieu, Sander Huyghebaert, Dominique Devriese, and Lars Birkedal. 2021. Efficient and provable local capability revocation using uninitialized capabilities. Proc. ACM Program. Lang. 5, POPL (2021), 1–30. doi:10.1145/3434287 [2] Aïna Linn Georges, Alix Trieu, and Lars Birkedal. 2022. Le temps des cerises: efficient temporal stack safety on capability machines using directed capabilities. Proc. ACM Program. Lang. 6, OOPSLA1 (2022), 1–30. [3] Lau Skorstengaard, Dominique Devriese, and Lars Birkedal. 2020. Reasoning about a Machine with Local Capabilities: Provably Safe Stack and Return Pointer Management. ACM Trans. Program. Lang. Syst. 42, 1 (2020), 5:1–5:53. doi:10. 1145/3363519 [4] Lau Skorstengaard, Dominique Devriese, and Lars Birkedal. 2021. StkTokens: Enforcing well-bracketed control flow and stack encapsulation using linear capabilities. J. Funct. Program. 31 (2021), e9. doi:10.1017/S095679682100006X Proc. ACM Program. Lang., Vol. 1, No. CONF, Article 1. Publication date: January 2018.