Cryptol: DSL for specifying cryptographic algorithms

[tommd]

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

[CHY872]

Parallel proving should be a big bonus. Nipkow found that on the Isabelle test set, using 3 theorem proves in parallel gave as good results in 5 seconds as the best among them gave in 120.

[nickpsecurity]

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

[tronracer]

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

[nickpsecurity]

It was. It's since been used by all sorts of groups and open sourced. One of the few, good things that come from NSA's Information Assurance Directorate. Btw, below is a better link that isn't sideways and full of NSA's crap.

http://cryptol.net/files/empowering_the_experts.pdf