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).
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.
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.
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.
> 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.
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...
"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.
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 :)
> 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.
> I erroneously assumed that it's intended to address implementation errors (that is to replace C or asm implementations with something easier to code).
Indeed, and those are absolutely things we need to watch out for when building backends suitable for direct implementation.
> 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.
Agda and Coq are both much more general-purpose and powerful in terms of the types of programs and theorems they can express. Cryptol is specialized toward theorems involving functions that manipulate sequences of bits. As a result, it's much easier to start Cryptol up and prove properties of crypto algorithms, but you aren't able to express the range of theorems that you can in a dependently-typed language.
For example, Cryptol lets you write polymorphic functions and theorems, but if you wanted to prove something about such a function:
plus_id : {a} (fin a) => [a] -> Bit
plus_id x = x + 0 == x
You'd first have to instantiate `a` to some concrete size, rather than proving it for all `a`, which would be a beginner-level proof in Coq or Agda:
Main> :prove plus_id
Not a monomorphic type:
{a} (fin a) => [a] -> Bit
Main> :prove plus_id : [32] -> Bit
Q.E.D.
So overall I'd say it's the classic story of the tradeoffs of a DSL. It's easier to get up, running, and proving things within the domain, but the domain itself is more restricted.
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.)
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).
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.
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.
"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."
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).