Cryptography DSL.

Lifted from a press release issued back in 2008.

Cryptol is a domain specific language for the design,
implementation and verification of cryptographic algorithms,
developed over the past decade by Galois for the United States
National Security Agency. It has been used successfully in a
number of projects, and is also in use at Rockwell Collins, Inc.

Domain-specific languages (DSLs) allow subject-matter experts to
design solutions in using familiar concepts and
constructs. Cryptol, as a DSL, allows domain experts in
cryptography to design and implement cryptographic algorithms
with a high degree of assurance in the correctness of their
design, and at the same time, producing a high performance
implementation of their algorithms.

Note: I am not in any way affiliated with Galois inc, and not, myself, a user of the Cryptol language. I'm posting it because I thought LtU might find this an interesting thing to discuss.

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Nice find

Thanks for taking the time to post this.


I've been following Galois's work for a while. They've done quite a few things with Haskel and DSL's for highly assured systems. The CRYPTOL system allows domain experts to specify the algorithms, then a "correct by construction" implementation can be generaged in C, VHDL and maybe others. I think it's also compatible with the formally verified AAMP7G system. I wonder if a variation of the tech could be used to easily generate a bunch of non-crypto algorithms for the Verified Software Repository.

many interesting articles here