Verifying Safety of Behaviour Trees in Event-B

Behavior Trees (BT) are becoming increasingly popular in the robotics community. The BT tool is well suited for decision-making applications allowing a robot to perform complex behavior while being explainable to humans as well. Verifying that BTs used are well constructed with respect to safety and reliability requirements is essential, especially for robots operating in critical environments. In this work, we propose a formal specification of Behavior Trees and a methodology to prove invariants of already used trees, while keeping the complexity of the formalization of the tree simple for the final user. Allowing the possibility to test the particular instance of the behavior tree without the necessity to know the more abstract levels of the formalization.

Securing Optimized Code Against Power Side Channels

Side-channel attacks impose a serious threat to cryptographic algorithms, including widely employed ones, such as AES and RSA, taking advantage of the algorithm implementation in hardware or software to extract secret information via timing and/or power side-channels. Software masking is a software mitigation approach against power side-channel attacks, aiming at hiding the secret-revealing dependencies from the power footprint of a vulnerable implementation. However, this type of software mitigation often depends on general-purpose compilers, which do not preserve non-functional properties. Moreover, microarchitectural features, such as the memory bus and register reuse, may also reveal secret information. These abstractions are not visible at the high-level implementation of the program. Instead, they are decided at compile time. To remedy these problems, security engineers often sacrifice code efficiency by turning off compiler optimization and/or performing local, post-compilation transformations. This paper proposes SecConCG, a constraint-based compiler approach that generates optimized yet secure code. SecConCG controls the quality of the mitigated program by efficiently searching the best possible low-level implementation according to a processor cost model. In our experiments with ten masked implementations on MIPS32 and ARM Cortex M0, SecConCG speeds up the generated code from 10% to 10x compared to non-optimized secure code at a small overhead of up to 7% compared to non-secure optimized code. For security and compiler researchers, this paper proposes a formal model to generate secure low-level code. For software engineers, SecConCG provides a practical approach to optimize code that preserves security properties.

Online Path Generation and Navigation for Swarms of UAVs

With the growing popularity of Unmanned Aerial Vehicles (UAVs) for consumer applications, the number of accidents involving UAVs is also increasing rapidly. Therefore, motion safety of UAVs has become a prime concern for UAV operators. For a swarm of UAVs, a safe operation can not be guaranteed without preventing the UAVs from colliding with one another and with static and dynamically appearing, moving obstacles in the flying zone. In this paper, we present an online, collision-free path generation and navigation system for swarms of UAVs. The proposed system uses geographical locations of the UAVs and of the successfully detected, static and moving obstacles to predict and avoid: (1) UAV-to-UAV collisions, (2) UAV-to-static-obstacle collisions, and (3) UAV-to-moving-obstacle collisions. Our collision prediction approach leverages efficient runtime monitoring and Complex Event Processing (CEP) to make timely predictions. A distinctive feature of the proposed system is its ability to foresee potential collisions and proactively find best ways to avoid predicted collisions in order to ensure safety of the entire swarm. We also present a simulation-based implementation of the proposed system along with an experimental evaluation involving a series of experiments and compare our results with the results of four existing approaches. The results show that the proposed system successfully predicts and avoids all three kinds of collisions in an online manner. Moreover, it generates safe and efficient UAV routes, efficiently scales to large-sized problem instances, and is suitable for cluttered flying zones and for scenarios involving high risks of UAV collisions.