seROS: Securing Robotic Systems with seL4

The Robotic Operating System (ROS) middleware has been a key enabler of robotic platform and application development. This modular componentized architecture has made it possible for a community of developers to leverage innovations from across the industry while decoupling individual nodes from changes in the rest of the system. Unfortunately, security has been an after thought in this ecosystem, but it is of critical importance. Industrial robots have a long unfortunate history of accidents involving injury or death of the people working alongside them, even with strict safety protocols and guardrails. The potential for a malicious entity to bypass these guardrails is a major cause for concern. Furthermore, even small robots can be dangerous in the right conditions regardless of their size, locomotion, or manipulator capabilities. Since the availability of warfighters is naturally limited by the population this force is drawn from, robotics provide a way to surpass this limit to match the force potential of adversaries with much larger civilian populations. Realizing this, the Army has created the Army Common Robotics Software (ARCS) as a key enabler for autonomous ground vehicle applications. However, the removal of human personnel with physical access to the vehicle negates the typical security mitigation deployed by the Army: guards with guns, making cybersecurity a fundamental concern in these applications. Many efforts are underway to harden the ROS software stack such as security plug-ins to the Data Distribution Service (DDS) middleware, but since software is only as secure as its lowest layer, running this stack on a more security focused operating environment would go a long way to securing these applications. While some commercial RTOS vendors provide ROS compatible software libraries these offerings are costly and vendor specific reducing portability and maintainability, not to mention their sometimes dubious security claims. seL4, on the other hand, has a strong security posture established using formal methods to prove separation of processes and components running on the microkernel. These separation properties also enable seL4 to run isolated virtual machines (VM) which can be leveraged to quickly support legacy applications such as existing ROS/ARCS deployments and in turn incrementally harden these systems. This incremental approach will allow the Army to maximize past investments while addressing security concerns and overcoming hurdles with supporting ROS in limited operating environments such as seL4 as they are encountered. In phase I, DornerWorks showed it was feasible to leverage this approach to run ROS applications supported by native seL4 Micro-ROS threads to increase the resiliency of those applications. The proposed effort continues this work to seamlessly support a greater portion of the ROS/ARCS software stack, provide the necessary security extensions, and transition this work to a physical robotics platform.