F-Store — Shared storage with erasure
F-Store (Shared storage with erasure) is part of Idealized Setup and Resources in the UC functionality encyclopedia. Status: an idealized setup assumption or shared resource.
F-Rand’s companion: where a randomness source produces values and lets them be forgotten, a store takes values and holds them until they are. A party puts a value at an index, gets it back, and can erase it; an erased index is reusable. Together the two are what lets a protocol keep no persistent state on its own machine tape — draw coins through F-Rand, keep everything else through F-Store — so that whatever the adversary can read off a corrupt party’s leakage is exactly what these two functionalities choose to expose, and nothing hidden in an implementation’s memory besides.
Functionality
Reading the box: two markers do the work of three conditions — \(\square\) is an index never written, \(\bot\) is one written and since erased, and anything else is a value put and still there. The refusals are written as requires rather than as returns of \(\mathsf{rej}\); the framework answers a refused require with \(\mathsf{rej}\) of its own accord.
- \(\mathtt{L} : \mathbb{N} \to \{0,1\}^* \cup \{\bot,\square\}\)
- \(\mathtt{L}[*] \gets \square\)
- \(\textbf{require}\ \mathtt{L}[i] \in \{\bot,\square\}\)// an occupied index refuses
- \(\mathtt{L}[i] \gets x\)
- \(\textbf{return}\) ok
- \(\mathtt{L}[i] \gets \bot\)
- \(\textbf{return}\) ok
- \(\textbf{require}\ \mathtt{L}[i] \neq \square\)// never written refuses
- \(\textbf{return}\ \mathtt{L}[i]\)// \(\bot\) if erased
- \(\textbf{return}\ \mathtt{L}\)
The box is transcribed from UC for Gamers (§14.1, p. 140), line numbering and all.
The three conditions are kept apart on purpose. A caller can tell “nothing was ever here” from “something was here and is gone”, where a store that answered the same either way could not be asked whether an erasure actually happened — which is precisely the question a protocol relying on erasure needs answered. That is why Get refuses \(\square\) (line 8) but happily returns \(\bot\) (line 9): the refusal means “wrong index”, the \(\bot\) means “gone”, and collapsing them would lose the distinction the state was built to carry.
Lines 3 and 8 are the only two refusals a store owes. Put refuses an occupied index, so a value cannot be silently overwritten — an erasure has to be asked for explicitly. Erase refuses nothing at all: erasing an index that holds nothing is a harmless no-op, and making it fail would only give a caller a way to probe the table.
State is shared across every party the instance serves, exactly as for F-Rand: one party may retrieve what another put, which is what makes this a shared store rather than a per-party tape.
Known realizations
An idealization of ordinary local storage together with a secure-erasure primitive; nothing computational realizes the erasure guarantee exactly, since a real machine’s memory is not erasure-transparent the way this functionality’s \(\mathsf{gone}\) marker is. It stands in, in a protocol write-up, for “this value is kept on the party’s own tape until explicitly deleted.”
Properties
Two properties, proven with probability exactly \(0\) (information-theoretic, no adversary strategy succeeds at all):
- Persistence. A value put and not erased is the value later got back — no get ever returns anything other than the last successful put at that index, so long as no erasure intervened.
- Erasure. A value that has been erased is never got back — no get ever returns the value an erasure removed, so long as no later put restored it first.
Both hold against every occupant of the adversary slot, not just a canonical one, since (as with F-Rand) the functionality places no calls of its own for an adversary to interfere with.
Formal artifacts
No machine-checked formalization yet.
References:
- UC for Gamers, this site’s own book draft on composable security. Chapter “Storage” gives the functionality above and both properties in full.