Comment by acfoltzer | Hacker News Reader

Comment by acfoltzer | Hacker News Reader

Parent Full thread

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

Reply on news.ycombinator.com