[Cryptography] Swift and cryptography

[Bear]

On Tue, 2014-06-10 at 07:55 -0400, Jerry Leichter wrote:

> On the more general question of whether we need yet another programming
> language to add to the thousands we already have - well, it's not like
> people are going to stop developing new languages.  

Indeed.  Language hacking is, I think, a fundamental part of 
learning to master one's tools for a significant fraction of
programmers. There's a certain -- temperament? -- anyway, 
there's a set of very good coders that would never fully develop 
its skills without an opportunity to wrestle with programming 
language design as an art.  They're not the majority, and 
they have no exclusive on being highly skilled - but they're 
some of the visionaries and once in a while they do come up 
with a good idea.

> The ideal crypto implementation language has three features:  The
> ability to generate highly efficient code; the ability to control that
> code very closely (to prevent or at least control things like timing
> attacks); and a semantics that allows for formal verification (whether
> you actually do it right now or not; that's an indirect way of saying
> that the language's semantics is completely and tightly specified).  

'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.  

				Bear