Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Cryptol: DSL for specifying cryptographic algorithms

cryptol.net

Post reply on HN
Print view View original

1–6 of 6 posts

Re: Cryptol: DSL for specifying cryptographic algorithms

#3

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

Re: Cryptol: DSL for specifying cryptographic algorithms

#4

Post by nickpsecurity »

tronracer wrote: post #2

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

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

Re: Cryptol: DSL for specifying cryptographic algorithms

#5

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

Re: Cryptol: DSL for specifying cryptographic algorithms

#6

Post by CHY872 »

tommd wrote: post #3

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…

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.
Post reply on HN