Modular Software Fault Isolation as Abstract Interpretation

Abstract

Software Fault Isolation (SFI) consists in transforming untrusted code so that it runs within a specific address space, (called the sandbox) and verifying at load-time that the binary code does indeed stay inside the sandbox. Security is guaranteed solely by the SFI verifier whose correctness therefore becomes crucial. Existing verifiers enforce a very rigid, almost syntactic policy where every memory access and every control-flow transfer must be preceded by a sandboxing instruction sequence, and where calls outside the sandbox must implement a sophisticated protocol based on a shadow stack. We propose to define SFI as a defensive semantics, with the purpose of deriving semantically sound verifiers that admit flexible and efficient implementations of SFI. We derive an executable analyser, that works on a per-function basis, which ensures that the defensive semantics does not go wrong, and hence that the code is well isolated. Experiments show that our analyser exhibits the desired flexibility: it validates correctly sandboxed code, it catches code breaking the SFI policy, and it can validate programs where redundant instrumentations are optimised away.

Appendices

A Concrete Operational Semantics

B Intra-procedural Semantics

C Proof of Lemma 1

First we need an intermediate lemma:

Lemma 3

(Base pointer is contained).

$$\begin{aligned} \begin{array}{ll} \forall S = &{} \langle \langle bp, cs, \rho _i \rangle , \langle \rho ,\delta ,\phi ^{(\beta )},\iota \rangle \rangle \in Acc , \\ \quad \text {if } &{} \beta = 1 \\ \text { then } &{} s_0 - s_s + {\textsc {gz}}_\bot< bp \le s_0 - {\textsc {gz}}_\top \\ \text { else } &{} s_0 - s_s + {\textsc {gz}}_\bot - f_s < bp \le s_0 - {\textsc {gz}}_\top \end{array} \end{aligned}$$

Proof

We reason by induction on $S \in Acc$. In the initial state, we have $bp = s_0 - {\textsc {gz}}_\top$ and $\beta = 0$, so the property is true since $s_s > {\textsc {gz}}_\top + {\textsc {gz}}_\bot$.

In the inductive case, we procede by case analysis on , where S verifies the property. Because the property only depends on the context and $\beta$, most cases are trivial: they preserve the context and $\beta$. In the case of the StoreFrame rule, the context is preserved, and $\beta$ is updated to 1. The property is still preserved because the property when $\beta =0$ implies the property when $\beta = 1$.

The last case is when the extended call rule applies. In that case, $\beta (S) = 1$, $bp(S') = bp(S) - \mid \phi _1 \mid$ with $\mid \phi _1 \mid \le f_s$ and $\beta (S') = 0$.

Since $s_0 - s_s + {\textsc {gz}}_\bot < bp(S) \le s_0 - {\textsc {gz}}_\top$, $s_0 - s_s + {\textsc {gz}}_\bot - \mid \phi _1 \mid < bp(S') \le s_0 - {\textsc {gz}}_\top$, so $s_0 - s_s + {\textsc {gz}}_\bot - f_s < bp(S') \le s_0 - {\textsc {gz}}_\top$ and the property holds.

Now we can prove the main lemma:

Proof

First, we prove that $Acc \subseteq \gamma ({\textit{I}}\hbox {-} {\textit{Acc}})$.

Let $S \in Acc$. By induction on S, we have the following cases:

• $S = \langle \varGamma _0,\varSigma _0 \rangle = \langle \langle [\langle s_0, \phi _i \rangle ] , s_0-{\textsc {gz}}_\top , \rho _0 \rangle , \langle \rho ,\delta ,\phi ^{(0)},\iota _0 \rangle \rangle$ with $\mid \phi _i \mid = {\textsc {gz}}_\top$.

  By definition, $\iota _0 \in \mathcal {F}$, so we can construct $Init(\iota _0)$. By construction, $S \in \gamma (Init(\iota _0))$.

• $S = \langle \varGamma _2, \varSigma _2 \rangle \text { with } \langle \varGamma _1, \varSigma _1 \rangle \in Acc$ and . By induction hypothesis, we also have $S^\natural$ such that $\langle \varGamma _1, \varSigma _1 \rangle \in \gamma (S^\natural )$.

  Since ${\textit{I}}\hbox {-}{\textit{Safe}}({\textit{I}}\hbox {-} {\textit{Acc}})$, $S^\natural \rightarrow ^\natural S_2^\natural$.

  By case analysis on the rule that allows $\rightarrow ^\natural$, we have:

  • (FunAssign)    The preconditions are the same as for (Assign), so there is $S'$ such that $S \rightarrow ^\natural S'$. Furthermore, $S' \in \gamma (s'^{\sharp })$.

  • (FunStD, FunLdD, FunCont, FunIndirectJump, FunHalt, FunCrash)

    Similar reasoning.

  • (FunStF)    Here, the preconditions are either true for (StoreFrame) or (StoreCrash) because of Lemma 3, so there is $S'$ such that $S \rightarrow ^\natural S'$, with $S' = \blacksquare$ (writing in the guard zone) or $S' = \langle \rho ,\delta ,\phi ^{(\beta )},\iota \rangle$ (writing in the frame). Furthermore, $S' \in \gamma (s'^{\sharp })$.

  • (FunLdS)    Here, the preconditions are either true for (LoadStack) or (LoadCrash) because of Lemma 3, so there is $S'$ such that $S \rightarrow ^\natural S'$, with $S' = \blacksquare$ (reading in the guard zone) or $S' = \langle \rho ,\delta ,\phi ^{(\beta )},\iota \rangle$ (reading in the stack). Futhermore, $S' \in \gamma (s'^{\sharp })$.

  • (FunCall)    Here the preconditions are the same as for (CallAcc) because of Lemma 3, so there is $S'$ such that . Furthermore, $S' \in \gamma _s(Init(f)) \subseteq \gamma _s(S^{\sharp })$.

  • (FunRet)    Here the preconditions are the same as for (RetAcc), so . Furthermore, $\blacksquare \in \gamma (s'^{\sharp })$.

Hence our intermediate conclusion: $Acc \subseteq \gamma ({\textit{I}}\hbox {-} {\textit{Acc}})$.

Let’s now take $S \in Acc$. We use the previous conclusion to also choose $S^\natural \in {\textit{I}}\hbox {-} {\textit{Acc}}$ such that $S \in \gamma (S^\natural )$. Because we have ${\textit{I}}\hbox {-}{\textit{Safe}}({\textit{I}}\hbox {-} {\textit{Acc}})$, we can also take $S_2^\natural$ such that $S^\natural \rightarrow S_2^\natural$.

By case analysis with a similar reasoning as the previous property, we get that with $S' \in \gamma (S_2^\natural )$.

Hence $Safe ( Acc )$.

D Proof of Lemma 2

Proof

First, we prove that ${\textit{I}}\hbox {-} {\textit{Acc}}\subseteq \gamma ({\textit{A}}\hbox {-} {\textit{Acc}})$.

Let $S \in {\textit{I}}\hbox {-} {\textit{Acc}}$. By induction on S, we have the following cases:

• $S \in Init(f) = \langle \langle \phi _i, bp, \rho \rangle , \langle \rho ,\phi ^{(f)},0 \rangle \rangle$

  We can construct $S^\sharp = \langle \langle \phi _i', bp, \rho ' \rangle , \langle \rho ',\phi '^{(f)},0 \rangle \in AInit(f)$ such that $S \in \gamma (S^\sharp )$.

  $S^\sharp \in {\textit{A}}\hbox {-} {\textit{Acc}}$, so the property is true in that case.

• $S = \langle \varGamma , \varSigma _2 \rangle \text { with } \langle \varGamma , \varSigma _1 \rangle \in {\textit{I}}\hbox {-} {\textit{Acc}}\text { and } \varGamma \vdash \varSigma _1 \rightarrow ^\natural \varSigma _2$. By induction hypothesis, we also have $S^\sharp$ such that $\langle \varGamma _1, \varSigma _1 \rangle \in \gamma (S^\sharp )$.

  Because we have ${\textit{A}} \hbox {-} {\textit{Safe}}({\textit{A}}\hbox {-} {\textit{Acc}})$, we also have $S_2^\sharp$ such that $S^\sharp \rightarrow S_2^\sharp$.

  By case analysis on $\rightarrow$, we can see as before that the preconditions of the abstract semantics are the same or more restrictive than those of the intra procedural semantics. It is also built in a way that $\langle \varGamma , \varSigma _2 \rangle \in \gamma (S_2^\sharp )$.

Hence our intermediate conclusion: ${\textit{I}}\hbox {-} {\textit{Acc}}\subseteq \gamma ({\textit{A}}\hbox {-} {\textit{Acc}})$.

Let’s now take $S \in {\textit{I}}\hbox {-} {\textit{Acc}}$. We use the previous conclusion to also choose $S^\sharp \in {\textit{A}}\hbox {-} {\textit{Acc}}$ such that $S \in \gamma (S^\sharp )$. Because we have ${\textit{A}} \hbox {-} {\textit{Safe}}({\textit{A}}\hbox {-} {\textit{Acc}})$, we can also take $S_2^\sharp$ such that $S^\sharp \rightarrow S_2^\sharp$.

By case analysis with a similar reasoning as the previous property, we get that with $S' \in \gamma (S_2^\sharp )$.

Hence $Safe ({\textit{I}}\hbox {-} {\textit{Acc}})$.