seROS: Securing Robotic Systems with seL4

The Robotic Operating System (ROS) software stack has been a key enabled to 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 other parts of the system. Unfortunately, security has been a bit of 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 qualified warfighters is naturally limited by the population which 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 Robotics Technology Kernel (RTK) 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 the addition of security extensions to the Data Distribution Service (DDS) middleware, but since a software stack is only as secure as its lowest layer, moving some or all of the ROS software stack to 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 through the use of 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/RTK 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.