[Cryptography] [FORGED] Re: How programming language design can help us write secure crypto code

[Mansour Moufid]

On Sat, Oct 24, 2015 at 9:35 PM, Ray Dillinger <bear at sonic.net> wrote:

> I would be in favor of an extended standard for "Crypto C" such
> that all code whose behavior is specified in C would be specified
> identically in Crypto C, no new syntax or keywords would be
> introduced, and most of things that are left unspecified in the
> C standard would be either guaranteed to be compile-time errors
> or specified with an exact semantics.

Check out Clight and CompCert:

http://pauillac.inria.fr/~xleroy/publi/Clight.pdf
http://compcert.inria.fr/

I compile large projects like Tor using CompCert with a simple
"./configure CC=ccomp" and the results are just as fast.

As a bonus, CompCert has an "interpreter" that can find undefined
behaviour for you.