Usable Security and Verification for Distributed Robotic Systems

Security and usability are often paradoxically portrayed as zero-sum trade-offs; this is especially true of cyber-physical systems. Historically, security has taken a back seat in open source robotic software initiatives, such as Robot Operating System (ROS), which have focused on development productivity instead of deployment hardening, and this has contributed, perhaps inadvertently, to the belated adoption of ROS by industry, impeding technical transfer between industry and academia. This dissertation studies methods for automating and verifying middleware configurations to improve the security for distributed robotic systems.We introduce procedural tooling for automating the setup of authenticated encryption and access control across the distributed data bus network used in robotic middleware frameworks, in a concerted effort to remove sources of errors such as human factors during configuration development. This includes an immutable logging framework with which to record event data used by any tooling in order to continuously profile and/or monitor system security. We then present methods for conducting passive reachability and controllability analysis over the data bus, and for combining that with static information flow control to guarantee isolation between sensitive or mission critical computations over larger integrations. Finally, we propose principles for the design, verification, and deployment of robotic architectures composed of partially distrusting components. We seek to establish a set of automated tools, methods, and design principles to compose and audit multiple robotic subsystems into hardened stacks for service and industry, and we call it "Usable Security and Verification for Distributed Robotic Systems.