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

[Henry Baker]

At 06:35 PM 10/24/2015, Ray Dillinger 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.

John Launchbury (currently at DARPA) has already developed
a safer language & compiler for crypto code called "Cryptol".

It is more bit-twiddling than C; in fact it can compile into
FPGA's in addition to compiling into assembly language.

I haven't used it myself, but it's open source so you can
try it out:

https://github.com/GaloisInc/cryptol

http://www.darpa.mil/staff/dr-john-launchbury

http://galois.com/project/cryptol/

https://www.youtube.com/watch?v=hcbg2PL6TRM

http://dl.acm.org/citation.cfm?doid=2047862.2047894

http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.232.7971&rep=rep1&type=pdf

http://www.csiir.ornl.gov/csiirw/09/CSIIRW09-Proceedings/Slides/Erkok-slides.pdf

etc.