A soundness proof for the offline memory checker of Clarke et al. (2003)

The memory checker of Incremental Multiset Hash Functions and Their Application to Memory Integrity Checking (Clarke et al., 2003) is sound, but the soundness proof they give in Appendix E has problems (see the very end for details). We give a correct proof here.

[This is not a big deal. The central contribution of the paper was incremental hash functions for multisets. The offline memory checking functionality (setting hashes aside) was adopted with only minor modifications from Blum et al.’s “Checking the correctness of memories” (1991). The proof in Blum et al. was correct, but Clarke et al.’s exposition is sufficiently preferable to warrant my taking the time to patch their proof. Also, it’s interesting.]

We ignore the hashes and work information theoretically; let \(R,W\) denote the multisets of read and write triples \((a,v,t)\), respectively, maintained by the checker. The checker’s state is trusted, and timestamps do not overflow.

An execution is defined to be a sequence

where \(E_{\mathrm{init}}\) and \(E_{\mathrm{check}}\) are calls to initialize() and check(), respectively, and \(E_1,\ldots,E_k\) are either load or store operations; \(k\geq0\).

For \(0\leq i\leq k+1\), write \((\Delta R)_i\) for the set of tuples added to \(R\) by \(E_i\) (it is always a set); similarly for \((\Delta W)_i\).

For every address \(a\) and \(0\leq i\leq k\), let \(j\) be maximal such that

Then \(v,t\) are uniquely defined; write \(L_i(a):=(v,t)\). That is, after operation \(E_i\) has completed, \(L_i(a)\) is the most recent \((v,t)\) pair that was asked to be written to RAM at address \(a\).

For \(1\leq i\leq k+1\), write \(H_i\) for “RAM was honest at \(E_i\)”, where honesty is defined by

Note. The untrusted RAM is a black box, so dishonesty is only meaningful where it can be observed, namely at reads from RAM (in get(a)). Thus dishonesty is definitionally impossible at \(E_0=E_{\mathrm{init}}\), but is possible at \(E_{k+1}=E_{\mathrm{check}}\).

Note. Our definition of honesty is stronger than that of the paper, which sometimes allows returned timestamps to be false if the returned value was correct. Indeed, inconsistency in this regard appears in the problem with their soundness proof.

For every \((a,v,t)\) and \(0\leq i\leq k+1\), write \(r_i(a,v,t)\) for the multiplicity of \((a,v,t)\) in \(R\) after \(E_i\); similarly, write \(w_i(a,v,t)\) for its multiplicity in \(W\).

For \(0\leq i\leq k\), define the following statements:

where \(T_i\) denotes the value of the checker’s timer, or counter, after \(E_i\), and \(\delta\) is the Kronecker delta. We will show that operations transition between \(A\) and \(B\) as follows:

Define the statement

TIMER holds after all operations—indeed, before and after every completed get and put in an execution (this is needed)—irrespective of RAM honesty. This is obvious from the pseudocode. It is this statement that ensures the transition from \(A\) to \(B\) when \(\neg H_i\) for some \(1\leq i\leq k\), as we will see.

Proposition \(A\xrightarrow{\mathrm{dishonest}}B\):

Proof. Since \(i<k\), \((\Delta R)_{i+1}=\{(a,v,t)\}\) is a singleton, and since \(\neg H_{i+1}\), \(L_i(a)\ne(v,t)\). Writing \(x=(a,v,t)\), we thus have

After the get of \(E_{i+1}\), TIMER gives \(T>t\), so the put of \(E_{i+1}\) adds \((a,v’,T)\) to \(W\), and this is different from \(x\). In particular, \(w_{i+1}(x)=w_i(x)\). Thus

and so \(B_{i+1}\) holds. \(\square\)

Proposition \(\operatorname{init}()\longrightarrow A_0\):

Proof. After \(E_0=E_{\mathrm{init}}\),

and \(L_0(a)=(0,0)\) for all addresses \(a\). Thus, for any \(x=(a,v,t)\), the condition of \(A_0\) holds with pattern \(1=0+1\) when \(v=t=0\), and pattern \(0=0+0\) otherwise. \(\square\)

Proposition \(A\xrightarrow{\mathrm{honest}}A\):

Proof. Since \(i<k\), \((\Delta R)_{i+1}=\{\underbrace{(a,v,t)}_{x}\}\) is a singleton, and since \(H_{i+1}\), \(L_i(a)=(v,t)\). Thus

After the get of \(E_{i+1}\), TIMER ensures \(T>t\), so \((\Delta W)_{i+1}=\{(a,v’,T)\}\) for some \(v’\). In particular, \(x\ne(a,v’,T)=:x’\). So

Thus, for \(x\),

While for \(x’\),

Since \(x,x’\) are the only tuples for which \(r_i,w_i\) can differ from \(r_{i+1},w_{i+1}\), respectively, and \(a\) is the only address at which \(L_i\) and \(L_{i+1}\) differ, we thus have that \(A_{i+1}\) holds. \(\square\)

Proposition \(B\xrightarrow{\mathrm{any}}B\):

Proof. Suppose \(B_i\). Then there exists \((a,v,t)\) such that \(w_i(a,v,t)<r_i(a,v,t)\) and \(t<T_i\). We have

for some \(a’,v’\), and \(T_{i+1}\geq T_i>t\). Thus

and so

Thus \(B_{i+1}\) holds. \(\square\)

Proposition check():

Proof. (a) Supposing \(A_k\),

(b) Let \(x=(a,v,t)\) witness \(B_k\). Then

and so check() rejects, since \(w_{k+1}(x)\ne r_{k+1}(x)\). \(\square\)

Theorem:

Proof. By Proposition \(\operatorname{init}()\longrightarrow A_0\), we have \(A_0\). If \(H_i\) holds for every \(1\leq i\leq k+1\), then repeated use of Proposition \(A\xrightarrow{\mathrm{honest}}A\) gives \(A_k\), and Proposition check(), part (a), ensures that check() accepts.

Suppose instead that \(\neg H_i\) for some \(1\leq i\leq k+1\), and choose the minimal such \(i\). By minimality and repeated use of Proposition \(A\xrightarrow{\mathrm{honest}}A\), we have \(A_{i-1}\). If \(i\leq k\), then Proposition \(A\xrightarrow{\mathrm{dishonest}}B\) gives \(B_i\); repeated application of Proposition \(B\xrightarrow{\mathrm{any}}B\) gives \(B_k\), and Proposition check(), part (b), ensures that check() rejects.

If instead \(i=k+1\), then part (a) of the same proposition ensures the same result. \(\square\)

The gap in their proof (c.f. their Appendix E)

The paper starts its proof with the first read that returns an incorrect data value. It then considers an earlier read, which must have returned the correct data value, and infers that this earlier read returned the same pair that had been written:

A read can return the correct value with an incorrect timestamp. Consequently, the inference about the pair is not justified. This was the gap in their proof.