Question Lists:
Task, Procedure and Critical Procedure. A task $T$ is a set of procedures where a procedure takes inputs and / or returns an output. We define $p(S) \in T$ as a critical procedure, where $p$ takes input a secret set $S$ and returns a value $r_p$.
Proof of Being Forgotten (PoBF) refers to a kind of regulation enforcing that code dealing with secrets is verified so that:
Formally, given a critical procedure $p(S)$, Being Forgotten $\mathsf{BF}(p(S))$ is a conjunction of not Leaked and not residual; that is:
$$ \mathsf{BF}(p(S)) \overset{\Delta}{=} \neg \mathsf{Leaked}(p, S^) \wedge \neg \mathsf{Residual}(p, S^). $$
Leaked. Given a critical procedure $p(S)$, $\mathsf{Leaked}(p, S^)$ is a predicate which evaluates to true if and only if some $s^ \in S^*$ is accessed by procedures other than $p(S)$ while it is not returned, unless it is accessed by critical procedures invoked by $p(S)$.
Residual. Given a critical procedure $p(S)$, $\mathsf{Residual}(p, S^)$ is a predicate which evaluates to true when some $s^ \in S^* \setminus \{r_p\}$ exists after $p(S)$ finishes, or the return value $r_p$ is accessed by non-critical procedures.
Why use TEE as core infrastructure of PoBF? This is because TEE provided code integrity, and the platform can attest to the end-users that the code is indeed in compliance with PoBF constraints. With TEE deployed, there is another term called zone. A zone $\cal Z$ is a set of all modifiable enclave resources accessible by a critical procedure $p(S)$. PoBF ensures that a) critical procedures can only write to $\cal Z$, and b) secrets are completely scrubbed after execution except the return value $r_p$.
An interesting fact is, the term leakage also considers the values tainted by the initial secret. In the core functionalities of POBF, we just designate a simple private computation function called private_vec_compute as the workflow.
Restriction for Leakage ⇒ the aforementioned zone should be restricted while the program is running and should be read exclusive. Formally,
$$ \mathsf{Restricted}(p(S), \mathcal{Z}) \overset{\Delta}{=}\mathsf{WriteBounded} \wedge \mathsf{ReadExclusive} $$
where
$$ \mathsf{WriteBounded}(p(S), \mathcal{Z}) \Leftrightarrow \forall \mathsf{op}(\mathrm{arg}*) \in p, \mathsf{op} = \mathsf{Write} \Rightarrow \mathrm{arg} \in \cal Z. $$
$$ \mathsf{ReadExclusive}(p(S), \mathcal{Z}) \Leftrightarrow \forall\mathsf{op}(\mathrm{arg}*) \in \mathcal{T} \setminus \{p\}, \mathsf{op} = \mathsf{Read} \Rightarrow \mathrm{arg} \notin \mathcal{Z} $$
The thing is, for a single-threaded task, read exclusion can be without doubt guaranteed, but this does not necessarily hold true for multi-threaded tasks. Using Coq, the following theorem holds true.
Theorem. Restricted means no leakage.
CleanMoved for residual. Residue should be safely cleaned after the execution of critical procedures. Also the return value $r_p$ must be passed to the next procedure intactly and cannot be accessed by any other entities. Formally,
$$ \mathsf{CleanMoved}(p(S), \mathcal{Z}) \overset{\Delta}{=} \mathsf{Zeroized(p(S), \mathcal{Z})} \wedge \mathsf{SafeTransferred}(p(S), p_{next}(S_{next})). $$
where
$$ \mathsf{Zerorized}(p(S), \mathcal{Z}) \Leftrightarrow \forall l \in \mathcal{Z} \setminus loc(r_p), read(l) = 0. $$
$$ \mathsf{SafeTransferred}(p(S), p_{next}(S_{next})) \Leftrightarrow r_p \in S_{next} \wedge (\forall \mathsf{op} \in \mathcal{T}, \mathrm{arg} \in loc(r_p) \wedge \mathsf{op} = read(\mathrm{arg}*) \Rightarrow \mathsf{op} \in p_{next}(S_{next})) $$
Using Coq, the following theorem holds true.
Theorem. CleanMoved means no residue.
Theorem. For a single-thread program, if $p_{next}$ is executed right after $p(S)$ and the zone remains unchanged, then the transfer is safe. ⇒ creusot: Only need to prove zeroized.
Exception: the last critical procedure does not have any next procedure, so we assume it always satisfies safe transfer, but to the extent that it is an encryption algorithm that completely consumes the input secret. We call it EndWithEncryption.
PoBF for the Task.
$$ \mathsf{BF}(\mathcal{T}) \Leftrightarrow \bigwedge_{p_i \in \mathcal{T}}\mathsf{Restricted}(p_i(S), \mathcal{Z}) \wedge \bigwedge_{p_i \in \mathcal{T}}\mathsf{CleanMoved}(p_i(S), \mathcal{Z}) \wedge \mathsf{EndWithEncryption} $$
By 1, 2, 3, to prove the single-threaded task is BF, we only need to prove that each critical procedure is write bounded, safe transferred and zeorized, and the last critical procedure is an encryption algorithm. These can be done using Coq (see Software Foundations).
Rust (Ownership, Memory and Thread Safety)+ Teaclave (Code Integrity and Confidentiality) + MIRAI (Abstract Interpretation for verification and static analysis).