[Cryptography] Secure erasure in C.
hbaker1 at pipeline.com
Mon Sep 12 18:30:57 EDT 2016
At 08:08 AM 9/11/2016, Henry Baker wrote:
>As many people have pointed out, the problem with erasure is that it deals with a concept not captured by normal programming languages, operating systems or computing hardware.
>Programming languages deal with *returned values* and *variable values*, and so long as these values achieve the desired bit patterns, everyone is cool. No one cares about the values of (supposedly) "dead" variables which can "never" be referenced.
>There is a formal notion from the lambda calculus about all of this: so-called "lazy evaluation". Lazy evaluation never attempts to evaluate an expression until it is *absolutely necessary for the ultimate output value*, out of fear that this expression will loop or err out. Lazy evaluation is the ultimate "leave sleeping dogs lie" approach to computation.
>A *lazy architecture* would *never* actually clear a variable value unless that variable value participated in a computation leading to a final result. So the whole concept of "secure erasure" is meaningless in this computing model.
I should have pointed out that there is a *general* procedure for compiling a computation into a form where you can *force* evaluation in the order (i.e., including forcing the evaluation of sub-expressions that might not otherwise be evaluated) of your choice.
The result of this general procedure is the program rewritten in "continuation-passing style".
In particular, continuation-passing style forces the computations that you want even in the presence of a *lazy evaluator*. This is because continuation passing style *linearizes* the computation in such a way that the compiler has no choices about what to evaluate next, and *all* of the results are passed -- either directly or indirectly -- as arguments to the next portion of the computation in such a way that the compiler can't avoid performing the computation.
Furthermore, continuation-passing style also works in C:
Continuation-passing style ("CPS") *looks* (after careful formatting) very like assembly language; indeed, Andrew Appel (who has also hacked voting machines) wrote an entire book on how to efficiently compile languages using CPS intermediate forms.
So, if you have a variable XXX that you want to set to zero and be certain that the compiler won't optimize this setting to zero, you arrange the computation in such a way that this variable is passed as an argument (probably in the form &XXX) to the *continuation* procedure of the rest of the computation. Thus, if the computation proceeds anywhere at all, it must proceed to this continuation, and the semantics of C require that the value of XXX actually be zero when it enters that continuation procedure.
I don't presume to imply that the C programs so produced are completely readable(!), but readability is often over-rated when humans read code and miss obvious errors -- e.g., the famous Apple "goto fail" bug.
The important point here is that both lambda lifting and CPS conversion are rigorous *algorithms*, so they can be thoroughly vetted.
If no one in the crypto community is aware of continuation-passing style (DJB: are you listening?), then perhaps I should go through some of the NaCL/libsodium code and demonstrate how CPS might be helpful in nailing down the semantics.
More information about the cryptography