I'm one of the researchers at Galois who's working on the quadcopter platform for HACMS. Let me first say that this headline makes me cringe just as much as anyone. I'd also like to give folks a pointer to some of the work we've developed on the project–it's all open source.
First we have Ivory, the DSL for doing safe systems programming that takes buffer overflows and other memory-safety bugs off the table: http://ivorylang.org/ [1]
Second, the flight control software we wrote for the 3DR Iris+: http://smaccmpilot.org/ The adventurous among you who fly with a Pixhawk can build it and try it out yourselves, and we'd love to hear your thoughts.
[1]: When we began work on HACMS, Rust was around but nowhere near mature enough to base a proposal on. These days, it covers a lot of the same bases, although currently Ivory is more suited for formal analysis with SMT solvers and model checkers.
The goals of Idris and similar languages are different from the goals we had with Ivory, though. We sometimes describe Ivory as "medium-assurance" as opposed to the high assurance one can get from a language with a more expressive type system.
It makes sense for some systems or components to be formally verified, for example the seL4 verified microkernel which is also used on our copter. However we simply would not have been able to formally verify (or even get to typecheck with fancier dependent types) something on the scale of an autopilot given the resources we had on the project. Instead we rely on getting quite a bit of bang for the buck with the memory safety features, and then augment with assertions.
We ended up with a working autopilot (and board-support package with drivers) in only ~4 engineer-years, so we think the tradeoff is working well so far :)
This is very interesting work! Do you have axiomatic semantics for Ivory and Tower, and/or specifications for SMACCMPilot? If so, it might be interesting to show specification preservation from Ivory to the Verified Software Toolchain (I'm just assuming that Ivory targets some C subset compatible with Verifiable C). With the ARM backend of CompCert this would give high assurance right down to the machine code.
In any case, I found your experience report to be very well written and would love to hear more about this project.
You might find our more recent Haskell Symposium paper of interest if you're interested in semantics (this is also a good reminder for us to update the webpage with a link): https://www.cs.indiana.edu/~lepike/pubs/ivory.pdf
Essentially, we built an Isabelle/HOL model of a Core Ivory language, and then used those semantics to prove type safety through the usual progress and preservation.
We don't have specifications of the higher-level properties of SMACCMPilot at the Ivory/Tower level. Instead our partners at Rockwell Collins are developing AADL specification and analysis tools to prove system-level properties at the architecture level.
Hello!
What are the reasons one would want to write C code in Haskell DSL instead of supplying ones C code with annotations and proving those annotations semi-automatically instead
(Frama-C) ?
Most people I know who have tried to write large-scale software with annotation techniques have stories that scare me away from ever wanting to experience such. As I mention in another comment, we sometimes describe our goal with Ivory as "medium assurance". In this sense, we are not precisely modeling the functional properties of the code, but rather use the combination of memory safety and occasional automatically-proved assertions to rule out the large classes of software defects/vulnerabilities that plague typical embedded software.
Another reason is simply productivity. Since the DSL is hosted within Haskell, we get the benefit of a fully-featured, expressive language for metaprogramming and abstraction of Ivory/Tower code. This has been crucial for letting us produce a functional autopilot (and board-support package/drivers) in only ~4 engineer-years.
We also have a stand-alone concrete syntax for Ivory that is intended to be more familiar to C/C++ programmers. It's being used heavily by our partners at Boeing on their Unmanned Little Bird. While they aren't reaping as many of the abstraction benefits as users of the EDSL, the fact that they can mostly focus on writing type-correct code vs. figuring out correct annotations makes them quite productive still.
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.)
First we have Ivory, the DSL for doing safe systems programming that takes buffer overflows and other memory-safety bugs off the table: http://ivorylang.org/ [1]
Second, the flight control software we wrote for the 3DR Iris+: http://smaccmpilot.org/ The adventurous among you who fly with a Pixhawk can build it and try it out yourselves, and we'd love to hear your thoughts.
[1]: When we began work on HACMS, Rust was around but nowhere near mature enough to base a proposal on. These days, it covers a lot of the same bases, although currently Ivory is more suited for formal analysis with SMT solvers and model checkers.