acfoltzer · HackerTrans

10 ปีที่แล้วdiscuss

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.

acfoltzer

10 ปีที่แล้วdiscuss

Thanks for the kind words!

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.

acfoltzer

10 ปีที่แล้วdiscuss

Indeed, we're fans of Idris here, and even hosted a series of Idris tech talks: https://galois.com/blog/2015/01/tech-talk-dependently-typed-...

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

acfoltzer

10 ปีที่แล้วdiscuss

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.

acfoltzer

12 ปีที่แล้วdiscuss

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

acfoltzer

12 ปีที่แล้วdiscuss

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

acfoltzer

12 ปีที่แล้วdiscuss

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

comments