[Cryptography] Secure erasure in C.

[Henry Baker]

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.

https://en.wikipedia.org/wiki/Continuation-passing_style

Furthermore, continuation-passing style also works in C:

http://home.pipeline.com/~hbaker1/CheneyMTA.html

http://home.pipeline.com/~hbaker1/CheneyMTA.pdf

---

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.

https://books.google.com/books/about/Compiling_with_Continuations.html

---

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.

There is a technical issue in the C language due to the fact that C doesn't support *full closures* like Pascal or Javascript; i.e., C supports only *global variables* and *argument variables*.  However, there is further well-known procedure (called "lambda lifting") which collects up all of the variables which might have participated in an actual closure, and passes them as additional arguments.  Thus, through a combination of lambda-lifting and continuation-passing style, a C program can be forced into a form where the optimizer is no longer free to elide computations it considers unnecessary.

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.