Recently on the cryptography list, people were discussing the requirements of a good programming language for doing cryptography and security.

My insight into this problem is that there are crucial, meaningful, requirements that cannot be described in terms of formal semantics.

‘Safety and formal verification’ are well studied semantic issues valuable to all langauges and not more valuable to a crypto/security language specifically than they are in general. But if you’re creating a cryptography and security language you need more than safety guarantees. You need security guarantees that are ignored by (indeed irrelevant to) current models of formal semantics, and which might be very hard to define in Coq or its equivalent.

Arguably these aren’t ‘semantic’ requirements at all because you could violate them hard and produce an implementation that always produces the same visible results given the same input, and that’s why modern formal semantics models cannot be defined in terms of them. So I’m going to use the term ‘quasi-semantic’ to describe them.

Any cryptography/security language needs absolute control over the lifetime and location in the machine of data. Specifically, a crypto language needs a quasi-semantic requirement that any operation rendering data unavailable to the program, including but not limited to subroutine returns, freeing of dynamic memory, overwriting values, deletions from or replacements in data structures, last use of a namespace, scope, or environment, or releasing the last pointer to a garbage-collected structure, etc, overwrites that data in memory making it unavailable to any tool that can be run on the machine including binary examinations of the running program image or disk image, and does so immediately, before the next program step is executed. And of course that includes also program exit and/or abort, where the next step is handing control back to the operating system.

It also needs a quasi-semantic guarantee that program data is never copied anywhere unless the program itself directs the copy to be made. A language implementation allowing the operating system to do “normal” paging and swapping of running programs would be non-compliant with the spec. No ‘debug’ environment allowing inspection of variable values could also be a compliant implementation, although it could otherwise be a simulation of one.

This means a whole class of optimizations will be things you can’t do, and will make any garbage collection agonizingly slow.

But that’s the price you pay for knowing that confidential data that you’re trying to protect is in fact being protected.