- a language for more naturally illustrating mutual distrust
- mutually distrustful components interacting via procedure calls
- keep this as simple as possible, but without trivializing
- have some interesting undefined behaviors in source language
that can be exploited in interesting ways at low level
- so we added (statically allocated, 2nd-class, component-local) buffers and buffer overflows
e ::= i | e₁ ⊗ e₂ | if e then e₁ else e₂ | b[e] | b[e₁] := e₂ | C.P(e) | exit
n ::= O | S n – natural number identifiers C ::= n – component identifier (globally unique “name”) P ::= n – procedure identifier (index relative to a given component) b ::= n – buffer identifier (index relative to current component)
operators (⊗) ∈ {(;), (+), …} – arbitrary binary functions on integers
procedure identifiers P of each component C mapped to procedures bodies, which are expressions e
- procedures’ single argument is passed in location 0 of buffer 0 of the callee component
- location 0 of variable 0 of the callee component is automatically restored on returns (reader monad)
procedures can of course be mutually recursive (global call stack)
buffers are 2nd class
Examples below are provided in a human-readable syntax that best matches the actual syntax of the language. Please note that there is no formalisation of this human-readable syntax.
component factorial { (* every component has at least one buffer, here called “vars” *) buff vars = { 0 }
proc main { (* procedure call argument goes in vars[0] *) if vars[0] <= 1 then 1 else (* vars[0] is changed upon call but restored upon return, so these updates are transparent to the programmer *) factorial.main(vars[0] - 1) * vars[0] } }
component factorial_buff { buff vars = { 0, 0 } (* buffer size is static and doesn’t change *)
proc main { (* argument goes in vars[0] ) ( we use vars[1] as an accumulator variable storing (n * … * i) *) vars[1] := vars[0]; factorial_buff.aux(vars[0]) }
private proc aux { if vars[0] <= 1 then vars[1] else begin vars[1] := vars[1] * (vars[0] - 1); factorial_buff.aux(vars[0] - 1) end } }
(* the starting component has a special name “main” *) component main { buff vars = { 0 }
(* execution starts in the first procedure, here called “main” *) proc main { (* argument goes in vars[0] *) factorial_buff.main(2) } }
- vars =def 0 – the first buffer used to store variables
- x =def vars[x] – variable lookup becomes buffer lookup
- x:=e
def vars[x] :e – variable assignment becomes buffer update
Note that accessing the vars buffer out of bounds is not caught statically and will be an undefined behavior dynamically (so in a way we did lose something when we encoded variables with buffers).
A component contains:
- a component name C
- a map from buffer identifiers to fixed-size lists of integers (private to the component)
- list of public and private procedures
- as in OO language procedure identifiers are just local indices
global call stack
only ints can be passed between components
- this restriction simplifies many things throughout (and especially in the target machine, where we need no “type tagging”)
A component interface contains:
- a component name C
- the names of its public procedures
- for this simple language
- we can derive a component’s interface uniquely from its code (but this means that the code already has information like which procedures are private)
- we can derive the interface at which other components are used
κ – component body κ.name ↦ C κ.bnum ↦ b – [0,b) are all buffers κ.bufs[b] ↦ [i₀, …, iₙ] – list of integer values for buffer b ∈ [0,κ.bnum) κ.pnum ↦ P – [0,P) are all procedures κ.export ↦ Q – [0,Q) are public procedures, [Q,P) are private procedures κ.procs[P] ↦ e – body for procedure P ∈ [0,κ.pnum)
ι — component interface ι.name ι.export ↦ Q ι.import ↦ {C₀.P₀, …, Cₘ.Pₘ} – don’t have to import all components or all procedures exported by an imported component; and this feature is used for least privilege
interfaceof(κ) — compute the interface of a component interfaceof(κ) ::= ι where ι.name = κ.name ι.export = κ.export ι.import = ⋃ { extprocsin(κ.name, e) | ∃P ∈ [0,κ.pnum). κ.procs[P] = e }
extprocsin(C, e) – syntactically extract all called procedures in e that are external with respect to C extprocsin(C, e) ::= { C’.P | C’.P ∈ procsin(e), C’ ≠ C }
intprocsin(C, e) – syntactically extract all called procedures in e that are internal with respect to C intprocsin(C, e) ::= procsin(e) ∖ extprocsin(e)
procsin(e) – syntactically extract all called procedures in e
procsin(e) ::=
match e with
i | exit => ∅
C.P(e) => { C.P } ∪ procsin(e)
b[e] > procsin(e)
e₁ ⊗ e₂ | b[e₁] : e₂ => procsin(e₁) ∪ procsin(e₂)
if e then e₁ else e₂ =>
procsin(e) ∪ procsin(e₁) ∪ procsin(e₂)
bufsin(e) – syntactically extract all used buffers in e
bufsin(e) ::=
match e with
i | exit => ∅
C.P(e) => bufsin(e)
b[e] > {b} ∪ bufsin(e)
b[e₁] : e₂ => {b} ∪ bufsin(e₁) ∪ bufsin(e₂)
e₁ ⊗ e₂ => bufsin(e₁) ∪ bufsin(e₂)
if e then e₁ else e₂ =>
bufsin(e) ∪ bufsin(e₁) ∪ bufsin(e₂)
bufsin(κ) ::= map bufsin κ.procs
φ – program φ ::= {κ₀, …, κₙ}
φ[C] – component access φ[C] ::= κᵢ₀ when {κᵢ | κᵢ.name = C} = {κᵢ₀}
ψ – program interface ψ ::= {ι₀, …, ιₙ}
ψ[C] – component interface access ψ[C] ::= ιᵢ₀ when {ιᵢ | ιᵢ.name = C} = {ιᵢ₀}
interfaceof(φ) — compute the interface of a program interfaceof({κ₀,…,κₙ}) ::= {interfaceof(κ₀),…,interfaceof(κₙ)} where
main is an arbitrarily chosen, fixed component name (C), e.g. 0. It is the name of the component that starts computation.
For a partial program: ψ ⊢ φ well formed
For a whole program: φ whole well formed
comps({C₀.P₀, …, Cₘ.Pₘ}) = {C₀,…,Cₘ} – all components in an import comps({κ₀, …, κₙ}) = {κ₀.name, …, κₙ.name} – all components of a program comps({ι₀, …, ιₙ}) = {ι₀.name, …, ιₙ.name} – all components of a program interface
comps(ι.import) ⊆ comps(ψ)\{ι.name} — all imported components are defined ∀(C.P ∈ ι.import). P ∈ [0, ψ[C].export) – all imported external procedures are public ——————————————————————————————————————— ψ ⊢ ι well formed
∀ ι ∈ ψ. ψ ⊢ ι well formed ∀ ι₁ ι₂ ∈ ψ. ι₁.name ≠ ι₂.name — names are unique ∃ι ∈ ψ. ι.name = main ∧ ι.export ≥ 1 — required to start the program ————————————————————————————————————— ⊢ ψ well formed
ι₁.name = ι₂.name ι₁.import ⊆ ι₂.import ι₁.export = ι₂.export ————————————————————— ι₁ ⊆ ι₂ – interface compatibility
interfaceof(κ) ⊆ ψ[κ.name] – κ appears in ψ with a compatible interface ∀(_.P ∈ intprocsin(κ)). P ∈ [0, κ.pnum) – all used internal procedures are defined bufsin(κ) ⊆ [0,κ.bnum) – all used buffers are defined κ.export ≤ κ.pnum – sanity check κ.bnum ≥ 1 ∧ length(κ.bufs[0]) ≥ 1 – sanity check, to transfer call argument ——————————————————————————————————————— ψ ⊢ κ well formed
∀ κ ∈ φ. ψ ⊢ κ well formed —————————————————————————— ψ ⊢ φ well formed
ψ = interfaceof(φ) ⇒ ⊢ ψ well formed ψ ⊢ φ well formed ———————————————————— φ whole well formed
Δ, C ⊢ s, e ⇓ s’, i
Δ[C,P] = e – if e is the body of procedure P in component C C – the currently executing component s[C,b] – mapping buffer b of C component to fixed-size list of integers
procbodies(φ) ::= Δ where Δ[C,P] = φ[C].procs[P]
s[C,b,i] ::: i’ access local buffer cell after checking bounds s[C,b,i ↦ i’] ::: s’ update local buffer cell after checking bounds
—————————————————— :: E_Int Δ, C ⊢ s, i ⇓ s, i
Δ, C ⊢ s, e₁ ⇓ s’, i₁ Δ, C ⊢ s’, e₂ ⇓ s”, i₂ ———————————————————————————————— :: E_BinOp Δ, C ⊢ s, e₁ ⊗ e₂ ⇓ s”, i₁ ⊗ i₂
Δ, C ⊢ s, e ⇓ s’, i where i ≠ 0 Δ, C ⊢ s’, e₁ ⇓ s”, i₁ ———————————————————————————————————————— :: E_IfNZ Δ, C ⊢ s, if e then e₁ else e₂ ⇓ s”, i₁
Δ, C ⊢ s, e ⇓ s’, 0 Δ, C ⊢ s’, e₂ ⇓ s”, i₂ ———————————————————————————————————————— :: E_IfZ Δ, C ⊢ s, if e then e₁ else e₂ ⇓ s”, i₂
Δ, C ⊢ s, e ⇓ s’, i —————————————————————————————— :: E_Read Δ, C ⊢ s, b[e] ⇓ s’, s’[C,b,i]
Δ, C ⊢ s, e₁ ⇓ s’, i Δ, C ⊢ s’, e₂ ⇓ s”, i’ ——————————————————————————————————————————— :: E_Write Δ, C ⊢ s, b[e₁] := e₂ ⇓ s”[C,b,i ↦ i’], i’
Δ[C’,P] = eₚ Δ, C ⊢ s, e ⇓ s’, iₐ Δ, C’ ⊢ s’[C’,0,0 ↦ iₐ], eₚ ⇓ s”, iᵣ —————————————————————————————————————————————— :: E_Call Δ, C ⊢ s, C’.P(e) ⇓ s”[C,0,0 ↦ s’[C,0,0]], iᵣ
—————————————————————————— :: E_Exit Δ, C ⊢ s, exit ⇓ s, EXITED
- error monad rules to propagate this everywhere
e.g.
Δ, C ⊢ s, e₁ ⇓ s’, EXITED ———————————————————————————————— :: E_BinOp Δ, C ⊢ s, e₁ ⊗ e₂ ⇓ s’, EXITED
- using a single stack for both local and cross-compartment calls
cfg ::= (C, s, σ, K, e)
E ::= – flat evaluation contexts □⊗e₂ | i₁⊗□ | if □ then e₁ else e₂ | b[□] | b[□] := e₂ | b[i] := □ C.P(□) |
K ::= E :: K | [] – continuations
σ ::= (C,i,K) :: σ | [] – call stack
s[C,b] ↦ [i₀, …, iₙ] – integer list for buffer b
s[C,b,j] = iⱼ when s[C,b] = [i₀, …, iₙ] ─ read buffer C.b at position j
Initial configurations: I(φ) — initial configuration for a whole program φ I(φ) ::= (main, s[main,0,0 ↦ 0], [], [], φ[main].procs[0]) where φ = {κ₀,…,κₙ} s = { κ₀.name,b ↦ κ₀.bufs[b] | b ∈ dom(κ₀.bufs) } ⊎ … ⊎ { κₙ.name,b ↦ κₙ.bufs[b] | b ∈ dom(κₙ.bufs) }
Final configurations: (C,s, σ, K, exit) final (Final_Exit) (C,s,[],[], i) final (Final_Value)
Δ ⊢ (C, s, σ, K, e₁⊗e₂) → (C, s, σ, □⊗e₂ :: K, e₁) (S_BinOp_Push)
Δ ⊢ (C, s, σ, □⊗e₂ :: K, i₁) → (C, s, σ, i₁⊗□ :: K, e₂) (S_BinOp_Switch)
Δ ⊢ (C, s, σ, i₁⊗□ :: K, i₂) → (C, s, σ, K, i₁⊗i₂) (S_BinOp_Pop)
Δ ⊢ (C, s, σ, K, if e then e₁ else e₂) → (C, s, σ, if □ then e₁ else e₂ :: K, e) (S_If_Push)
i ≠ 0 —————————————————————————————————————————————————————————————— (S_If_Pop_NZ) Δ ⊢ (C, s, σ, if □ then e₁ else e₂ :: K, i) → (C, s, σ, K, e₁)
Δ ⊢ (C, s, σ, if □ then e₁ else e₂ :: K, 0) → (C, s, σ, K, e₂) (S_If_Pop_Z)
Δ ⊢ (C, s, σ, K, b[e]) → (C, s, σ, b[□] :: K, e) (S_Read_Push)
Δ ⊢ (C, s, σ, b[□] :: K, i) → (C, s, σ, K, s[C,b,i]) (S_Read_Pop)
Δ ⊢ (C, s, σ, K, b[e₁] := e₂) → (C, s, σ, b[□] := e₂ :: K, e₁) (S_Write_Push)
Δ ⊢ (C, s, σ, b[□] := e₂ :: K, i) → (C, s, σ, b[i] := □ :: K, e₂) (S_Write_Swap)
Δ ⊢ (C, s, σ, b[i] := □ :: K, i’) → (C, s[C,b,i ↦ i’], σ, K, i’) (S_Write_Pop)
Δ ⊢ (C, s, σ, K, C’.P’(e)) → (C, s, σ, C’.P’(□) :: K, e) (S_Call_Push)
Δ[C’,P’] = eₚ ——————————————————————————————————————————————————————————————————— (S_Call_Pop) Δ ⊢ (C, s, σ, C’.P’(□) :: K, iₐ) → (C’, s[C’,0,0 ↦ iₐ], (C,s[C,0,0],K) :: σ, [], eₚ)
Δ ⊢ (C, s, (C’,iₐ,K) :: σ, [], i) → (C’, s[C’,0,0 ↦ iₐ], σ, K, i) (S_Return)
Note: At this level we don’t need to enforce interfaces in the operational semantics. The interface is syntactically extracted from the code, so the code trivially respects the interface (this can be seen as an invariant of reduction: code never changes since it’s on the left of ⊢).
Δ ⊢ cfg →* cfg
Δ ⊢ cfg →* cfg’ Δ ⊢ cfg’ → cfg” ————————————————— Δ ⊢ cfg →* cfg”
∀ cfg’, ¬(Δ ⊢ cfg → cfg’) ————————————————————————— Δ ⊢ cfg ↛
∀ cfg Δ. Δ ⊢ cfg → cfg₁ ∧ Δ ⊢ cfg → cfg₂ ⇒ cfg₁ = cfg₂
η – component well-formedness invariants (preserved by reduction) η.name η.pnum η.bnum η.blens – list of lengths of the component’s buffers
Γ – partial program well-formedness invariant Γ ::= {η₀, …, ηₙ}
Γ[C] – component access Γ[C] ::= ηᵢ₀ when {ηᵢ | ηᵢ.name = C} = {ηᵢ₀}
wfinv(κ) ::= η where η.name = κ.name η.pnum = κ.pnum η.bnum = κ.bnum η.blens = map length κ.bufs
wfinv(φ) ::= Γ where φ = {κ₀, …, κₙ} Γ = {wfinv(κ₀), …, wfinv(κₙ)}
extprocsin(ι.name, e) ⊆ ι.import – all used external procedures are imported ∀(_.P ∈ intprocsin(ι.name, e)). P ∈ [0, η.pnum) – all used internal procedures are defined bufsin(e) ⊆ [0,η.bnum) – all used buffers are defined ——————————————————————————————————————————————— ι; η ⊢ e well formed
extprocsin(ι.name, E) ⊆ ι.import – all used external procedures are imported ∀(_.P ∈ intprocsin(ι.name, E)). P ∈ [0, η.pnum) – all used internal procedures are defined bufsin(E) ⊆ [0,η.bnum) – all used buffers are defined ——————————————————————————————————————————————— ι; η ⊢ E well formed
ι; η ⊢ E well formed ι; η ⊢ K well formed ————————————————————————— ι; η ⊢ E :: K well formed
————————————————————— ι; η ⊢ [] well formed
————————————————————— ψ; Γ ⊢ [] well formed
ψ[C]; Γ[C] ⊢ K well formed ψ; Γ ⊢ σ well formed ————————————————————————————— ψ; Γ ⊢ (C,i,K)::σ well formed
∀ η ∈ Γ, b, i, b ∈ [0,η.bnum) ∧ i ∈ [0,η.blens[b]) ⇒ s[η.name,b,i] is defined ————————————————————————————————————— Γ ⊢ s well formed
Γ ⊢ s well formed ψ; Γ ⊢ σ well formed ψ[C]; Γ[C] ⊢ K well formed ψ[C]; Γ[C] ⊢ e well formed ————————————————————————————————————————————————— ψ; Γ ⊢ (C, s, σ, K, e) well formed
∀φ. φ well formed ⇒ let ψ = interfaceof(φ) in let Γ = wfinv(φ) in ψ; Γ ⊢ I(φ) well formed
For any well-formed configuration cfg one of the following holds:
- cfg is a final configuration (value or exit)
- cfg takes a step
- cfg is stuck but of one of the following forms: (a) (C, s, σ, b[□] :: K, i) where s[C,b,i] is undefined (b) (C, s, σ, b[i] := □ :: K, i’) where s[C,b,i] is undefined
Formally: ∀ φ. φ well formed ⇒ ψ = interfaceof(φ) ∧ Γ = wfinv(φ) ∧ Δ = procbodies(φ) ⇒ ∀ cfg. ψ; Γ ⊢ cfg well formed ⇒ cfg final ∨ cfg undef ∨ (∃ cfg’. Δ ⊢ cfg → cfg’)
where
s[C,b] = [i₀, …, iₙ] i ∉ {0, …, n} ————————————————————————————— Undef_Load (C, s, σ, b[□] :: K, i) undef
s[C,b] = [i₀, …, iₙ] i ∉ {0, …, n} ——————————————————————————————————— Undef_Store (C, s, σ, b[i] := □ :: K, i’) undef
Formally: ∀ φ. φ well formed ⇒ ψ = interfaceof(φ)∧ Γ = wfinv(φ) ∧ Δ = procbodies(φ) ⇒ ∀ cfg cfg’. ψ;Γ ⊢ cfg well formed ⇒ Δ ⊢ cfg → cfg’ ⇒ ψ;Γ ⊢ cfg’ well formed
A program has undefined behavior if some bad action (e.g. writing outside a buffer) can happen for some inputs. To a first approximation, the compiler is free to produce a target program behaving arbitrarily for those inputs.
Note that this is different than saying that an undefined behavior causes the program to go to an arbitrary high-level state:
- We are talking about low-level attacks, and for such attacks (without additional protection at least) an undefined compiled program will transition to states in that have no high-level equivalent whatsoever! So high-level configurations are not good enough for expressing what happens after the bad action.
- Since compiler optimizations assume defined behavior, the compiler can cause the bad action to happen earlier, later, or not at all.
This is also different from saying that the compiler is free to produce an arbitrary output if the source program has (any) undefined behavior. For inputs for which the bad action cannot happen the compiler has to produce correctly behaving code, even if the program can cause a bad action for other inputs.
Without good ways of (1) knowing/specifying on which inputs a program/component is defined and on which ones it is not and (2) restricting the inputs a program/component can take to those that make it be defined, we go with the following coarse notion of undefinedness.
Definition: A well-formed program φ is undefined if I(φ) gets stuck.
Definition: A well-formed program φ is defined if it is not undefined.
Starting point: RISC register machine from Oakland 2015
- the instructions from the basic machine with two additions: Call C P and Return
Separate memories
- Each isolated component has its own infinite memory and memory addressing is relative to the current component
Global protected call stack
- only deals with cross-component calls and returns
- on a micro-policy machine this would be implemented using return capabilities
- for SFI/XFI machine this would be implemented via a shadow call stack
The memory of each component contains:
- code (stored instructions; can mount code injection and ROP attacks)
- a local stack
- arrays (statically allocated)
We know the external entry points for each component, list of addresses
no protection against overflows affecting the offending component’s memory
- in particular we can mount code injection and ROP attacks
- but only to the current component
- the writes to other component’s memory are prevented (by design)
this abstract machine can later (i.e. future work) be implemented in various ways, including:
- process-level sandboxing (different address spaces)
- software-fault isolation (same address space)
- micro-policies (same address space)
- multi-PMA systems (same address space)
Instr ::= Nop | Const i → r | Mov r₁ → r₂ | BinOp r₁ ⊗ r₂ → r₃ | Load *r₁ → r₂ | Store *r₁ ← r₂ | Jal r | – for internal calls Jump r | – for internal returns Call C P | – for external calls (to designated entry points) Return | – for external returns (to top of call stack) Bnz r i | Halt
p ::= (ψ, mem, E) – low-level program
ψ — defined in the high-level
E[C] – the list of external entry points of component C (internal calls are done via Jal and not monitored)
ψ; E ⊢ ρ → ρ’
ρ ::= (C,σ,mem,reg,pc)
ψ — high-level program interface E – external entry points C – the current component σ – protected stack, each entry has the form (C,i)
- we return to component C at (local) address i
mem[C,i] – the value of memory address i in component C reg and pc are as in the basic machine from the Oakland 2015 paper
mem[C,pc] = i decode i = Nop ———————————————————————————————————————————— :: S_Nop ψ; E ⊢ (C,σ,mem,reg,pc) → (C,σ,mem,reg,pc+1)
mem[C,pc] = i decode i = Const i’ → r reg’ = reg[r ↦ i’] ————————————————————————————————————————————— :: S_Const ψ; E ⊢ (C,σ,mem,reg,pc) → (C,σ,mem,reg’,pc+1)
mem[C,pc] = i decode i = Mov r₁ → r₂ reg’ = reg[r₂ ↦ reg[r₁]] ————————————————————————————————————————————— :: S_Mov ψ; E ⊢ (C,σ,mem,reg,pc) → (C,σ,mem,reg’,pc+1)
mem[C,pc] = i decode i = BinOp r₁ ⊗ r₂ → r₃ reg’ = reg[r₃ ↦ reg[r₁] ⊗ reg[r₂]] ————————————————————————————————————————————— :: S_BinOp ψ; E ⊢ (C,σ,mem,reg,pc) → (C,σ,mem,reg’,pc+1)
mem[C,pc] = i decode i = Load *r₁ → r₂ reg[r₁] = i₁ reg’ = reg[r₂ ↦ mem[C,i₁]] ————————————————————————————————————————————— :: S_Load ψ; E ⊢ (C,σ,mem,reg,pc) → (C,σ,mem,reg’,pc+1)
mem[C,pc] = i decode i = Store *r₁ ← r₂ reg[r₁] = i₁ reg[r₂] = i₂ mem’ = mem[C,i₁ ↦ i₂] ————————————————————————————————————————————— :: S_Store ψ; E ⊢ (C,σ,mem,reg,pc) → (C,σ,mem’,reg,pc+1)
mem[C,pc] = i decode i = Jal r reg[r] = i’ reg’ = reg[rᵣₐ → pc + 1] ——————————————————————————————————————————— :: S_Jal ψ; E ⊢ (C,σ,mem,reg,pc) → (C,σ,mem,reg’,i’)
mem[C,pc] = i decode i = Call C’ P’ C’.P’ ∈ ψ[C].import ∨ C’ = C – checking interface σ’ = (C,pc+1) :: σ – updating call stack ——————————————————————————————————————————————————— :: S_Call ψ; E ⊢ (C,σ,mem,reg,pc) → (C’,σ’,mem,reg,E[C’][P’])
mem[C,pc] = i decode i = Jump r reg[r] = i’ —————————————————————————————————————————— :: S_Jump ψ; E ⊢ (C,σ,mem,reg,pc) → (C,σ,mem,reg,i’)
mem[C,pc] = i decode i = Return σ = (C’,i’) :: σ’ – return address from protected stack ———————————————————————————————————————————— :: S_Return ψ; E ⊢ (C,σ,mem,reg,pc) → (C’,σ’,mem,reg,i’)
mem[C,pc] = i decode i = Bnz r i’ reg[r] ≠ 0 ————————————————————————————————————————————— :: S_BnzNZ ψ; E ⊢ (C,σ,mem,reg,pc) → (C,σ,mem,reg,pc+i’)
mem[C,pc] = i decode i = Bnz r i’ reg[r] = 0 ———————————————————————————————————————————— :: S_BnzZ ψ; E ⊢ (C,σ,mem,reg,pc) → (C,σ,mem,reg,pc+1)
Note: this semantics can be used to reduce partial programs.
I(ψ, mem, E) := (main,[],mem,reg₀,E[main][0]) where reg₀ is a register file with all registers set to 0
∀ ψ E ρ ρ₁ ρ₂. ψ; E ⊢ ρ → ρ₁ ∧ ψ; E ⊢ ρ → ρ₂ ⇒ ρ₁ = ρ₂
Here are all stuck states:
- instruction decoding errors (decode is probably a partial function)
- mem[C] could fail if accessing a non-existent component?
- this won’t happen if the current component C and all comps(ψ[C].import) are in dom(C) to start with; this particular thing is something one can check statically, but whatever
- access control check failure on calls (C’.P’ ∈ ψ[C].import in S_Call)
- return with empty call stack (σ = (C’,i’) : σ’ in S_Return)
- trying to execute the Halt instruction also leads to a stuck state the semantics above
They all correspond to easily detectable errors
- they could lead to error states if needed
s ::= (ψ, — whole program interface {C₀,…,Cₙ}) — names of the components that the attacker gets
⊢ ψ well formed {C₀,…,Cₙ} ⊆ dom(ψ) ———————————————————————————— (ψ, {C₀,…,Cₙ}) well formed
P, Q, A ::= φ
(no syntactic distinction between partial and whole programs)
ψ ⊢ φ well formed comps(φ) = {C₀,…,Cₙ} —————————————————————— φ ∈• (ψ, {C₀,…,Cₙ})
ψ ⊢ φ well formed dom(φ) = comps(ψ)∖{C₀,…,Cₙ} ————————————————————————————— φ ∈∘ (ψ, {C₀,…,Cₙ})
φ_A[φ_P] ::= φ_A ⊎ φ_P
∀ A P s. s well formed ∧ A ∈∘ s ∧ P ∈• s ⇒ A[P] whole well formed
p, q, a ::= (ψ, mem, E)
(no syntactic distinction between partial and whole programs)
∀ ι ∈ ψₚ, ι ⊆ ψ[ι.name] dom(E) ⊆ dom(mem) = comps(ψₚ) = {C₀,…,Cₙ} ——————————————————————————————————————————— (ψₚ, mem, E) ∈• (ψ, {C₀,…,Cₙ})
∀ ι ∈ ψₐ, ι ⊆ ψ[ι.name] dom(E) ⊆ dom(mem) = comps(ψₐ) = comps(ψ)∖{C₀,…,Cₙ} ———————————————————————————————————————————————————— (ψₐ, mem, E) ∈∘ (ψ, {C₀,…,Cₙ})
(ψₐ, memₐ, Eₐ)[(ψₚ, memₚ, Eₚ)] ::= (ψₐ ⊎ ψₚ, memₐ ⊎ memₚ, Eₐ ⊎ Eₚ)
A partial program P ∈• s is fully defined wrt. contexts of shape ∘s if there exists no context A ∈∘ s so that I(A[P]) →* cfg, cfg is a stuck state (i.e. cfg not final and cfg does not step), and the current component in cfg is in comps(P).
A context A ∈∘ s is fully defined wrt. programs of shape •s if there exists no program P ∈• s so that I(A[P]) →* cfg, cfg is a stuck state (i.e. cfg not final and cfg does not step), and the current component in cfg is in comps(A).
We want to make sure that the following intuitive properties are satisfied:
(1) ∀ s, ∀ P ∈• s, P fully defined wrt. contexts of shape ∘s ⇔ (∀ A ∈∘ s, A fully defined wrt. programs of shape •s ⇒ A[P] defined)
(2) ∀ s, ∀ A ∈∘ s, A fully defined wrt. programs of shape •s ⇔ (∀ P ∈• s, P fully defined wrt. contexts of shape ∘s ⇒ A[P] defined)
∀ s, ∀ P ∈• s, ∀ A ∈∘ s, A fully defined wrt. programs of shape •s ⇒ P fully defined wrt. contexts of shape ∘s ⇒ A[P] defined
Proof:
Let P A. Assume A[P] is undefined, i.e. I(A[P]) →* cfg where cfg is a stuck state. The current component in cfg must be in either A or P; however, by full definedness, neither case is possible. Contradiction.
∀ s, ∀ P ∈• s, ∀ A ∈∘ s, I(A[P]) →* cfg ∧ cfg stuck ∧ current_component cfg ∈ comps(P) ⇒ ∃ A’ cfg’. A’ ∈∘ s ∧ A’ fully defined wrt. programs of shape •s ∧ I(A’[P]) →* cfg’ ∧ cfg’ stuck
∀ s, ∀ P ∈• s, ∀ A ∈∘ s, I(A[P]) →* cfg ∧ cfg stuck ∧ current_component cfg ∈ comps(A) ⇒ ∃ P’ cfg’. P’ ∈• s ∧ P’ fully defined wrt. contexts of shape ∘s ∧ I(A[P’]) →* cfg’ ∧ cfg’ stuck
Proof sketch for first property (second is symmetric):
Note: the simulation relation proposed below doesn’t work. We provide the sketch for intuition only, but it cannot prove the property as is.
We defined a mapping FD(A) that takes and arbirtrary context A to a fully defined context and a statement “φ ⊢ cfg rewrites to cfg’” that satisfy the simulation diagram illustrated by the second property below:
∀ s, ∀ A ∈∘ s, FD(A) ∈∘ s ∧ FD(A) fully defined wrt. programs of shape •s
∀ s, ∀ A ∈∘ s, ∀ P ∈• s, A ⊢ I(P[A]) rewrites to I(P[FD(A)]) ∧ let ψ = interfaceof(P[A]) in let Γ = wfinv(P[A]) in let Δ = procbodies(P[A]) in let Γ_FD = wfinv(P[FD(A)]) in let Δ_FD = procbodies(P[FD(A)]) in ∀ cfg₀ cfg₁, ψ; Γ ⊢ cfg₀ well formed ⇒ Δ ⊢ cfg₀ → cfg’₀ ⇒ A ⊢ cfg₀ rewrites to cfg₁ ⇒ ∃ cfg’₁. A ⊢ cfg’₀ rewrites to cfg’₁ ∧ Δ_FD ⊢ cfg₁ →* cfg’₁
FD(φ) ::= {FD(κ) | κ ∈ φ}
FD(κ) ::= κ’ such that κ’.name = κ’.name κ’.bnum = κ.bnum + 1 κ’.bufs[b] = κ.bufs[b] for all b in 0 .. κ.bnum-1 κ’.bufs[κ.bnum] = [ 0 ] κ’.pnum = κ.pnum κ’.export = κ.export κ’.procs[P] = FD_κ(κ.procs[P]) for all P in 0 .. κ.pnum - 1
FD_κ(i) ::= i FD_κ(e₁ ⊗ e₂) ::= FD_κ(e₁) ⊗ FD_κ(e₂) FD_κ(if e then e₁ else e₂) ::= if FD_κ(e) then FD_κ(e₁) else FD_κ(e₂) FD_κ(b[e]) ::= let b’ = κ.bnum in let i = κ.blens[b] in b’[0] := make_fd e; if b’[0] < i then b[b’[0]] else 0 FD_κ(b[e] := e’) ::= let b’ = κ.bnum in let i = κ.blens[b] in b’[0] := make_fd e; if b’[0] < i then b[b’[0]] := e’ else 0 FD_κ(C.P(e)) ::= C.P(FD_κ(e)) FD_κ(exit) ::= exit
(C₀, s₀, σ₀, K₀, e₀) well formed (C₀, s₁, σ₁, K₁, e₁) well formed dom(s₀) = dom(s₁) (in terms of components) ∀ C ∈ dom(s₀)∖dom(φ), s₁[C] = s₀[C] ∀ C ∈ dom(φ), length s₁[C] = 1 + length s₀[C] ∀ C ∈ dom(φ), ∀ b in 0 .. length s₀[C] - 1, s₁[C,b] = s₀[C,b] C₀ ∈ dom(φ) ⇒ FDφ[C](K₀) = K₁ ∧ FDφ[C](e₀) = e₁ C₀ ∉ dom(φ) ⇒ K₀ = K₁ ∧ e₀ = e₁ φ ⊢ σ₀ rewrites to σ₁ ———————————————–——————————————————————————–—————————————– φ ⊢ (C₀, s₀, σ₀, K₀, e₀) rewrites to (C₀, s₁, σ₁, K₁, e₁)
————–———————————————– φ ⊢ [] rewrites to []
R σ₀ σ₁ C₀ ∈ dom(φ) ⇒ FDφ[C](K₀) = K₁ C₀ ∉ dom(φ) ⇒ K₀ = K₁ ——————–———————————————————————————————————–———–—————————– φ ⊢ ((C₀, i₀, K₀) :: σ₀) rewrites to ((C₀, i₀, K₁) :: σ₁)
∀ s, ∀ P ∈• s, (∀ A ∈∘ s, A fully defined wrt. programs of shape •s ⇒ A[P] defined) ⇒ P fully defined wrt contexts of shape ∘s
∀ s, ∀ A ∈∘ s, (∀ P ∈• s, P fully defined wrt. contexts of shape ∘s ⇒ A[P] defined) ⇒ A fully defined wrt programs of shape •s
Proof of first property (second is symmetric):
Let s P such that (∀ A ∈∘ s, A fully defined wrt. programs of shape •s ⇒ A[P] defined) and let us show that P fully defined wrt contexts of shape ∘s. Take an arbitrary context A ∈∘ s. Suppose by contradiction that for some cfg, I(A[P]) →* cfg ∧ cfg stuck ∧ current_component cfg ∈ comps(P). We can apply the previous lemma to get a context A’ ∈∘ s such that A’ fully defined wrt. programs of shape •s ∧ ∃ cfg’. I(A’[P]) →* cfg’ ∧ cfg’ stuck, so, A’ fully defined wrt. programs of shape •s ∧ A’[P] undefined, which contradicts the assumption on P. Contradiction.
Non-optimizing, naive compiler.
This compiler explicitly clears all registers before each cross-component call.
- we need to clear the registers our compiler uses in order to prevent accidentally leaking information
- we need to also clear the registers our compiler does not use in order to prevent attacker components that cannot communicate directly from using these registers as a side-channel
BUFADDR(κ,b): map from buffer identifiers to addresses INTERNALENTRY(κ,P): map from procedures to internal entry points (an address in that procedure’s component) STACKBASE(κ): Base address of component C’s stack
The concrete memory layout is given below:
BUFADDR(κ,0) = 0 BUFADDR(κ,b) when b < κ.bnum = BUFADDR(κ,b-1) + length(κ.bufs[b-1])
EXTERNALENTRY(κ,0) = BUFADDR(κ, κ.bnum-1) + length(κ.bufs[κ.bnum-1]) EXTERNALENTRY(κ,P) when P < κ.pnum = EXTERNALENTRY(κ,P-1) + length(code) where code = (κ, P - 1)↓
Note: length(code((κ, P)↓)) should be computed without actually compiling the code. The length of the code does not depend on the values provided by macro functions. The actual code however does, and an attempt to compute it here would lead to an infinite recursion.
INTERNALENTRY(κ,P) when P < κ.pnum = EXTERNALENTRY(κ,P) + 3
STACKBASE(κ) = EXTERNALENTRY(κ,κ.pnum - 1) + length(code) + 1 where code = (κ, κ.pnum-1)↓
The memory cell at location STACKBASE(κ) - 1 is used to (re)store the stack pointer when switching components.
Assuming dom(reg) \ {r_com} = {r₀,…,rₙ}.
CLEARREG ::= Const 0 → r₀; … Const 0 → rₙ
The environment is saved on cross-compartment calls and returns and restored when getting back control.
STOREENV(κ,r) ::= store current stack pointer value Const (STACKBASE(κ) - 1) → r; (register r gets overwritten in the process) Store *r ← rₛₚ
RESTOREENV(κ) ::= restore stack pointer value, set rₒₙₑ Const 1 → rₒₙₑ; Const (STACKBASE(κ) - 1) → rₛₚ; Load *rₛₚ → rₛₚ
LOADARG(κ → r) ::= Const BUFADDR(κ,0) → r; Load *r → r
STOREARG(κ ← r, r’) ::= Const BUFADDR(κ,0) → r’; Store *r’ ← r
PUSH(r) ::= add the value in register r on top of the local stack BinOp rₛₚ + rₒₙₑ → rₛₚ; Store *rₛₚ ← r
POP(r) ::= remove top value on the stack and put it into register r Load *rₛₚ → r; BinOp rₛₚ - rₒₙₑ → rₛₚ
When the environment is set it is the case that:
- rₒₙₑ holds value 1;
- rₛₚ holds a pointer to the current top of the local stack;
- rₐᵤₓ₂ holds 0 if the call originated from the same component, 1 otherwise.
Register rₐᵤₓ₁ is used to store temporary results.
Expression compilation e↓ produces code which corresponds to reducing e and putting the resulting value in r_com. If e goes to an infinite loop or terminates the program, then so will e↓.
The stack is used both to store intermediate results and to spill registers. Stack usage by compiled procedures is such that at return time (when hitting a Jump or Return instruction), the local stack pointer is exactly at the position where it was at the beginning of the call: every time the stack pointer increments by one (PUSH), dual code will decrement it by one (POP).
lext — external call entry point lint — internal call entry point
(κ,P)↓ ::=
lext: Const 1 → rₐᵤₓ₂; RESTOREENV(κ); Bnz rₒₙₑ lmain; – always branches lint: Const 0 → rₐᵤₓ₂; PUSH(rᵣₐ); lmain: STOREARG(κ ← r_com, rₐᵤₓ₁); – store call argument in memory (κ,κ.procs[P])↓; – compute result into r_com Bnz rₐᵤₓ₂ lret; POP(rᵣₐ); Jump rᵣₐ; lret: STOREENV(κ,rₐᵤₓ₁); CLEARREG; Return
(κ,i)↓ ::= Const i → r_com
(κ,e₁⊗e₂)↓ when ⊗ ≠ (;) ::= (κ,e₁)↓; PUSH(r_com); (κ,e₂)↓; POP(rₐᵤₓ₁); BinOp rₐᵤₓ₁ ⊗ r_com → r_com
(κ,e₁;e₂)↓ ::= – just an optimization (κ,e₁)↓; (κ,e₂)↓
(κ,if e then e₁ else e₂)↓ ::= (κ,e)↓; Bnz r_com lnz; (κ,e₂)↓; Bnz rₒₙₑ lend; — will always branch lnz: (κ,e₁)↓; lend: Nop
(κ,b[e])↓ ::= (κ,e)↓; Const BUFADDR(κ,b) → rₐᵤₓ₁; Binop rₐᵤₓ₁ + r_com → rₐᵤₓ₁; Load *rₐᵤₓ₁ → r_com
(κ,b[e₁] := e₂)↓ ::= (κ,e₁)↓; Const BUFADDR(κ,b) → rₐᵤₓ₁; Binop rₐᵤₓ₁ + r_com → rₐᵤₓ₁; PUSH(rₐᵤₓ₁); (κ,e₂)↓; POP(rₐᵤₓ₁); Store *rₐᵤₓ₁ ← r_com
(κ,C’.P’(e))↓ when C’ ≠ κ.name ::= (κ,e)↓; PUSH(rₐᵤₓ₂); LOADARG(κ → rₐᵤₓ₁); PUSH(rₐᵤₓ₁); STOREENV(κ,rₐᵤₓ₁); CLEARREG; Call C’ P’; RESTOREENV(κ); POP(rₐᵤₓ₁); STOREARG(κ ← rₐᵤₓ₁, rₐᵤₓ₂); POP(rₐᵤₓ₂)
(κ,C.P(e))↓ when C = κ.name ::= – local calls optimization (κ,e)↓; PUSH(rₐᵤₓ₂); LOADARG(κ → rₐᵤₓ₁); PUSH(rₐᵤₓ₁); Const INTERNALENTRY(κ,P) → rₐᵤₓ₁; Jal rₐᵤₓ₁; POP(rₐᵤₓ₁); STOREARG(κ ← rₐᵤₓ₁, rₐᵤₓ₂); POP(rₐᵤₓ₂)
(κ,exit)↓ ::= Halt
φ↓ ::= (ψ₁ ⊎ … ⊎ ψₙ, mem₁ ⊎ … ⊎ memₙ, E₁ ⊎ … ⊎ Eₙ) where φ = {κ₁, …, κₙ} (ψᵢ, memᵢ, Eᵢ) = κᵢ↓
κ↓ = (ψ, mem, E) where ψ = {interfaceof(κ)} mem[κ.name] = κ.bufs[0] ++ … ++ κ.bufs[κ.bnum - 1] ++ (κ,0)↓ ++ … ++ (κ,κ.pnum - 1)↓ ++ [STACKBASE(̨κ)] ++ [0, …] E[̨(κ.name).0] = EXTERNALENTRY(κ,0) … E[̨(κ.name).(κ.pnum-1)] = EXTERNALENTRY(κ,κ.pnum-1)
φ terminates ≜ let Δ = procbodies(φ) in ∃cfg. Δ ⊢ I(φ) →* cfg ∧ Δ ⊢ cfg ↛
φ diverges ≜ let Δ = procbodies(φ) in ∀ cfg. Δ ⊢ I(φ) →* cfg ⇒ ∃ cfg’. Δ ⊢ cfg → cfg’
(ψ,mem,E) terminates ≜ ∃ ρ. ψ; E ⊢ I(ψ,mem,E) →* ρ ∧ ψ; E ⊢ ρ ↛
(ψ,mem,E) diverges ≜ ∀ ρ. ψ; E ⊢ I(ψ,mem,E) →* ρ ⇒ ∃ ρ’. ψ; E ⊢ ρ → ρ’
∀ φ. φ whole well formed ∧ φ defined ⇒ (φ↓ terminates ⇔ φ terminates)
∀ φ. φ whole well formed ∧ φ defined ⇒ (φ↓ diverges ⇔ φ diverges)
∀ s P. s well formed ∧ P ∈• s ⇒ P↓ ∈• s
∀ s A. s well formed ∧ A ∈∘ s ⇒ A↓ ∈∘ s
∀ s A P. A well formed ∧ A fully defined ∧ A ⊢ s ⇒ P well formed ∧ P fully defined ∧ P ⊢ₙ s ⇒ (A[P])↓ ~L A↓[P↓]
We define a labeled reduction of the form:
α ψ; E ⊢• θ → θ’
E — external entry points for the program components only ψ – interfaces for all components (both player and opponent) both defined as in the low-level semantics
Note: the set of program components is dom(E) context components is dom(ψ)∖dom(E)
α ::= action and origin
| Eα external action and origin |
| Iα internal action and origin |
Eα ::= external action and origin
| ea ! external action performed by the program |
| ea ? external action performed by the context |
ea, γ ::= cross-boundary action
| C.P(reg) cross-boundary call |
| Ret reg cross-boundary return |
| ✓ termination |
Note that calls and return actions record the whole register file, not just the value in register r_com, since there is no a priori guarantee that components clean their other registers. The compiler will add code for this, but that will make no difference for compromised components.
Iα ::= internal action and origin
| ia + internal action taken by the program |
| ia - internal action taken by the context |
ia ::= internal action
| τ silent step |
| C.P(/) internal call |
| Ret / internal return |
The notation / is used to for partial knowledge: one could expect a call argument or a return value to stand in place of /, but we actually don’t know (nor care about) what the actual call argument or value is for an internal action.
In a given state θ, control is either held by the program (Pθ) or by the context (Aθ). Internal steps always preserve control ownership, while cross-boundary calls and returns always transfer control (either from the program to the context, or from the context to the program).
θ ::= partial view on machine state
| Pθ the program has control |
| Aθ the context has control |
| EXITED |
Pθ ::= ( C, current component PΣ, view on global protected call stack mem, program’s view on memory reg, register file pc program counter )
Aθ ::= ( C, current component AΣ, view on global protected call stack mem, program’s view on memory /, register file unknown to the program / program counter unknown to the program )
PΣ ::= partial view on the call stack when the program has control
| σ :: program internal call frames AΣ remainder of the global stack| σ |
AΣ ::= partial view on the call stack when the context has control
| Aσ partial view on context internal call frames :: PΣ remainder of the global stack| Aσ |
Aσ ::= context internal call frames: only remember components
| [] |
| (C, /) :: Aσ |
(σ is defined as above, in the low-level semantics)
Intuition for PΣ and AΣ: a list of elements of alternating types (Aσ and σ)
Program starts computation and program has control: σ :: (Aσ :: (… :: (Aσ₁ :: (σ₁ :: (Aσ₀ :: σ₀))) …))
Program starts computation and context has control: Aσ :: (σ :: (… :: (Aσ₁ :: (σ₁ :: (Aσ₀ :: σ₀))) …))
Context starts computation and program has control: σ :: (Aσ :: (… :: (Aσ₁ :: (σ₁ :: Aσ₀)) …))
Context starts computation and context has control: Aσ :: (σ :: (Aσ :: (… :: (Aσ₁ :: (σ₁ :: Aσ₀)) …)))
Top : PΣ → σ Top(σ) ≜ σ Top(σ :: AΣ) ≜ σ
Top : AΣ → Aσ Top(Aσ) ≜ Aσ Top(Aσ :: PΣ) ≜ Aσ
SetTop : (PΣ, σ) → PΣ SetTop(σ, σ’) ≜ σ’ SetTop(σ :: AΣ, σ’) ≜ σ’ :: AΣ
SetTop : (AΣ, Aσ) → AΣ SetTop(Aσ, Aσ’) ≜ Aσ’ SetTop(Aσ :: AΣ, Aσ’) ≜ Aσ’ :: AΣ
We use the standard semantics with a (more) partial E. This gets stuck when calling or returning to the context (which is not in E), but then other rules will apply (6 and 7).
Top(PΣ) = σ PΣ’ = SetTop(PΣ, σ’) ψ; E ⊢ (C,σ,mem,reg,pc) → (C’,σ’,mem’,reg’,pc’) ————————————————————————————————————————————————— T_CallRetTau+ action(C,σ,mem,reg,pc) ψ; E ⊢• (C,PΣ,mem,reg,pc) → (C’,PΣ’,mem’,reg’,pc’)
action(C,σ,mem,reg,pc) = match decode(mem[C,pc]) with Call C₀ P₀ -> C₀.P₀(/) + Return -> Ret / + _ -> τ +
———————————————————————————————————————— T_Tau- τ - ψ; E ⊢• (C,AΣ,mem,/,/) → (C,AΣ,mem,/,/)
C’.P’ ∈ ψ[C].import ∨ C’ = C – check interface C’ ∉ dom(E) — call target in context Top(AΣ) = Aσ AΣ’ = SetTop(AΣ, (C,/)::Aσ) ————————————————————————————————————————————— T_Call- C’.P’() - ψ; E ⊢• (C,AΣ,mem,,/) → (C’,AΣ’,mem,/,/)
(C’,/)::σ = Top(AΣ) AΣ’ = SetTop(AΣ,σ) —————————————————————————————————————————— T_Ret- Ret / - ψ; E ⊢• (C,AΣ,mem,/,/) → (C’,AΣ’,mem,/,/)
C’.P’ ∈ ψ[C].import – check interface C’ ∈ dom(E) – call target in program Top(AΣ) = Aσ AΣ’ = SetTop(AΣ, (C,/)::Aσ) ——————————————————————————————————————————————————————— T_Call? C’.P’(reg) ? ψ; E ⊢• (C,AΣ,mem,/,/) → (C’,[]::AΣ’,mem,reg,E[C’][P’])
Top(PΣ) = (C’,pc)::σ PΣ’ = SetTop(PΣ,σ) ———————————————————————————————————————————————— T_Ret? Ret reg ? ψ; E ⊢• (C,[]::PΣ,mem,/,/) → (C’,PΣ’,mem,reg,pc)
mem[C,pc] = i decode i = Call C’ P’ C’.P’ ∈ ψ[C].import – check interface C’ ∉ dom(E) – call target in context Top(PΣ) = σ PΣ’ = SetTop(PΣ, (C,pc+1)::σ) ———————————————————————————————————————————————— T_Call! C’.P’(reg) ! ψ; E ⊢• (C,PΣ,mem,reg,pc) → (C’,[]::PΣ’,mem,/,/)
mem[C,pc] = i decode i = Return Top(AΣ) = (C’,/)::Aσ AΣ’ = SetTop(AΣ,Aσ) ———————————————————————————————————————————————— T_Ret! Ret reg ! ψ; E ⊢• (C,[]::AΣ,mem,reg,pc) → (C’,AΣ’,mem,/,/)
——————————————————————————————— T_Exit? ✓? ψ; E ⊢• (C,AΣ,mem,/,/) → EXITED
α ∀ α ≠ ✓!. ψ; E ⊢• (C,PΣ,mem,reg,pc) ↛ ————————————————————————————————————— T_Exit! ✓! ψ; E ⊢• (C,PΣ,mem,reg,pc) → EXITED
Initial states have the same definition for partial program players and context players:
I(ψ,mem,E) – initial state I(ψ,mem,E) when main ∈ dom(E) ≜ (C, [], mem, reg₀, E[main][0]) – player starts computation I(ψ,mem,E) when main ∉ dom(E) ≜ (C, [], mem, /, /) – opponent starts computation
t ≜ a word over alphabet Eα (as defined above).
ε is the empty word.
————————————— T_Refl ε ψ; E ⊢• θ ⇒ θ
Iα ψ; E ⊢• θ → θ’ —————————————— T_Internal ε ψ; E ⊢• θ ⇒ θ’
Eα ψ; E ⊢• θ → θ’ —————————————— T_Cross Eα ψ; E ⊢• θ ⇒ θ’
t ψ; E ⊢• θ ⇒ θ’ u ψ; E ⊢• θ’ ⇒ θ” ———————————————— T_Trans t.u ψ; E ⊢• θ ⇒ θ”
Intuition: permute context and program in all actions.
(γ ?)⁻¹ ≜ γ ! (γ !)⁻¹ ≜ γ ?
ε⁻¹ ≜ ε Eα :: t ≜ Eα⁻¹ :: t⁻¹
Due to the symmetry between programs and contexts, we can define context traces via program traces. This amounts to using the exact same rules as the one for programs, while permuting the roles of the program and the context: we exchange “?” for “!” and “!” for “?”.
t⁻¹ ψ; E ⊢• θ ⇒ θ’ —————————————— t ψ; E ⊢∘ θ ⇒ θ’
Traces_•s(p) – the set of traces that a program has t Traces_•s(p) = {t | ∃θ. ψ; Eₚ ⊢• I(p) ⇒ θ} where p = (ψₚ,memₚ,Eₚ) s = (ψ,{C₀,…,Cₙ})
Traces_∘s(a) – the set of traces that a context has t Traces_∘s(a) = {t | ∃θ. ψ; Eₐ ⊢∘ I(a) ⇒ θ} where a = (ψₐ,memₐ,Eₐ) s = (ψ,{C₀,…,Cₙ})
T ≜ a word over alphabet α – generalized traces that include internal actions
erase(T) – erase internal actions in a generalized trace to get a trace t erase(ε) ≜ ε erase(Iα :: t) ≜ erase(t) erase(Eα :: t) ≜ Eα :: erase(t)
(ia -)⁻¹ ≜ ia + (ia +)⁻¹ ≜ ia -
ε⁻¹ ≜ ε Iα :: T ≜ Iα⁻¹ :: T⁻¹ Eα :: T ≜ Eα⁻¹ :: T⁻¹
Intuition: the same trace, where the context cleans all his registers.
ζ(γ) – clean registers in an external action ζ(C.P(reg)) ≜ C.P(reg[r←0,r≠r_com]) ζ(Ret reg) ≜ Ret reg[r←0,r≠r_com] ζ(✓) ≜ ✓
ζ∘(Eα) – clean registers in context actions only ζ∘(γ !) ≜ γ ! ζ∘(γ ?) ≜ ζ(γ) ?
ζ∘(t) — clean registers in context actions of a trace ζ∘(ε) ≜ ε ζ∘(Eα :: t) ≜ ζ∘(Eα) :: ζ∘(t)
ζ∘(T) — internal actions don’t mention register values anyway ζ∘(ε) ≜ ε ζ∘(Eα :: T) ≜ ζ∘(Eα) :: ζ∘(T) ζ∘(Iα :: T) ≜ Iα :: ζ∘(T)
ζ•(Eα) – clean registers in program actions only ζ•(γ !) ≜ ζ(γ) ! ζ•(γ ?) ≜ γ ?
ζ•(t) — clean registers in program actions of a trace ζ•(ε) ≜ ε ζ•(Eα :: t) ≜ ζ•(Eα) :: ζ•(t)
ζ•(T) ζ•(ε) ≜ ε ζ•(Eα :: T) ≜ ζ•(Eα) :: ζ•(T) ζ•(Iα :: T) ≜ Iα :: ζ•(T)
C ∈ dom(E) dom(mem) = dom(E) E ⊢ PΣ well formed Pθ = (C, PΣ, mem, reg, pc) —————————————————————————— E ⊢ Pθ well formed
C ∉ dom(E) dom(mem) = dom(E) E ⊢ AΣ well formed Aθ = (C, AΣ, mem, /, /) —————————————————————————— E ⊢ Aθ well formed
PΣ = σ E ⊢ σ well formed —————————————————————————— E ⊢ PΣ well formed
PΣ = σ::AΣ Top(AΣ) = _ :: _ E ⊢ σ well formed E ⊢ AΣ well formed —————————————————————————— E ⊢ PΣ well formed
AΣ = Aσ E ⊢ Aσ well formed —————————————————————————— E ⊢ AΣ well formed
AΣ = Aσ::PΣ Top(PΣ) = _ :: _ E ⊢ Aσ well formed E ⊢ PΣ well formed —————————————————————————— E ⊢ AΣ well formed
σ = [] ————————————————— E ⊢ σ well formed
σ = (C, pc) :: σ’ C ∈ dom(E) E ⊢ σ’ well formed —————————————————— E ⊢ σ well formed
Aσ = [] ————————————————— E ⊢ Aσ well formed
Aσ = (C, /) :: Aσ’ C ∉ dom(E) E ⊢ Aσ’ well formed —————————————————— E ⊢ Aσ well formed
——————— [] ⊆ []
Aσ ⊆ σ ————————————————————————— (C, /) :: Aσ ⊆ (C, i) :: σ
Aσ ⊆ σ —————————————— mergeable σ Aσ
Aσ ⊆ σ mergeable PΣ AΣ —————————————————————————— mergeable σ::AΣ Aσ::PΣ
merge PΣ AΣ ≜ match PΣ, AΣ with σ, _ → σ σ::AΣ, _::PΣ → σ ++ merge PΣ AΣ
mergeable PΣ AΣ dom(memₚ) ∩ dom(memₐ) = ∅ —————————————————————————————————————————————————————— mergeable (C, PΣ, memₚ, reg, pc) (C, AΣ, memₐ, /, /)
merge Pθ Aθ ≜ match Pθ, Aθ with (C, PΣ, memₚ, reg, pc), (_, AΣ, memₐ, /, /) → (C, merge PΣ AΣ, memₚ ⊎ memₐ, reg, pc)
For all properties below, the second variant (about the context) follows from the first variant (about the program).
∀ s t u v γ₀ γ₁ p. s well formed ∧ p ∈• s ∧ t ∈ Traces_∘s(p) ⇒ (t = u.γ₀?.Eα.v ⇒ ∃ γ₁. Eα = γ₁!) ∧ (t = u.γ₀!.Eα.v ⇒ ∃ γ₁. Eα = γ₁?)
∀ s t u v γ₀ γ₁ a. s well formed ∧ a ∈∘ s ∧ t ∈ Traces_•s(a) ⇒ (t = u.γ₀?.Eα.v ⇒ ∃ γ₁. Eα = γ₁!) ∧ (t = u.γ₀!.Eα.v ⇒ ∃ γ₁. Eα = γ₁?)
∀ s t u p. s well formed ∧ p ∈• s ∧ t.u ∈ Traces_∘s(p) ⇒ t ∈ Traces_∘s(p)
∀ s t u a. s well formed ∧ a ∈∘ s ∧ t.u ∈ Traces_•s(a) ⇒ t ∈ Traces_•s(a)
∀ s a p t u γ. s well formed ⇒ a well formed ∧ a ∈∘ s ⇒ p well formed ∧ p ∈• s ⇒ t ∈ Traces_∘s(p) ∧ t.γ? ∈ Traces_•s(a) ⇒ t.γ? ∈ Traces_∘s(p)
∀ s a p t u γ. s well formed ⇒ a well formed ∧ a ∈∘ s ⇒ p well formed ∧ p ∈• s ⇒ t ∈ Traces_•s(a) ∧ t.γ! ∈ Traces_∘s(p) ⇒ t.γ! ∈ Traces_•s(a)
∀ s P t. s well formed ∧ P ∈• s ⇒ P fully defined wrt. contexts of shape ∘s ⇒ t ∈ Traces_∘s(P↓) ⇒ t = ζ•(t)
∀ s A t. s well formed ∧ A ∈∘ s ⇒ A fully defined wrt. programs of shape •s ⇒ t ∈ Traces_•s(A↓) ⇒ t = ζ∘(t)
Intuition:
The code of fully defined players never changes (Stores are limited to buffers). Except for r_com, compiled players always clean their registers before performing a call or a return. As a consequence, in their traces, except for r_com, all registers hold value 0 upon communication originating from the player.
∀ s P t. s well formed ∧ P ∈• s ⇒ P fully defined wrt. contexts of shape ∘s ⇒ t ∈ Traces_∘s(P↓) ⇔ ζ∘(t) ∈ Traces_∘s(P↓)
∀ s A t. s well formed ∧ A ∈∘ s ⇒ A fully defined wrt. programs of shape •s ⇒ t ∈ Traces_•s(A↓) ⇔ ζ•(t) ∈ Traces_•s(A↓)
Intuition:
The code of fully defined players never changes (Stores are limited to buffers). Except for r_com, compiled players only read the content of registers after writing to them. As a consequence, any sequence of reductions followed under t can be followed under the canonicalized variant of t.
t ∀ ψ E t θ θ’. ψ; E ⊢• θ ⇒ θ’ ⇒ ∃ (T=α₁…αₙ) (θ₀…θₙ₊₁). θ₀ = θ ∧ θₙ₊₁ = θ’ ∧ erase(T) = t ∧ αᵢ ∀i. ψ; E ⊢• θᵢ → θᵢ₊₁
Proof: We can repeatedly apply inversion to directly get the result.
Note: Alternative point of view.
Consider the alternate trace semantics T ψ; E ⊢• θ ⇒ θ’ where the rules are copied except rule T_Internal which we replace with:
Iα ψ; E ⊢• θ → θ’ —————————————— T_Internal’ Iα ψ; E ⊢• θ ⇒ θ’
There is a direct mapping between proofs of t ψ; E ⊢ θ ⇒ θ’ and proofs of T ψ; E ⊢ θ ⇒ θ’ in which t = erase(T).
∀ E Eₚ Eₐ ψ Pθ Aθ state’, ψ well formed ∧ ψ ⊢ E well formed ∧ E = Eₚ ⊎ Eₐ ⇒ Eₚ ⊢ Pθ well formed ∧ Eₐ ⊢ Aθ well formed ⇒ mergeable Pθ Aθ ⇒
ψ; E ⊢ (merge Pθ Aθ) → state’ ⇒
∃ Pθ’ Aθ’. state’ = merge Pθ’ Aθ’ ∧ Iα Iα⁻¹ (∃Iα. ψ; Eₚ ⊢ Pθ → Pθ’ ∧ ψ; Eₐ ⊢ Aθ → Aθ’ ∧ Eₚ ⊢ Pθ’ well formed ∧ Eₐ ⊢ Aθ’ well formed
∨ Eα Eα⁻¹ ∃Eα. ψ; Eₚ ⊢ Pθ → Aθ’ ∧ ψ; Eₐ ⊢ Aθ → Pθ’ ∧ Eₚ ⊢ Aθ’ well formed ∧ Eₐ ⊢ Pθ’ well formed)
Start by inverting (mergeable Pθ Aθ): ∃ C, PΣ, AΣ, memₚ, memₐ, reg, pc Pθ = (C, PΣ, memₚ, reg, pc) Aθ = (C, AΣ, memₐ, /, /) mergeable PΣ AΣ dom(memₚ) ∩ dom(memₐ) = ∅
By the well formedness assumption on PΣ, C ∈ dom(memₚ) = dom(Eₚ).
Define state as: state ≜ merge Pθ Aθ = (C, merge PΣ AΣ, memₚ ⊎ memₐ, reg, pc)
We now proceed by case on the rule applied in ψ; E ⊢ (merge Pθ Aθ) → state’ and invert the rule.
These rules don’t change the stack nor look at it. Neither do they change the current compartment. They may only change the memory of the current compartment C, which lives in memₚ by the well-formedness assumption on PΣ. Hence, by inversion, ∃ mem’ₚ reg’ pc’.
state’ = (C, merge PΣ AΣ, mem’ₚ ⊎ memₐ, reg’, pc’) dom(mem’ₚ) = dom(memₚ)
No matter the rule, one can check that we can also apply said rule to get that:
ψ; Eₚ ⊢ (C, Top(PΣ), memₚ, reg, pc) → (C, Top(PΣ), mem’ₚ, reg’, pc’)
Hence, we can apply rule T_CallRetTau+ and get that: τ+ ψ; Eₚ ⊢ (C,PΣ,memₚ,reg,pc) → Pθ’
where
Pθ’ = (C, PΣ, mem’ₚ, reg’, pc’).
We can trivially apply rule T_Tau- and get that:
τ- ψ; Eₐ ⊢ Aθ → Aθ.
So we can take Aθ’ = Aθ and get state’ = merge Pθ’ Aθ’ then prove left by choosing Iα = τ+ (well formedness conditions are met).
By inversion, ∃ C’ P’ state’ = (C’, (C, pc+1) :: merge PΣ AΣ, memₚ ⊎ memₐ, reg, (Eₚ ⊎ Eₐ)[C’][P’]) decode((memₚ ⊎ memₐ)[C,pc]) = Call C’ P’ C’.P’ ∈ ψ[C].import ∨ C’ = C
Component C lives in memₚ by the well formedness assumption, so decode(memₚ[C,pc]) = decode((memₚ ⊎ memₐ)[C,pc]) = Call C’ P’.
In this case Eₚ[C’][P’] = (Eₚ ⊎ Eₐ)[C’][P’].
We have all required premises to apply rule S_Call and get that ∀σ ψ; Eₚ ⊢ ( C, σ, memₚ, reg, pc) → (C’, (C, pc+1) :: σ, memₚ, reg, Eₚ[C’][P’]) which we can instantiate with σ=Top(PΣ) to get, using T_CallRetTau+, that C’.P’(/) + ψ; Eₚ ⊢ Pθ → Pθ’ where Pθ’ = (C’, SetTop(PΣ, (C, pc+1) :: Top(PΣ)), memₚ, reg, Eₚ[C’][P’]).
Moreover C’ ∉ dom(Eₐ) since Eₐ ∩ Eₚ = ∅ follows from E = Eₐ ⊎ Eₚ. We have all required premises to apply rule T_Call- and get that C’.P’(/) - ψ; Eₐ ⊢ Aθ → Aθ’ where Aθ’ = (C’,SetTop(AΣ,(C,/)::Top(AΣ)),memₐ,/,/).
We have all required premises to conclude that (mergeable Pθ’ Aθ’) and that merge Pθ’ Aθ’ = (C’,(C,pc+1)::merge PΣ AΣ,memₚ ⊎ memₐ,reg,Eₚ[C’][P’)) = state’.
In other words we can prove left by choosing Iα = C’.P’(/)+ (well formedness conditions are met).
In this case Eₐ[C’][P’] = (Eₚ ⊎ Eₐ)[C’][P’].
Since C’∉ dom(Eₚ) and C∈dom(Eₚ), we have that C’≠C. Hence C’.P’ ∈ ψ[C].import.
We have all required premises to apply rule T_Call! and get that C’.P’(reg) ! ψ; Eₚ ⊢ Pθ → Aθ’ where Aθ’ = (C’, []::SetTop(PΣ, (C, pc+1)::Top(PΣ)), memₚ, /, /).
We have all required premises to apply rule T_Call? and get that C’.P’(reg) ? ψ; Eₐ ⊢ Aθ → Pθ’ where Pθ’ = (C’,[]::SetTop(AΣ,(C,/)::Top(AΣ)),memₐ,reg,Eₐ[C’][P’]).
We have all required premises to conclude that (mergeable Pθ’ Aθ’) and that merge Pθ’ Aθ’ = (C’,[] ++ (C,pc+1)::merge PΣ AΣ,memₚ ⊎ memₐ,reg,Eₐ[C’][P’]) = state’.
In other words we can prove right by choosing Eα = C’.P’(reg)! (well formedness conditions are met).
By inversion, ∃ C’ P’ σ’ merge PΣ AΣ = (C’, i’) :: σ’ state’ = (C’, σ’, memₚ ⊎ memₐ, reg, i’) decode((memₚ ⊎ memₐ)[C,pc]) = Return
Component C lives in memₚ by the well formedness assumption, so decode(memₚ[C,pc]) = decode((memₚ ⊎ memₐ)[C,pc]) = Return.
In this case, it follows from the state wellformedness conditions that Top(PΣ) = (C’, i’) :: tail Top(PΣ) Top(AΣ) = (C’, /) :: tail Top(AΣ).
We have all required premises to apply rule S_Return and get that ∀ σ ψ; Eₚ ⊢ ( C, (C’, i’) :: σ, memₚ, reg, pc) → (C’, σ, memₚ, reg, i’) which we can instantiate with σ=tail Top(PΣ) to get, using T_CallRetTau+, that Ret / + ψ; Eₚ ⊢ Pθ → Pθ’ where Pθ’ = (C’, SetTop(PΣ, tail Top(PΣ)), memₚ, reg, i’).
We have all required premises to apply rule T_Ret- and get that Ret / - ψ; Eₐ ⊢ Aθ → Aθ’ where Aθ’ = (C’,SetTop(AΣ,tail Top(AΣ)),memₐ,/,/).
We have all required premises to conclude that (mergeable Pθ’ Aθ’) and that merge Pθ’ Aθ’ = (C’,tail (merge PΣ AΣ),memₚ ⊎ memₐ,reg,i’) = state’.
In other words we can prove left by choosing Iα = Ret / + (well formedness conditions are met).
In this case, it follows from the state wellformedness conditions that PΣ = [] :: AΣ’ Top(AΣ’) = (C’, /) :: tail Top(AΣ’) AΣ = [] :: PΣ’ Top(PΣ’) = (C’, i’) :: tail Top(PΣ’).
We have all required premises to apply rule T_Ret! and get that C’.P’(reg) ! ψ; Eₚ ⊢ Pθ → Aθ’ where Aθ’ = (C’, SetTop(AΣ’, tail Top(AΣ’)), memₚ, /, /).
We have all required premises to apply rule T_Ret? and get that C’.P’(reg) ? ψ; Eₐ ⊢ Aθ → Pθ’ where Pθ’ = (C’,SetTop(PΣ’,tail Top(PΣ’)),memₐ,reg,i’).
We have all required premises to conclude that (mergeable Pθ’ Aθ’) and that merge Pθ’ Aθ’ = (C’,tail (merge PΣ AΣ),memₚ ⊎ memₐ,reg,i’) = state’.
In other words we can prove right by choosing Eα = Ret reg! (well formedness conditions are met).
∀ Eₚ Eₐ ψ Pθ Aθ Pθ’ Aθ’ Iα, ψ well formed ∧ ψ ⊢ Eₚ well formed ∧ ψ ⊢ Eₐ well formed ⇒ dom(Eₚ) ∩ dom(Eₐ) = ∅ ⇒ Eₚ ⊢ Pθ well formed ∧ Eₐ ⊢ Aθ well formed ⇒ mergeable Pθ Aθ ⇒
Iα ψ; Eₚ ⊢ Pθ → Pθ’ ⇒
Iα⁻¹ ψ; Eₐ ⊢ Aθ → Aθ’ ⇒
mergeable Pθ’ Aθ’ ∧ ψ; Eₚ ⊎ Eₐ ⊢ (merge Pθ Aθ) → (merge Pθ’ Aθ’)
∀ Eₚ Eₐ ψ Pθ Aθ Pθ’ Aθ’ Eα, ψ well formed ∧ ψ ⊢ Eₚ well formed ∧ ψ ⊢ Eₐ well formed ⇒ dom(Eₚ) ∩ dom(Eₐ) = ∅ ⇒ Eₚ ⊢ Pθ well formed ∧ Eₐ ⊢ Aθ well formed ⇒ mergeable Pθ Aθ ⇒
Eα ψ; Eₚ ⊢ Pθ → Aθ’ ⇒
Eα⁻¹ ψ; Eₐ ⊢ Aθ → Pθ’ ⇒
mergeable Pθ’ Aθ’ ∧ ψ; Eₚ ⊎ Eₐ ⊢ (merge Pθ Aθ) → (merge Pθ’ Aθ’)
∀ Eₚ Eₐ ψ Pθ Aθ Pθ’ Aθ’, ψ well formed ∧ ψ ⊢ Eₚ well formed ∧ ψ ⊢ Eₐ well formed ⇒ dom(Eₚ) ∩ dom(Eₐ) = ∅ ⇒ Eₚ ⊢ Pθ well formed ∧ Eₐ ⊢ Aθ well formed ⇒ mergeable Pθ Aθ ⇒
✓! ψ; Eₚ ⊢ Pθ → EXITED ⇒
✓? ψ; Eₐ ⊢ Aθ → EXITED ⇒
ψ; Eₚ ⊎ Eₐ ⊢ (merge Pθ Aθ) ↛
The proof is similar for all lemmas. Start by inverting (mergeable Pθ Aθ): ∃ C, PΣ, AΣ, memₚ, memₐ, reg, pc Pθ = (C, PΣ, memₚ, reg, pc) Aθ = (C, AΣ, memₐ, /, /) mergeable PΣ AΣ dom(memₚ) ∩ dom(memₐ) = ∅
Moreover from the wellformedness condition on Pθ, C ∈ dom(memₚ)
Define state as: state ≜ merge Pθ Aθ = (C, merge PΣ AΣ, memₚ ⊎ memₐ, reg, pc)
We proceed by case on action α. In each case, only one rule applies for Pθ →α and Aθ →α⁻¹ and we apply inversion on these rules.
For non-terminating actions, these inversions are enough to check: (1) that mergeability conditions are met for Pθ’ and Aθ’; (2) that merge Pθ Aθ reduces to merge Pθ’ Aθ’.
For terminating actions, these inversions are enough to check that merge Pθ Aθ does not reduce. More details are provided below.
Inversion of T_Tau-: Aθ’ = Aθ
Inversion of T_CallRetTau+: ∃ C’, σ, σ’, mem’ₚ, reg’, pc’, PΣ’ ψ; Eₚ ⊢ (C,σ,memₚ,reg,pc) → (C’,σ’,mem’ₚ,reg’,pc’) Top(PΣ) = σ PΣ’ = SetTop(PΣ, σ’) Pθ = (C,PΣ,memₚ,reg,pc) Pθ’ = (C’,PΣ’,mem’ₚ,reg’,pc’) decode(memₚ[C,pc]) ≠ Call _ _ decode(memₚ[C,pc]) ≠ Return
As an invariant of the operational semantics, dom(mem’ₚ) = dom(memₚ).
S_Call and S_Return are the only rules that modify C and σ in the low-level semantics. However, they do not apply since: decode(memₚ[C,pc]) ≠ Call _ _ decode(memₚ[C,pc]) ≠ Return. Hence, C’ = C and σ’ = σ, i.e. PΣ’ = PΣ.
Thus, Pθ’ = (C, PΣ, mem’ₚ, reg’, pc’) Aθ’ = (C, AΣ, memₐ, /, /) which are mergeable since we know that mergeable PΣ AΣ dom(mem’ₚ) ∩ dom(memₐ) = dom(memₚ) ∩ dom(memₐ) = ∅.
By case on the rule applied in ψ; Eₚ ⊢ (C,σ,memₚ,reg,pc) → (C,σ,mem’ₚ,reg’,pc’) which we know is not S_Call and S_Return, we can show that ψ; Eₚ ⊎ Eₐ ⊢ (C,merge PΣ AΣ,memₚ ⊎ memₐ, reg,pc) → (C,merge PΣ AΣ,mem’ₚ ⊎ memₐ,reg’,pc’). We already know that the rule doesn’t change nor look at the stack, and doesn’t change the component. Moreover, all potential memory reads and updates will happen in the memory of component C, which lives in memₚ.
Inversion of T_Call-: ∃ AΣ’, Aσ Aθ’ = (C’, AΣ’, memₐ, /, /) C’.P’ ∈ ψ[C].import ∨ C’ = C C’ ∉ dom(Eₐ) Top(AΣ) = Aσ AΣ’ = SetTop(AΣ, (C,/)::Aσ)
Inversion of T_CallRetTau+: ∃ C”,σ,σ’,mem’ₚ,reg’,pc’,PΣ’,C₀,P₀ ψ; Eₚ ⊢ (C,σ,memₚ,reg,pc) → (C”,σ’,mem’ₚ,reg’,pc’) Top(PΣ) = σ PΣ’ = SetTop(PΣ, σ’) Pθ = (C,PΣ,memₚ,reg,pc) Pθ’ = (C’,PΣ’,mem’ₚ,reg’,pc’) decode(memₚ[C,pc]) = Call C’ P’
Because of the condition on mem[C,pc], the only rule that can reduce (C,σ,memₚ,reg,pc) to (C”,σ’,mem’ₚ,reg’,pc’) is S_Call. Inversion of S_Call: C’.P’ ∈ ψ[C].import ∨ C’ = C C’ = C” σ’ = (C,pc+1)::σ mem’ₚ = memₚ reg’ = reg pc’ = Eₚ[C’][P’].
Hence Pθ’ = (C’,SetTop(PΣ,(C,pc+1)::Top(PΣ)),memₚ,reg,Eₚ[C’][P’]) Aθ’ = (C’,SetTop(AΣ,(C, /)::Top(AΣ)),memₐ, /, /) which are mergeable, and merge Pθ’ Aθ’ = (C’, (C,pc+1) :: merge PΣ AΣ, memₚ ⊎ memₐ, reg, Eₚ[C’][P’]). We have also gathered all premises to apply rule S_Call. We conclude that (C,merge PΣ AΣ,memₚ ⊎ memₐ, reg, pc) reduces to the state above, given that (Eₐ⊎Eₚ)[C’][P’] = Eₚ[C’][P’].
Inversion of T_Ret-: ∃ C’, AΣ’, Aσ’ Aθ’ = (C’, AΣ’, memₐ, , /) Top(AΣ) = (C’,)::Aσ’ AΣ’ = SetTop(AΣ, Aσ’)
Inversion of T_CallRetTau+: ∃ C”,σ,σ’,mem’ₚ,reg’,pc’,PΣ’ ψ; Eₚ ⊢ (C,σ,memₚ,reg,pc) → (C”,σ’,mem’ₚ,reg’,pc’) Top(PΣ) = σ PΣ’ = SetTop(PΣ, σ’) Pθ = (C,PΣ,memₚ,reg,pc) Pθ’ = (C’,PΣ’,mem’ₚ,reg’,pc’) decode(memₚ[C,pc]) = Return
Because of the condition on mem[C,pc], the only rule that can reduce (C,σ,memₚ,reg,pc) to (C”,σ’,mem’ₚ,reg’,pc’) is S_Return. Inversion of S_Return: ∃ i’ σ = (C”, i’)::σ’ mem’ₚ = memₚ reg’ = reg pc’ = i’.
From the knowledge that mergeable PΣ AΣ we can infer that Top(AΣ) ⊆ Top(PΣ) i.e. (C’,/)::Aσ’ ⊆ (C”,i’)::σ’ from which we can infer that C” = C’.
By inverting mergeable PΣ AΣ we also get all the premises we need to conclude that mergeable PΣ’ AΣ’ since PΣ’ = SetTop(PΣ, tail Top(PΣ)) AΣ’ = SetTop(AΣ, tail Top(AΣ)) where tail takes the tail of a list.
Hence Pθ’ = (C’,SetTop(PΣ, tail Top(PΣ)),memₚ,reg,i’) Aθ’ = (C’,SetTop(AΣ, tail Top(AΣ)),memₐ, /, /) which are mergeable, and merge Pθ’ Aθ’ = (C’, tail (merge PΣ AΣ), memₚ ⊎ memₐ, reg, i’).
We have also gathered all premises to apply rule S_Return. We conclude that (C,merge PΣ AΣ,memₚ ⊎ memₐ, reg, pc) reduces to the state above, given that ∃ σ” merge PΣ AΣ = σ ++ σ” = (C’, i’) :: (σ’ ++ σ”).
Inversion of T_Call?: ∃ AΣ’, Aσ Pθ’ = (C’, []::AΣ’, memₐ, reg, E[C’][P’]) C’.P’ ∈ ψ[C].import C’ ∈ dom(Eₐ) Top(AΣ) = Aσ AΣ’ = SetTop(AΣ, (C,/)::Aσ)
Inversion of T_Call!: ∃ PΣ’, σ Aθ’ = (C’,[]::PΣ’,memₚ,/,/) decode(memₚ[C,pc]) = Call C’ P’ C’.P’ ∈ ψ[C].import C’ ∉ dom(Eₚ) Top(PΣ) = σ PΣ’ = SetTop(PΣ, (C,pc+1)::σ)
Hence Pθ’ = (C’,[]::SetTop(AΣ,(C, /)::Top(AΣ)),memₐ,reg,Eₚ[C’][P’]) Aθ’ = (C’,[]::SetTop(PΣ,(C,pc+1)::Top(PΣ)),memₚ, /, /) which are mergeable, and merge Pθ’ Aθ’ = (C’, (C,pc+1) :: merge PΣ AΣ, memₚ ⊎ memₐ, reg, Eₚ[C’][P’]). We have also gathered all premises to apply rule S_Call. We conclude that (C,merge PΣ AΣ,memₚ ⊎ memₐ, reg, pc) reduces to the state above, given that (Eₐ⊎Eₚ)[C’][P’] = Eₚ[C’][P’].
Inversion of T_Ret?: ∃ C’, PΣₐ, PΣ’, σ, pc’ Pθ’ = (C’, PΣ’, memₐ, reg, pc’) AΣ = [] :: PΣₐ Top(PΣₐ) = (C’,pc’)::σ PΣ’ = SetTop(PΣₐ, σ)
Inversion of T_Ret!: ∃ C”, AΣₚ, AΣ’, Aσ Aθ’ = (C”, AΣ’, memₚ, /, /) decode(memₚ[C,pc]) = Return PΣ = [] :: AΣₚ Top(AΣₚ) = (C”,/)::Aσ AΣ’ = SetTop(AΣₚ, Aσ)
From the knowledge that mergeable PΣ AΣ we can infer that Top(AΣₚ) ⊆ Top(PΣₐ) i.e. (C’,/)::Aσ ⊆ (C”,pc’)::σ from which we can infer that C” = C’.
By inverting mergeable PΣ AΣ we also get mergeable PΣₐ AΣₚ from which we also get all the premises we need to conclude that mergeable PΣ’ AΣ’ since PΣ’ = SetTop(PΣₐ, tail Top(PΣₐ)) AΣ’ = SetTop(AΣₚ, tail Top(AΣₚ)) where tail takes the tail of a list.
Hence Pθ’ = (C’,SetTop(PΣₐ, tail Top(PΣₐ)),memₚ,reg,pc’) Aθ’ = (C’,SetTop(AΣₚ, tail Top(AΣₚ)),memₐ, /, /) which are mergeable, and merge Pθ’ Aθ’ = (C’, tail (merge PΣ AΣ), memₚ ⊎ memₐ, reg, i’) since merge PΣ AΣ = [] ++ merge PΣₐ AΣₚ = merge PΣₐ AΣₚ.
We have also gathered all premises to apply rule S_Return. We conclude that (C,merge PΣ AΣ,memₚ ⊎ memₐ, reg, pc) reduces to the state above, given that ∃ σ” merge PΣ AΣ = σ ++ σ” = (C’, pc’) :: (σ’ ++ σ”).
Inversion of T_Exit!: α ∀ α ≠ ✓!. ψ; Eₚ ⊢ (C,PΣ,memₚ,reg,pc) ↛
Goal: ψ; Eₚ ⊎ Eₐ ⊢ (C, merge PΣ AΣ, memₚ ⊎ memₐ, reg, pc) ↛
By contradiction. Assume one of the rules of the operational semantics applies. In this case, we can apply our non-terminating action decomposition lemma to this reduction and get that Pθ reduces with either an internal action or an external action from the program, that isn’t termination. But no such reduction is possible, from what we’ve learned by inverting T_Exit!.
∀ E Eₚ Eₐ ψ Pθ Aθ state’, ψ well formed ∧ ψ ⊢ E well formed ∧ E = Eₚ ⊎ Eₐ ⇒ Eₚ ⊢ Pθ well formed ∧ Eₐ ⊢ Aθ well formed ⇒ mergeable Pθ Aθ ⇒
ψ; E ⊢ (merge Pθ Aθ) ↛ ⇒
✓! ✓? ψ; Eₚ ⊢ Pθ → EXITED ∧ ψ; Eₐ ⊢ Aθ → EXITED
Start by inverting (mergeable Pθ Aθ): ∃ C, PΣ, AΣ, memₚ, memₐ, reg, pc Pθ = (C, PΣ, memₚ, reg, pc) Aθ = (C, AΣ, memₐ, /, /) mergeable PΣ AΣ dom(memₚ) ∩ dom(memₐ) = ∅
By the well formedness assumption on PΣ, C ∈ dom(memₚ) = dom(Eₚ).
Define state as: state ≜ merge Pθ Aθ = (C, merge PΣ AΣ, memₚ ⊎ memₐ, reg, pc)
We can trivially apply T_Exit? to get that ψ; Eₐ ⊢ Aθ → EXITED. In order to apply T_Exit! and conclude that ✓! ψ; Eₚ ⊢ Pθ → EXITED, we only have to show that α ∀ α ≠ ✓!. ψ; E ⊢ (C,PΣ,mem,reg,pc) ↛.
We prove this by contradiction. Suppose such an α exists. The only rules that reduce a Pθ are those labeled with a program marker (! or +). So α is an internal or external program action, which is not termination (since we know α ≠ ✓!). We can thus apply a non-terminating trace composition lemma to get Pθ’ and Aθ’ such that ψ; E ⊢ (merge Pθ Aθ) → (merge Pθ’ Aθ’). This contradicts the hypothesis that ψ; E ⊢ (merge Pθ Aθ) ↛. Qed.
∀ Eₚ Eₐ ψ Pθ Aθ Pθ’ Aθ’, ψ well formed ∧ ψ ⊢ Eₚ well formed ∧ ψ ⊢ Eₐ well formed ⇒ dom(Eₚ) ∩ dom(Eₐ) = ∅ ⇒ Eₚ ⊢ Pθ well formed ∧ Eₐ ⊢ Aθ well formed ⇒ mergeable Pθ Aθ ⇒
t ψ; Eₚ ⊢ Pθ ⇒ Pθ’ ⇒
t⁻¹ ψ; Eₐ ⊢ Aθ ⇒ Aθ’ ⇒
mergeable Pθ’ Aθ’ ∧ ψ; Eₚ ⊎ Eₐ ⊢ (merge Pθ Aθ) →* (merge Pθ’ Aθ’)
∀ Eₚ Eₐ ψ Pθ Aθ Pθ’ Aθ’, ψ well formed ∧ ψ ⊢ Eₚ well formed ∧ ψ ⊢ Eₐ well formed ⇒ dom(Eₚ) ∩ dom(Eₐ) = ∅ ⇒ Eₚ ⊢ Pθ well formed ∧ Eₐ ⊢ Aθ well formed ⇒ mergeable Pθ Aθ ⇒
t ψ; Eₚ ⊢ Pθ ⇒ Aθ’ ⇒
t⁻¹ ψ; Eₐ ⊢ Aθ ⇒ Pθ’ ⇒
mergeable Pθ’ Aθ’ ∧ ψ; Eₚ ⊎ Eₐ ⊢ (merge Pθ Aθ) →* (merge Pθ’ Aθ’)
∀ Eₚ Eₐ ψ Pθ Aθ, ψ well formed ∧ ψ ⊢ Eₚ well formed ∧ ψ ⊢ Eₐ well formed ⇒ dom(Eₚ) ∩ dom(Eₐ) = ∅ ⇒ Eₚ ⊢ Pθ well formed ∧ Eₐ ⊢ Aθ well formed ⇒ mergeable Pθ Aθ ⇒
Eα ψ; Eₚ ⊢ Pθ ⇒ EXITED ⇒
Eα⁻¹ ψ; Eₐ ⊢ Aθ ⇒ EXITED ⇒
∃ ρ. ψ; Eₚ ⊎ Eₐ ⊢ (merge Pθ Aθ) →* ρ ↛
∀ Eₚ Eₐ ψ Pθ Aθ, ψ well formed ∧ ψ ⊢ Eₚ well formed ∧ ψ ⊢ Eₐ well formed ⇒ dom(Eₚ) ∩ dom(Eₐ) = ∅ ⇒ Eₚ ⊢ Pθ well formed ∧ Eₐ ⊢ Aθ well formed ⇒ mergeable Pθ Aθ ⇒
ψ; Eₚ ⊢ Pθ ⇏ ⇒
∀ ρ. ψ; Eₚ ⊎ Eₐ ⊢ (merge Pθ Aθ) →* ρ ⇒ ∃ ρ’. ψ; Eₚ ⊎ Eₐ ⊢ ρ → ρ’
∀ E Eₚ Eₐ ψ Pθ Aθ state’, ψ well formed ∧ ψ ⊢ E well formed ∧ E = Eₚ ⊎ Eₐ ⇒ Eₚ ⊢ Pθ well formed ∧ Eₐ ⊢ Aθ well formed ⇒ mergeable Pθ Aθ ⇒
ψ; E ⊢ (merge Pθ Aθ) →* state’ ⇒
∃ Pθ’ Aθ’ t. state’ = merge Pθ’ Aθ’ ∧ t t⁻¹ ( ψ; Eₚ ⊢ Pθ ⇒ Pθ’ ∧ ψ; Eₐ ⊢ Aθ ⇒ Aθ’ ∧ Eₚ ⊢ Pθ’ well formed ∧ Eₐ ⊢ Aθ’ well formed ∨ t t⁻¹ ψ; Eₚ ⊢ Pθ ⇒ Aθ’ ∧ ψ; Eₐ ⊢ Aθ ⇒ Pθ’ ∧ Eₚ ⊢ Aθ’ well formed ∧ Eₐ ⊢ Pθ’ well formed)
∧ (ψ; E ⊢ state’ ↛ ⇒ t.✓! t⁻¹.✓? (ψ; Eₚ ⊢ Pθ ⇒ EXITED ∧ ψ; Eₐ ⊢ Aθ → EXITED ∨ t.✓? t⁻¹.✓! ψ; Eₚ ⊢ Pθ ⇒ EXITED ∧ ψ; Eₐ ⊢ Aθ → EXITED))
By induction on →*.
In this case state’ = (merge Pθ Aθ). We can choose Pθ’ = Pθ Aθ’ = Aθ t = ε.
Prove left in the disjunction by applying rule rule T_Refl.
Apply terminating action decomposition lemma.
Induction hypothesis gives us Pθ₀ Aθ₀ t₀ such that ψ; E ⊢ (merge Pθ Aθ) →* state₀ ψ; E ⊢ state₀ → state’ state₀ = merge Pθ₀ Aθ₀ t₀ t₀⁻¹ ( ψ; Eₚ ⊢ Pθ ⇒ Pθ₀ ∧ ψ; Eₐ ⊢ Aθ ⇒ Aθ₀ ∧ Eₚ ⊢ Pθ₀ well formed ∧ Eₐ ⊢ Aθ₀ well formed ∨ t₀ t₀⁻¹ ψ; Eₚ ⊢ Pθ ⇒ Aθ₀ ∧ ψ; Eₐ ⊢ Aθ ⇒ Pθ₀ ∧ Eₚ ⊢ Aθ₀ well formed ∧ Eₐ ⊢ Pθ₀ well formed)
We show that ∃ Pθ’ Aθ’ t. state’ = merge Pθ’ Aθ’ ∧ t t⁻¹ ( ψ; Eₚ ⊢ Pθ ⇒ Pθ’ ∧ ψ; Eₐ ⊢ Aθ ⇒ Aθ’ ∧ Eₚ ⊢ Pθ’ well formed ∧ Eₐ ⊢ Aθ’ well formed ∨ t t⁻¹ ψ; Eₚ ⊢ Pθ ⇒ Aθ’ ∧ ψ; Eₐ ⊢ Aθ ⇒ Pθ’ ∧ Eₚ ⊢ Aθ’ well formed ∧ Eₐ ⊢ Pθ’ well formed).
For this we proceed by case on the disjunction. The proof is similar in both cases.
Left caseIn this case t₀ t₀⁻¹ ψ; Eₚ ⊢ Pθ ⇒ Pθ₀ ∧ ψ; Eₐ ⊢ Aθ ⇒ Aθ₀ ∧ Eₚ ⊢ Pθ₀ well formed ∧ Eₐ ⊢ Aθ₀ well formed
We can apply action decomposition lemma to ψ; E ⊢ state₀ → state’ to get Pθ’ Aθ’ such that state’ = merge Pθ’ Aθ’ and Iα Iα⁻¹ (∃Iα. ψ; Eₚ ⊢ Pθ₀ → Pθ’ ∧ ψ; Eₐ ⊢ Aθ₀ → Aθ’ ∧ Eₚ ⊢ Pθ’ well formed ∧ Eₐ ⊢ Aθ’ well formed
∨ Eα Eα⁻¹ ∃Eα. ψ; Eₚ ⊢ Pθ₀ → Aθ’ ∧ ψ; Eₐ ⊢ Aθ₀ → Pθ’ ∧ Eₚ ⊢ Aθ’ well formed ∧ Eₐ ⊢ Pθ’ well formed). We proceed by case on this disjunction.
In the left case, well formedness conditions Eₚ ⊢ Pθ’ well formed ∧ Eₐ ⊢ Aθ’ well formed are met. We can apply rule T_Internal twice to get that ε ψ; Eₚ ⊢ Pθ₀ ⇒ Pθ’ ε ψ; Eₐ ⊢ Aθ₀ ⇒ Aθ’ so we can apply rule T_Trans twice and deduce that t₀ t₀⁻¹ ψ; Eₚ ⊢ Pθ ⇒ Pθ’ ∧ ψ; Eₐ ⊢ Aθ ⇒ Aθ’. Qed (we have proved left with t = t₀).
In the right case, well formedness conditions Eₚ ⊢ Aθ’ well formed ∧ Eₐ ⊢ Pθ’ well formed are met. We can apply rule T_Cross twice to get that Eα ψ; Eₚ ⊢ Pθ₀ ⇒ Aθ’ Eα⁻¹ ψ; Eₐ ⊢ Aθ₀ ⇒ Pθ’ so we can apply rule T_Trans twice and deduce that t₀.Eα t₀⁻¹.Eα⁻¹ ψ; Eₚ ⊢ Pθ ⇒ Aθ’ ∧ ψ; Eₐ ⊢ Aθ ⇒ Aθ’. Qed (we have proved right with t = t₀.Eα).
Right caseIn this case t₀ t₀⁻¹ ψ; Eₚ ⊢ Pθ ⇒ Aθ₀ ∧ ψ; Eₐ ⊢ Aθ ⇒ Pθ₀ ∧ Eₚ ⊢ Aθ₀ well formed ∧ Eₐ ⊢ Pθ₀ well formed
We can apply action decomposition lemma to ψ; E ⊢ state₀ → state’ to get Pθ’ Aθ’ such that state’ = merge Pθ’ Aθ’ and Iα Iα⁻¹ (∃Iα. ψ; Eₐ ⊢ Pθ₀ → Pθ’ ∧ ψ; Eₚ ⊢ Aθ₀ → Aθ’ ∧ Eₐ ⊢ Pθ’ well formed ∧ Eₚ ⊢ Aθ’ well formed
∨ Eα Eα⁻¹ ∃Eα. ψ; Eₐ ⊢ Pθ₀ → Aθ’ ∧ ψ; Eₚ ⊢ Aθ₀ → Pθ’ ∧ Eₐ ⊢ Aθ’ well formed ∧ Eₚ ⊢ Pθ’ well formed). We proceed by case on this disjunction.
In the left case, well formedness conditions Eₐ ⊢ Pθ’ well formed ∧ Eₚ ⊢ Aθ’ well formed are met. We can apply rule T_Internal twice to get that ε ψ; Eₐ ⊢ Pθ₀ ⇒ Pθ’ ε ψ; Eₚ ⊢ Aθ₀ ⇒ Aθ’ so we can apply rule T_Trans twice and deduce that t₀ t₀⁻¹ ψ; Eₚ ⊢ Pθ ⇒ Aθ’ ∧ ψ; Eₐ ⊢ Aθ ⇒ Pθ’. Qed (we have proved right with t = t₀).
In the right case, well formedness conditions Eₐ ⊢ Aθ’ well formed ∧ Eₚ ⊢ Pθ’ well formed are met. We can apply rule T_Cross twice to get that Eα ψ; Eₐ ⊢ Pθ₀ ⇒ Aθ’ Eα⁻¹ ψ; Eₚ ⊢ Aθ₀ ⇒ Pθ’ so we can apply rule T_Trans twice and deduce that t₀.Eα⁻¹ t₀⁻¹.Eα ψ; Eₚ ⊢ Pθ ⇒ Pθ’ ∧ ψ; Eₐ ⊢ Aθ ⇒ Aθ’. Qed (we have proved left with t = t₀.Eα⁻¹).
We have chosen t, Aθ’, Pθ’ when proving left-hand side. We now show that for this t,
(ψ; E ⊢ state’ ↛ ⇒ t.✓! t⁻¹.✓? (ψ; Eₚ ⊢ Pθ ⇒ EXITED ∧ ψ; Eₐ ⊢ Aθ → EXITED ∨ t.✓? t⁻¹.✓! ψ; Eₚ ⊢ Pθ ⇒ EXITED ∧ ψ; Eₐ ⊢ Aθ → EXITED)).
First, recall that we have shown that state’ = merge Aθ’ Pθ’. Hence, if ψ; E ⊢ state’ ↛ we have all the premises to apply terminating action decomposition and get that either t t⁻¹ ψ; Eₚ ⊢ Pθ ⇒ Pθ’ ∧ ψ; Eₐ ⊢ Aθ ⇒ Aθ’ ∧ ✓! ✓? ψ; Eₚ ⊢ Pθ’ → EXITED ∧ ψ; Eₐ ⊢ Aθ’ → EXITED or t t⁻¹ ψ; Eₚ ⊢ Pθ ⇒ Aθ’ ∧ ψ; Eₐ ⊢ Aθ ⇒ Pθ’ ∧ ✓? ✓! ψ; Eₚ ⊢ Aθ’ → EXITED ∧ ψ; Eₐ ⊢ Pθ’ → EXITED. In both cases, we can apply rules T_Cross and T_Trans and conclude that t.✓! t⁻¹.✓? ψ; Eₚ ⊢ Pθ ⇒ EXITED ∧ ψ; Eₐ ⊢ Aθ ⇒ EXITED in the first case, and that t.✓? t⁻¹.✓? ψ; Eₚ ⊢ Pθ ⇒ EXITED ∧ ψ; Eₐ ⊢ Aθ ⇒ EXITED in the second case. Qed.
∀ s t γ₁. t = ζ∘(t) ⇒ (∃ p. p ∈• s ∧ t.γ₁! ∈ Traces_∘s(p)) ⇒ ∃A. A ∈∘ s ∧ A fully defined wrt. programs of shape •s ∧ (1) t ∈ Traces_•s(A↓) ∧ (2) γ₁ ≠ ✓ ⇒ (t.γ₁!.✓?) ∈ Traces_•s(A↓) ∧ (3) (∀ γ γ’. (t.γ!.γ’?) ∈ Traces_•s(A↓) ⇒ ζ(γ) = ζ(γ₁) ∧ γ’ = ✓)
Proof intuition: From the fact that t.γ₁! ∈ Traces(p) we can apply internal trace recovery to trace t to get a trace with internal actions T such that t = erase(T) ∧ T=ζ∘(T).
We have written an algorithm in OCaml that constructs A. Its correctness would deserve its own proof and we later give some intuition about it. Here, we assume it: A ∈∘ s ∧ A fully defined wrt. programs of shape •s ∧ (1) t ∈ Traces_•s(A↓) ∧ (2) γ₁ ≠ ✓ ⇒ (t.γ₁!.✓?) ∈ Traces_•s(A↓) ∧ (3) (∀ γ γ’. (t.γ!.γ’?) ∈ Traces_•s(A↓) ⇒ ζ(γ) = ζ(γ₁) ∧ γ’ = ✓)
Implementation of the algorithm: <tracemapping.ml>
Intuition about algorithm correctness: The algorithm uses component-local counters to do a potentially different action each time a context procedure is called. The counter increments by one upon each call to a procedure in the component. Based upon the value of the counter, we can produce the series of context actions that is prescribed by T. This corresponds to function reproduce_trace : state → trace → state where state is the type that is used to progressively reconstruct code for all procedures.
A key point is that context actions in T is a legitimate sequence of actions with respect to interface ψ since it’s extracted from a proof that t ∈ Traces(p). This allows us to define A such that A well formed ∧ A ⊢ s ∧ (1) erase(T⁻¹) = t⁻¹ ∈ Traces(A↓). In particular, the attacker will only produces calls that were described in T, and all of these calls are valid with respect to interface ψ.
A second key point is that after executing T⁻¹, we can choose a different action to take depending on the next program external action. If the next program action is a call, then counters allow us to make a distinction between that call and the previous ones in T. If the next program action is to return, then we can choose what to action to take after control returns to the pending function that is on top of the call stack. This allows us to only terminate if the next program action canonicalizes to γ₁ (provided that γ₁ gives back control, i.e. γ₁ ≠ ✓): we choose the next program action to be termination if the program takes a step that canonicalizes to γ₁, or divergence otherwise. The latter is done by calling a private procedure that unconditionally calls itself recursively. This corresponds to function discriminate_action : state → external_action → state. Formally, this translates to: (2) γ₁ ≠ ✓ ⇒ (t.γ₁!.✓?)⁻¹ ∈ Traces(A↓) ∧ (3) (∀ γ γ’. t.γ!.γ’? ∈ Traces(A↓) ⇒ ζ(γ) = ζ(γ₁) ∧ γ’ = ✓).
Words over alphabet Hα.
Hα ::= action and origin
| HEα external action and origin |
| HIα internal action and origin |
HEα ::= external action and origin
| Hea ! external action performed by the program |
| Hea ? external action performed by the context |
Hea, Γ ::= cross-boundary action
| C.P(i) cross-boundary call |
| Ret i cross-boundary return |
| ✓ termination |
Note: undefined behavior and infinite loops lead to the same sets of traces here. We only consider high-level traces of fully defined programs anyway in this subsection. Could track undefined behavior in traces if necessary (could be useful e.g. if we want to prove the sanity checks on full-definedness using traces).
∀ s T Γ₁. (∃ P. P ∈• s ∧ T.Γ₁! ∈ TR_∘s(P)) ⇒ ∃A. A ∈∘ s ∧ A fully defined wrt. programs of shape •s ∧ (1) T ∈ TR_•s(A) ∧ (2) Γ₁ ≠ ✓ ⇒ (T.Γ₁!.✓?) ∈ TR_•s(A) ∧ (3) (∀ Γ Γ’. (T.Γ!.Γ’?) ∈ TR_•s(A) ⇒ Γ = Γ₁ ∧ Γ’ = ✓)
Note: Could require that P is fully defined here.
(C.P(i))↓ = C.P(reg₀[r_com ↦ i]) (Ret i)↓ = Ret reg₀[r_com ↦ i] ✓↓ = ✓
(C.P(reg))↑ = C.P(reg[r_com]) (Ret reg)↑ = Ret reg[r_com] ✓↑ = ✓
∀ t, ((t↑)↓) = ζ•(ζ∘(t)) = ζ∘(ζ•(t))
∀ T, (T↓)↑ = T
∀ s T P. P ∈• s ∧ P fully defined wrt. contexts of shape ∘s ⇒ (T↓ ∈ Tr_∘s(P↓) ⇔ T ∈ TR_∘s(P))
∀ s T A. A ∈∘ s ∧ A fully defined wrt. programs of shape •s ⇒ (T↓ ∈ Tr_•s(A↓) ⇔ T ∈ TR_•s(A))
Note: Full definedness is actively used for the left-to-right direction.
∀ s t P. t = ζ•(t) ∧ P ∈• s ∧ P fully defined wrt. contexts of shape ∘s ⇒ (t ∈ Tr_∘s(P↓) ⇔ t↑ ∈ TR_∘s(P))
∀ s t A. t = ζ∘(t) ∧ A ∈∘ s ∧ A fully defined wrt. programs of shape •s ⇒ (t ∈ Tr_•s(A↓) ⇔ t↑ ∈ TR_•s(A))
Proof:
⇒ Let s t P. Suppose that t ∈ Tr_∘s(P↓). Applying “Canonicalization is invisible to fully defined players”, we know that ζ∘(t) ∈ Tr_∘s(P↓). But since t = ζ•(t) by hypothesis, ζ∘(t) = ζ∘(ζ•(t)) = (t↑)↓. Applying “Compiler preserves high-level traces for fully-defined programs” to T = t↑, we get that t↑ ∈ TR_∘s(P). Qed.
⇐ Let s t P. Suppose that t↑ ∈ TR_∘s(P). Applying “Compiler preserves high-level traces for fully-defined programs” to T = t↑, we get that (t↑)↓ ∈ Tr_∘s(P↓) where (t↑)↓ = ζ∘(ζ•(t)) = ζ∘(t), hence ζ∘(t) ∈ Tr_∘s(P↓). From “Canonicalization is invisible to fully defined players” we get that t ∈ Tr_∘s(P↓). Qed.
∀ s t γ₁. t = ζ∘(t) ⇒ (∃ P. P ∈• s ∧ P fully defined wrt. contexts of shape ∘s ∧ t.γ₁! ∈ Tr_∘s(P↓)) ⇒ ∃A. A ∈∘ s ∧ A fully defined wrt. programs of shape •s ∧ (1) t ∈ Tr_•s(A↓) ∧ (2) γ₁ ≠ ✓ ⇒ (t.γ₁!.✓?) ∈ Tr_•s(A↓) ∧ (3) (∀ γ γ’. (t.γ!.γ’?) ∈ Tr_•s(A↓) ⇒ ζ(γ) = ζ(γ₁) ∧ γ’ = ✓)
Note: t = ζ∘(ζ•(t)) = (t↑)↓ in this case because “Compiled, fully-defined players only yield canonical traces” and P is fully defined.
Proof:
Let s t γ₁ P. Because (t.γ₁!) ∈ Traces_∘s(P↓) and “Compiled, fully-defined players only yield canonical traces”, t.γ₁! = ζ•(t.γ₁!). We can thus apply extended trace preservation to (t.γ₁!) and P to get that (t.γ₁!)↑ ∈ TR_∘s(P). Applying source-level definability, we get an A such that A ∈∘ s ∧ A fully defined wrt. programs of shape •s ∧ (a) t↑ ∈ TR_•s(A) ∧ (b) γ₁↑ ≠ ✓ ⇒ (t↑.γ₁↑.✓?) ∈ TR_•s(A) ∧ (c) (∀ Γ Γ’. (T.Γ!.Γ’?) ∈ TR_•s(A) ⇒ Γ = γ₁↑ ∧ Γ’ = ✓).
Applying extended trace preservation to (a) immediately gives (1).
Regarding (2), suppose that γ₁ ≠ ✓. In this case, γ₁↑ ≠ ✓↑. So applying (b) and extended trace preservation to (t.γ₁.✓?) yields the expected result.
Let us finally consider (3). Let γ γ’ such that (t.γ!.γ’?) ∈ Tr_•s(A↓). Hence, from extended trace preservation, (t.γ!.γ’?)↑ ∈ TR_•s(A). Applying (c), we get that γ↑ = γ₁↑ ∧ γ’↑ = ✓, hence ζ(γ) = ζ(γ₁) ∧ γ’ = ✓.
∀ s P Q. s well formed ⇒ P ∈• s ∧ P fully defined wrt. contexts of shape ∘s ⇒ Q ∈• s ∧ Q fully defined wrt. contexts of shape ∘s ⇒ (∃ A. A ∈∘ s ∧ A fully defined wrt. programs of shape •s ∧ A[P] ≁H A[Q]) ⇒ ∃ a. a well formed ∧ a ⊢ s ∧ a[P↓] ≁L a[Q↓]
Proof:
Let s P Q. Assume a high-level context A such that A ∈∘ s ∧ A fully defined wrt. programs of shape •s ∧ A[P] ≁H A[Q]. Note that A[P] and A[Q] are both defined due to full-definedness conditions on A, P and Q. From the last condition on A we know that either (1) A[P] terminates ∧ A[Q] diverges or (2) A[Q] terminates ∧ A[P] diverges. We assume (1) without loss of generality ((2) is symmetric).
Take a = A↓. From shape preservation we get that A↓ ∈∘ s. Moreover from whole program compiler correctness it follows that (A[P])↓ terminates ∧ (A[Q])↓ diverges. Applying separate compilation we get that A↓[P↓] terminates ∧ A↓[Q↓] diverges, hence, because the low-level language is deterministic, A↓[P↓] ≁L A↓[Q↓]. QED.
∀ s P Q. s well formed ⇒ P ∈• s ∧ P fully defined wrt. contexts of shape ∘s ⇒ Q ∈• s ∧ Q fully defined wrt. contexts of shape ∘s ⇒ (∃ a. a well formed ∧ a ⊢ s ∧ a[P↓] ≁L a[Q↓]) ⇒ (∃ A. A ∈∘ s ∧ A fully defined wrt. programs of shape •s ∧ A[P] ≁H A[Q])
Proof: detailed in the paper at the very end of section 4.
∀ s p q. s well formed ∧ p ∈• s ∧ q ∈• s ⇒ (∃P. P ∈• s ∧ P fully defined wrt. contexts of shape ∘s ∧ ∀a, a ∈∘ s ⇒ a[p] ~L a[P↓]) ⇒ (∃Q. Q ∈• s ∧ Q fully defined wrt. contexts of shape ∘s ∧ ∀a, a ∈∘ s ⇒ a[q] ~L a[Q↓]) ⇒ (∃a. a ∈∘ s ∧ a[p] ≁L a[q]) ⇒ ∃ A. A ∈∘ s ∧ A fully defined wrt. programs of shape •s ∧ A↓[p] ≁L A↓[q]
Intuition: If p is contextually equivalent to some P↓ and q to some Q↓, then low-level attackers can’t do more harm than the compilation of a fully-defined high-level attacker.
Proof: Let s p q. Assume a P Q. We have that a[P↓] ~L a[p] ≁L a[q] ~L a[Q↓]. By transitivity, it holds that a[P↓] ≁L a[Q↓], hence we can directly apply the 2nd theorem to get that ∃ A. A ∈∘ s ∧ A fully defined wrt. programs of shape •s ∧ A[P] ≁H A[Q]. Assume such an A, then we can prove that A↓[P↓] ≁L A↓[Q↓] (proved in theorem 1). Hence, since A↓[p] ~L A↓[P↓] ∧ A↓[Q↓] ~L A↓[q] we can deduce that A↓[p] ≁L A↓[q]. QED.