Cryptol DSL, a tool for writing correct crypto algorithms, is now open-source

http://www.cryptol.net/

by carterschonwald • 12 years ago

181 24 12 years ago

cryptol.net

mef• 12 years ago

www. subdomain seems broken.

http://cryptol.net/ works

tel• 12 years ago

Cryptol is REALLY cool. I followed its genesis from the Haskell community as it was primarily developed at Galois. Cryptol can be compared to Haskell somewhat neatly as similar with a significantly enhanced type system capable of representing more cryptographically important notions.

For anyone with an interest in Haskell, security, and/or dependent types it's worth taking a closer look at Cryptol.

thirsteh• 12 years ago

In case it wasn't clear, the DSL itself is also written in Haskell.

higherpurpose• 12 years ago

The Cryptol specification language was designed by Galois for the NSA's Trusted Systems Research Group as a public standard for specifying cryptographic algorithms.
In addition, much of the work on Cryptol has been funded by, and lots of design input was provided by the team at the NSA's Trusted Systems Research Group, including Brad Martin, Frank Taylor and Sean Weaver.

https://github.com/GaloisInc/cryptol

ape4• 12 years ago

And it sounded so promising.

a-saleh• 12 years ago

Hey, NSA is quite big :-) I remember reading how one branch of NSA tasked with strenghtening of TOR crypto was angry at anothe branch of NSA that tried to covertly introduce vulnerabilities to it...

tlrobinson• 12 years ago

If I understand correctly, this is meant to be used to help implement existing known good crypto algorithms correctly, not help design new crypto algorithms, which you absolutely should not do unless you're one of the few (thousand? hundred? dozen?) qualified to do so.

m0nastic• 12 years ago

No, it's useful for both.

Here's a presentation they gave in 2012 about Cryptol that does a pretty good job explaining it:

http://2012.sharcs.org/slides/hurd.pdf

ertdfgcb• 12 years ago

I think Cryptol will make it much easier to become qualified to write crypto because it makes the programming more similar to the math. Your average programmer will be able to start learning how to implement crypto from a much more rigorously mathematical standpoint, and inexperienced developers will write safer code. Seems pretty neat.

Sephr• 12 years ago

I'm getting NXDOMAIN on the www link. Change it to the bare domain.

acfoltzer3• 12 years ago

It should be working again within minutes; sorry for the DNS snafu.

krick2• 12 years ago

I don't know how to take it.

"A Cryptol implementation of an algorithm resembles its mathematical specification more closely than an implementation in a general purpose language."

So it's some easy-to-read DSL (at least from the authors perspective, but whatever). Well, yeah, it's cool. But there're many cool DSLs. And here we're talking about cryptography, that dangerous mystical beast. It's tricky. Many of those algorithms are invented with hardware performance in mind. So "who uses it" isn't really enough this time. There should be at least implementations of the most widely used algorithms and comparison of those from, say, OpenSSL. Are they fast enough (and on which platforms/architectures)? How complicated machine code is actually produced by this DSL? Aren't there some tricky issues with it, like, say, counting cash misses? Timing attacks? Power attacks? If so, are OpenSSL implementations doing any better? Or maybe they are even worse somehow?

It isn't something that makes me think "Wow, that's cool! I should use it in my next project!" the very moment I see it. It should be explored, and I think the authors are first who should provide some info on how safe is it.

acfoltzer3• 12 years ago

You're dead on. Cryptol is meant first and foremost as an executable specification language. There's an interpreter so that you can run your algorithms on concrete values to make sure that, for example, your test vectors check out. There's also a symbolic simulator for building formal models of the functions you define, so that you can prove properties about those programs using SMT.

Previous versions of Cryptol included backends for producing C and VHDL for higher-performing implementations on CPUs and FPGAs. Cryptol 2 is a ground-up rewrite and those backends aren't there yet, though we have plans to be working on new backends soon.

Cryptol is largely focused on issues of functional correctness. For power and timing attacks, you might want to build a C or Assembly implementation by hand that addresses those. However, what you're left with is fairly difficult to reason about on the level of functional correctness. We have another project, the Software Assurance Workbench, that builds formal models from LLVM and Java code. With this in hand, you prove equivalence between the hardened, high-performance implementation and the Cryptol specification.

Does that help clarify the role Cryptol might play in a cryptographer's workflow? Also, could you elaborate about your "how safe it is" question? I'm happy to answer :)

krick2• 12 years ago

Does that help clarify the role Cryptol might play in a cryptographer's workflow?

Yes, thank you very much. I erroneously assumed that it's intended to address implementation errors (that is to replace C or asm implementations with something easier to code). The "safety" I meant is irrelevant in case of "theorem prover" of course.

As I understand it's pretty unique tool in sense of easiness to generate VHDL specifications and such (as well as pretty DSL itself), as it's explained nicely in the presentation m0nastic reported on ( http://2012.sharcs.org/slides/hurd.pdf ). But, anyway, could you compare it somehow to the other "proving" tools that already exist, say Agda or Coq? I'm not expecting some specific information, just curious.

RolfRolles• 12 years ago

I think some timing attacks could be reasoned about in a formal context. You could model the timing details of a given CPU and then prove that two assembly language functions were indistinguishable with respect to that model. (For example, in the case of a comparison function that bailed out early when it found a difference leading to a timing discrepancy, you could replace it with a `for` loop like `for(i = 0; i < size; ++i) mismatch_ctr += src[i] != dest[i]` and then prove that the function takes the same amount of time regardless of whether `src` and `dst` are identical.)

azinman2• 12 years ago

Looks neat. We need more simple and verifiably correct cryptographic primitive frameworks that people can build upon to help secure the world. It'll take another 10-15 years before industry catches up.

The DSL allowed me to find a (trivial) error in the SHA-1 spec -- the description says 0 <= t < 79, but below they allow for 0 <= t <= 79 (which is also the cryptol implementation).

dylanmc2• 12 years ago

Nice catch! We noticed that error as well but didn't want to poke the NIST folks in the eye on the web page -- we're hoping to win them over with Cryptol, not put them on the defense. We're planning to submit an errata report on their website next week.

dfc• 12 years ago

How many more errors are you planning on submitting to NIST?

jfindley• 12 years ago

This looks really great - not only is the tool itself very useful, but I was surprised to find that it comes with what appears at first read to be really good documentation, with plenty of examples. More software should have docs like this (although a html version of the PDF would be nice).

platz• 12 years ago

Reminds me of TLA+ but for crypto

elo02• 12 years ago

"In addition, much of the work on Cryptol has been funded by, and lots of design input was provided by the team at the NSA’s Trusted Systems Research Group, including Brad Martin, Frank Taylor and Sean Weaver."

SonOfLilit• 12 years ago

TL;DR Cryptol is an amazing tool for communicating crypto specifications with your peers, for testing crypto implementations and for doing crypto research and formal verification. It has the most amazing and practical use of a SAT solver I've ever seen.

I've touched it briefly a very long time ago, so don't believe me blindly, but this is my impression of what Cryptol is about in practice:

* If you're publishing a paper on a new cryptographic building block, lets call it AES2, you need to specify it. Instead of using the usual math-oriented pseudo-code or unreadable-to-your-peers C, you can use the Cryptol DSL, which looks familiar to your readers but can be executed and toyed with.

* If you're implementing AES2 (be it in Cryptol, C, VHDL or assembly language) you can ask the Cryptol runtime to verify it against another implementation (usually a Cryptol implementation taken from the paper on AES2, but you could write your own or use an existing implementation in another supported language). The Cryptol runtime may be able to tell you if they are mathematically identical (and I do mean mathematically: this is not unit testing but proving identity). I say "may" because not every function can be verified this way - that would solve the proven unsolvable Halting Problem. This is implemented by translating the tested implementations to logic circuits and using a SAT solver to prove that their XOR is constant 0. (Please take a moment to reflect on how awesome this is.)

* If you're researching crypto, it gives you a programming language and toolset very fit for experimenting with cryptographic building blocks and running the sorts of statistical tests that you'd want to run on them in the process of research. It also gives you tools for formal verification (mathematically proving properties of your AES2 proposal in a way that a computer can verify is error-free).

* In theory, you can compile a Cryptol specification to optimized C or VHDL and use that in your project. acfoltzer said in this thread that Cryptol 2 is a rewrite and the compiler still isn't done (it was for Cryptol 1).

In a sane world, crypto journals and standards institutes would not accept proposals of new crypto building blocks that don't come with Cryptol code, and implementations would always use the Cryptol toolset to automatically mathematically verify that their implementation is identical to the published specification, eliminating many classes of implementation bugs.

This wouldn't have prevented Heartbleed, which isn't a crypto implementation bug.

Cryptol DSL, a tool for writing correct crypto algorithms, is now open-source

Related Stories