Formalizing ROS2 security configuration with Alloy

Abstract

Industrial manufacturing is becoming highly reliant on automation developments, as they bring more efficient and accurate processes, with lower associated costs. Consequently, robots are increasingly being deployed in a wide range of scenarios, especially where safety is demanded. In such cases, it is critical to employ appropriate procedures to verify both the system’s quality and safety. Following the current growth of cyber-physical systems, as well as their usage in various technology domains, the development of software applications is becoming more demanding due to the complexity behind the integration of complementing services, beyond those provided by the operating system. One of the most popular open-source software platforms for building robotic systems is the Robot Operating System (ROS) [53] middleware, where highly configurable robots are usually built by composing third-party modules. Robot Operating System 2 (ROS2) is implemented using the Data Distribution Service (DDS) [49] communication protocol. ROS2 implicitly makes use of the DDS-Security artefacts through the Secure Robot Operating System 2 (SROS2) security toolset. The present study focus on detecting security problems in ROS2 networks, in which it is intended to verify, through formal techniques, security properties. However, security is a very broad subject, so this study focuses on a particular security property to show the viability of the proposed technique, namely Observational Determinism (OD). This dissertation introduces a software tool, named Security Verification in ROS (svROS), that provides multiple functionalities to support this type of security analysis using Alloy [32], a formal specification language and analysis tool.

A crescente implementação de processos automáticos tem motivado a reestruturação nos mais diversos setores industriais, com o objetivo de aumentar a eficiência e precisão dos mesmos, e consequentemente, reduzir os custos associados. Além disso, esta ideia levou à integração da robótica nos mais amplos domínios tecnológicos, especialmente onde a segurança é exigida. Nestes casos, é fundamental adotar técnicas apropriadas de forma a verificar tanto a qualidade do sistema, como a segurança do mesmo. Como resultado do atual crescimento dos sistemas ciber-físicos, nomeadamente sistemas robóticos, bem como a sua utilização em vários domínios tecnológicos, o desenvolvimento de aplicações tem vindo a ficar mais exigente, em particular devido à complexidade da integração dos serviços necessários, tipicamente não fornecidos pelo sistema operativo. Uma das plataformas considerada como standard no que toca ao desenvolvimento de sistemas robóticos é o middleware ROS [53], onde robôs altamente configuráveis são construídos através da composição modular de software externo, oferecendo características como flexibilidade e interoperabilidade aos sistemas integrados. O ROS2 implementa um protocolo de comunicação, de nome DDS [49], que, para além de garantir serviços de comunicação, implementa a especificação DDS-Security, que oferece diferentes métodos de adoção de segurança, através de uma metodologia de plugins. Através do uso desta especificação, juntamente com o uso do toolset SROS2, é possível configurar o ROS2 de forma a proporcionar um ambiente seguro às aplicações integradas. O presente trabalho foca-se no estudo e deteção de problemas de segurança em topologias ROS2, através da verificação formal de propriedades de segurança. No entanto, a segurança é um assunto extenso, pelo que o foco de interesse nesta tese é numa propriedade particular de segurança para mostrar a viabilidade da presente técnica, de nome OD. Esta dissertação introduz a uma ferramenta de verificação de nome svROS, que contempla múltiplas funcionalidades para suportar este tipo de análise usando Alloy [32], uma linguagem de especificação formal e respectiva ferramenta de análise.