One of the goals of the SMACCMPilot project is to build a higher-assurance autopilot and to build languages and tools that make it easier to build other high-assurance systems.
The following sketches some of the requirements for SMACCMPilot and evidence we have that those requirements are met.
As of November 2013, SMACCMPilot is some 50k LOCs of C code and growing. (Because the C code is generated, this code is perhaps twice the length of comparable hand-written code.) Nonetheless, SMACCMPilot (or any fully-featured autopilot) will be tens of thousands or more of lines of code.
Our goal is to build an autopilot from-scratch quickly: our (end of) 2013 release represents only about 2 engineer years of development. Consequently, verification approaches that require significant manual labor (e.g., interactive theorem-proving) or that do not scale to large code-bases (e.g., model-checking) are not practical. Furthermore, we are taking a “green-field” approach rather than analyzing existing artifacts for bugs, so we want to do better than the “bug-hunting” approach found in unsound static analysis.
Our goal is increased programmer productivity and increased code assurance compared to typical embedded development projects.
Finally, our focus is to use open-source verification tools for our open-source project: we want the approaches developed here to be available to everyone interested in high-assurance software development.
SMACCMPilot is developed using Ivory and Tower, two domain-specific languages developed under the project. These languages improve programmer productivity but also ensure correctness properties by construction.
Ivory is designed to be expressive while providing evidence that the generated code does not contain undefined behaviors and memory-safety violations.
In addition, Ivory prevents various constructs that might be well-defined but often make code analysis more difficult, lead to bugs, or both. For example, the following properties hold for Ivory-generated code:
These kind of rules are reminiscent of JPL’s Power of 10 rules.
The Ivory compiler optionally instruments the generated C code with assertions. Current assertions checks are implemented for
We compile with
-Wall. Note that we in effect compile with
-Wall twice: once with our Haskell compiler (since Ivory is an embedded domain-specific language in Haskell), and once with our C compiler.
Additionally, we run the cppcheck lint tool on our generated (and hand-written) C and C++.
Tower lifts the level of abstraction in developing inter-communicating tasks (including device drivers). Tower helps to prevent
During development and internal deployment, we always execute code with assertions turned on always.
We have also implemented a QuickCheck harness for Ivory. We use QuickCheck to test some portions of SMACCMPilot, easily generating 100s of thousands of calls to C functions with random arguments.
We plan to extend our use of QuickCheck to more of SMACCMPilot in the future.
We have been using the open-source C model-checker CBMC. CBMC is an excellent model-checker for verifying C source code, and we have found bugs in SMACCMPilot using it.
However, it no longer scales due to the size of the code-base since it performs whole-program analysis.
We are currently in the process of writing a domain-specific model-checker customized to Ivory which we hope will scale better. Until then, there may be latent unchecked integer under/overflows or divisions-by-zero.
We have built a runtime verification framework. It automatically instruments C code to capture global state values whenever a variable changes. The framework is built using a combination of GCC plugins and Ivory macros for generating monitoring code based on past-time linear temporal logic assertions.
The framework is primarily intended for monitoring (and responding to failures) in untrusted C code.
SMACCMPilot consists of a large (and growing) number of libraries and application code. Here we briefly itemize the status of major components of the architecture in terms of their assurance and what a vulnerability might mean for the overall system.
Radio firmware: The 3DR radio firmware is currently written in C/assembler and should be considered to be not only untrusted but potentially buggy.
Ground control station (GCS): The GCS software has no particular assurance built into it. See below for more about cryptography and GCS communications.
ArduPilot libraries: SMACCMPilot currently relies on a small (and decreasing) amount of ArduPilot code for sensor input and filtering.
Board support package: SMACCMPilot relies on C drivers to interact with the PX4 hardware. These are being replaced with Ivory-implemented drivers, where possible.
libc: SMACCMPilot applications link to libc.
Build tools: of course, we rely on compilers like GCC, GHC (Haskell compiler), Make and linker scripts, all of which could introduce bugs. (If you are not afraid of compiler bugs, consider how many GCC bugs have been discovered by Csmith).
MAVLink: SMACCMPilot currently uses the MAVLink protocol to communicate with the GCS. Parsers and serializers are generated from XML specifications using a Python code generator. The parsers and serializers that are generated are Ivory programs, so they will have the memory-safety/well-defined properties that all Ivory programs have, but they may have logical bugs.
RTOS: see below.
crypto libs: see below.
The publicly available version of SMACCMPilot is built on FreeRTOS, a small, open-source, real-time operating system. FreeRTOS is written in C and is well tested and well documented; our experience is that it is highly-reliable.
We have developed an end-to-end encryption system for ground control system (GCS) communication. The design is based on a well-defined and studied standard, AES in Galois/Counter mode, and the implementations are built on top of open-source implementations in C and Haskell.
We do not currently have a key-distribution scheme implemented, so SMACCMPilot communication has all of the risks associated with using stale, leaked, or default keys.
The encryption/authentication SMACCMPilot firmware executes as a RTOS task, in the same address space as all of the other firmware. Thus, if an attacker gains access to the firmware binaries or discovers a memory safety vulnerability that allows her to read/overwrite arbitrary addresses, she can read/write the private keys.
However, assuming the following should hold of SMACCMPilot:
We have not addressed functional correctness of SMACCMPilot, except for small portions of the system, such as validating user inputs from the radio controller. Moreover, we have not developed a specification of autopilot correctness; doing so would be a research project itself.
The following are project goals related to increasing the assurance of SMACCMPilot: