Juliana Furgala (MIT Lincoln Laboratory), Samuel Jero (MIT Lincoln Laboratory), Andrea Lin (MIT Lincoln Laboratory), Rick Skowyra (MIT Lincoln Laboratory)
Satellite systems provide crucial services for the modern world, including global position, navigation, and timing as well as world-wide communication, earth imaging for weather forecasting, and a host of other functions. Due to the critical nature of these services and their increasing importance, satellites are increasingly targeted by attackers, including both criminals and nation-state actors. Unfortunately, the software controlling these satellites has not been designed with security in mind due to the assumption that access is difficult. With the increasing commodification of space, that assumption no longer holds, leaving these systems exposed and vulnerable.
In this paper, we share our experience attempting to combine real flight software with a key security technology developed by the security community. In particular, our goal is to run NASA’s core Flight System (cFS) on top of the formally verified seL4 microkernel to eliminate vulnerabilities related to the operating system and provide a strong foundation for satellite software systems. While we were successful at doing so, it required more than a year of effort and the development of a significant set of operating system services beyond the seL4 microkernel. Along the way, we learned some key lessons about flight software and security technologies like seL4.