Cryptol: DSL for specifying cryptographic algorithms

Some recent happenings in Cryptol land include:

  * Dylan recently released a literate Cryptol version of the CFRG's ChaCha20/Poly1305 document.  Very cool to see more Cryptol code like this.
  * Merged the fork of SBV with upstream.
  * ABC is now a supported prover.
  * Support for parallel (first to finish) proving using ':set prover=any'.
  * The type checker has been revamped for v2.3, so we should see simpler constraints "soon".

It's another amazing piece of work largely developed by Galois Inc: a company that invents and develops great stuff on a regular basis. One of the few doing high assurance. Their blog [1] is a gold mine of their interesting work and tips.

Two other works HN readers might like are Copilot [2] and Ivory [3]. Copilot is a DSL for distributed monitors and real-time systems. The result is QuickCheck'd, model-checked, hard, real-time C. Ivory is a DSL that embeds a subset of C into Haskell to leverage its power and increase safety. It was used in the SMACCMPilot UAV program [4], which is open source.

[1] https://galois.com/blog/

[2] http://leepike.github.io/Copilot/

[3] http://ivorylang.org/ivory-introduction.html

[4] https://galois.com/blog/2013/10/smaccmpilot-open-source-auto...

Cryptol was originally designed for the NSA. There's a good article on it in NSA's The Next Wave from 2011 [1], which is also linked under documentation.

[1] PDF: https://www.nsa.gov/research/tnw/tnw191/articles/pdfs/TNW_19...