5 ms·

Cryptol: DSL for specifying cryptographic algorithms

50 points by xkarga00 11y ago

tronracer 11y ago
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_1_Web.pdf https://www.nsa.gov/research/tnw/tnw191/articles/pdfs/TNW_19...
- nickpsecurity 11y ago
  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 http://cryptol.net/files/empowering_the_experts.pdf
tommd 11y ago
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 11y ago
  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 11y ago
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/ https://galois.com/blog/ [2] http://leepike.github.io/Copilot/ http://leepike.github.io/Copilot/ [3] http://ivorylang.org/ivory-introduction.html http://ivorylang.org/ivory-introduction.html [4] https://galois.com/blog/2013/10/smaccmpilot-open-source-autopilot-software-for-uavs/ https://galois.com/blog/2013/10/smaccmpilot-open-source-auto...

50 points by xkarga00 11y ago

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_1_Web.pdf https://www.nsa.gov/research/tnw/tnw191/articles/pdfs/TNW_19...

nickpsecurity 11y ago
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 http://cryptol.net/files/empowering_the_experts.pdf

tommd 11y ago

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 11y ago
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 11y ago

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/ https://galois.com/blog/ [2] http://leepike.github.io/Copilot/ http://leepike.github.io/Copilot/ [3] http://ivorylang.org/ivory-introduction.html http://ivorylang.org/ivory-introduction.html [4] https://galois.com/blog/2013/10/smaccmpilot-open-source-autopilot-software-for-uavs/ https://galois.com/blog/2013/10/smaccmpilot-open-source-auto...