Securely refresh secret storage to resist side-channel leaks

Leakage-resilient cryptography protects secrets against side-channel attacks, in which a physical implementation reveals partial information about its internal state. A fundamental primitive in this area is a leakage-resilient storage, which allows a secret to be stored in a way that remains secure even if an adversary learns some information about the storage's internal state. A popular approach represents a secret as the inner product of two $n$-bit vectors, called shares. The shares are stored and processed separately by two parts of the implementation, called the left and right parties. Because leakage accumulates over time, the shares must be refreshed repeatedly. We prove that a simple refresh, in which the left party multiplies its share by a uniform invertible matrix $M$ and the right party multiplies its share by $M^{-1}$, is secure under continual local leakage. After $T$ refreshes, each allowing at most $λ$ bits of leakage per party, the transcripts for two stored secrets are at statistical distance at most $C\cdot T\cdot 2^{6λ-n/9}$ for an absolute constant $C$. We also obtain a Boolean-circuit compiler with statistical privacy error at most $C\cdot S\cdot 2^{18λ-n/27}$ for $S$ operations and at most $λ$ bits of local leakage per party per operation. The guarantee covers repeated stateful evaluations with adaptively chosen public inputs, with $S$ counting all operations across invocations. Thus, for polynomial-size circuits, a constant leakage fraction is tolerated with share length depending only on the security parameter. We formalize the refreshing bound, the composition and compiler guarantees, and the expected-work bounds in Lean 4. Our results also provide efficient simulation: the leakage can be reproduced from the public inputs and the circuit outputs alone, with expected polynomial overhead.