Trustworthy software in the real world

*
Accepted Session
Short Form
Intermediate
Scheduled: Tuesday, June 23, 2015 from 1:30 – 2:15pm in B204

Excerpt

Software is made of bugs, yet software is controlling a growing part of our physical world. As bugs and security holes become potentially life-threatening, what can we do to make our software worthy of the trust we're placing in it?

Take quadcopters, for example. Toy vehicles are not just in specialty hobby shops but even in supermarkets; sports stadiums and the White House are trying to find ways to keep them out; and everyone from agriculture startups to Amazon wants to use them commercially. Quadcopters are becoming safety and security critical systems, but how are we going to make them truly safe and secure?

I'll present SMACCMPilot, a BSD-licensed high-assurance quadcopter autopilot, and the new tools and technologies that make it feasible to trust a large piece of software.

Description

With this proliferation of Unpiloted Aerial Vehicles (UAVs) comes a growing number of stories of UAVs appearing in places they shouldn’t (such as the White House lawn), or being commandeered in flight (such as in Iran in 2011). On the other hand, the December 2013 announcement of Amazon Prime Air demonstrated that there is a huge potential market for safe commercial pilotless vehicles. What to do?

Many of the safety and security challenges for UAVs are no different than for any software system: buffer overruns, missing or broken cryptography, and all the other bugs we’ve come to expect. In 2012, DARPA program manager Dr. Kathleen Fisher launched a program called HACMS to explore new ways to address these systemic software flaws. One outcome of that program is the high-assurance quadcopter autopilot called SMACCMPilot, written primarily by my colleagues at Portland software firm Galois.

SMACCMPilot, a BSD-licensed project hosted publicly on GitHub, is a proof of concept demonstrating several techniques for writing high-assurance software. A key technology is our Ivory embedded domain-specific language (also BSD-licensed), which acts as a verified safe subset of C. Because Ivory is embedded in Haskell, however, we’re also able to use the full power of Haskell as a macro language to generate code that would be complex and error-prone to write by hand. We run the resulting software on an STM32F4 microcontroller, which is too small to even run Linux but more than enough for the C that Ivory generates.

Other key technologies that Galois and our partners in the HACMS program have used include proper cryptography (obvious, yet missing from a surprising number of UAVs); formally-verified microkernels such as GPL-licensed seL4; and theorem provers and SMT solvers to verify that run-time assertions can’t actually fail under any inputs.

This sounds like deep magic, and some of it is—but we’ve found that these techniques are coming within reach of programmers outside academia. For example, non-Haskellers at Boeing have successfully used Ivory’s C-like concrete syntax to implement level-of-interoperability for the Stanag 4586 standard for UAV communication, and many properties of interest in Ivory programs can be automatically proven using cvc4, an open source SMT solver.

The end result: quadcopters running an earlier version of SMACCMPilot were called the most secure unmanned aerial system in the world after analysis by red-team penetration testers. 60 Minutes published a demonstration of SMACCMPilot in February as part of their coverage of DARPA’s I2O programs office, which includes the HACMS program. And the Security Now podcast interviewed us in March.

I’ll give you a taste of what it’s like to create large software systems that are trustworthy. Try these tools yourself: you may find that this is how you want to develop software too!

Tags

high-assurance, Haskell, domain-specific languages, microcontrollers, real-time operating systems, cryptography, quadcopters, C

Speaking experience

This is a new talk. I've spoken at Open Source Bridge several years, as well as a variety of other tech conferences going back to 2001, including USENIX and the X.Org Developers' Conference.

Speaker

  • Jamey is climbing the halls

    Biography

    Jamey Sharp was placed on Ritalin, briefly, in fifth grade. His interests and activities have been varied ever since. His biggest projects have been the Portland State Aerospace Society, a student rocketry club at Portland State University; XCB, a new low-level binding to the X protocol, in the process of replacing Xlib; and Comic Rocket, because his other projects didn’t leave him enough time to read his favorite webcomics without tool support.

    Jamey’s interests span computer science fields including cryptography, combinatorial search, compilers, and computational complexity; systems-level programming, such as file format and network protocol implementations, Linux kernel development, and boot-loader hacking; computer architecture and its impact on software design; and functional programming, preferably in Haskell.

    Sessions

      • Title: Trustworthy software in the real world
      • Track: Hacks
      • Room: B204
      • Time: 1:302:15pm
      • Excerpt:

        Software is made of bugs, yet software is controlling a growing part of our physical world. As bugs and security holes become potentially life-threatening, what can we do to make our software worthy of the trust we’re placing in it?

        Take quadcopters, for example. Toy vehicles are not just in specialty hobby shops but even in supermarkets; sports stadiums and the White House are trying to find ways to keep them out; and everyone from agriculture startups to Amazon wants to use them commercially. Quadcopters are becoming safety and security critical systems, but how are we going to make them truly safe and secure?

        I’ll present SMACCMPilot, a BSD-licensed high-assurance quadcopter autopilot, and the new tools and technologies that make it feasible to trust a large piece of software.

      • Speakers: Jamey Sharp