[Cryptography] Secure erasure

[Henry Baker]

At 05:19 PM 9/8/2016, Arnold Reinhold wrote:
>Imagine for a moment what might be possible if the toolmakers were actually trying to help instead of sticking to a language spec largely from the PDP-11 era.  One might add a "zeroizable" keyword, for example.  All that code generation ingenuity could be applied to not only insuring the code that erases zeroizable data was not elided, but also to keeping track of copies, and even minimizing their creation.  The compiler might be able to recognize when the data in question was no longer needed it and erase each copy of it at the earliest instant.  Object destructors could reliably destroy.  Pragmas could prevent optimization of critical code.  Leaky constructs, such as storing zeroizable data in flash, could be flagged. And so on.

There *is* such a computer language notion: so-called "linear" types.

A "linear" object is one which has exactly one reference, and the language and type system conspire to ensure that this constraint is preserved.

*You* (the programmer) can make a copy of the *contents* of such an object if you wish, but the compiler & run-time system are not allowed to make such a copy.

Similarly, you -- the programmer -- are allowed to destroy "the" reference to such an object (thereby also destroying the object itself), but the compiler and run-time system are not allowed to perform such destruction on their own.

Properly implementing linear types requires a whole new approach to compilers and operating systems, because both are typically quite profligate in their explosion of copies -- e.g., nearly ubiquitous caching.

Note also that the *lack of specific destruction* requirement places severe constraints on control flow: if a subprogram creates a new linear object, it cannot exit without providing a proper resting place for the linear object.  If the linear object cannot be (or is not) returned as a value, or assigned to a global variable, or explicitly destroyed, then the program must terminate with an error -- and the linear object is still preserved.

In short, the linearity constraint is not just a "hint" or "recommendation", but a *requirement* that -- if not possible to achieve -- requires that the computation halt.

Lisp programmers will see the need for an implicit "unwind-protect" construct to handle such errors; in other languages, variations on a "try" construct (but with more stringent assurances) will be required.

Here are some references re linear types, along with some programming examples.

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

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

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

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

https://en.wikipedia.org/wiki/Linear_types

https://en.wikipedia.org/wiki/Exception_handling