4 ms·

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 any

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/ http://ivorylang.org/ [1] Second, the flight control software we wrote for the 3DR Iris+: http://smaccmpilot.org/ 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.

eggy 10y ago
Glad to hear you say that. Aside from that the work seems very interesting. I am going to check out Ivory. I have been reading up and playing with Idris and F. I like F so far, and that you can output F# and OCaml. Idris's goals seem in line with what you were originally looking for. Have you evaluated it?
- eggy 10y ago
  [Edit] Replying to my post to edit, since no choice given to edit. Should say "I like Fstar" above, but asterisk turned on italics...
- acfoltzer 10y ago
  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-functional-programming-idris-1-3/ 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 :)
  - eggy 10y ago
    Sounds great. I'll check out the talks link and Ivory some more. Thanks!
fmap 10y ago
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.
- acfoltzer 10y ago
  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 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.
unboxed_type 10y ago
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) ?
- acfoltzer 10y ago
  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.

eggy 10y ago

Glad to hear you say that. Aside from that the work seems very interesting. I am going to check out Ivory. I have been reading up and playing with Idris and F. I like F so far, and that you can output F# and OCaml. Idris's goals seem in line with what you were originally looking for. Have you evaluated it?

eggy 10y ago
[Edit] Replying to my post to edit, since no choice given to edit. Should say "I like Fstar" above, but asterisk turned on italics...
acfoltzer 10y ago
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-functional-programming-idris-1-3/ 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 :)
- eggy 10y ago
  Sounds great. I'll check out the talks link and Ivory some more. Thanks!

fmap 10y ago

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.

acfoltzer 10y ago
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 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.

unboxed_type 10y ago

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

acfoltzer 10y ago
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.