Security-Minded Verification of Autonomous Robotic Systems: PhD Symposium - iFM 2025 - Paris

In Cyber Security, there is significant qualitative effort to secure systems despite ample autonomous tools that help uncover security weaknesses and design flaws at the development and design stages respectively. These activities are necessary to protect a systems end-to-end, from design to development and deployment. But generally the handover from Threat modelling to Penetration testing is usually disjointed and still relies heavily on Security expert’s qualitative input introducing dependency on the expert’s skills and availability (costly). Formal verification can help to tackle these problems, and we propose a framework that can help to automate the discoveries of relevant security weaknesses and vulnerabilities in systems at design-time and at run-time. This will forge a natural link between threat modelling of systems and security testing. Formal verification has been increasingly applied in security to rigorously prove that systems meet confidentiality, integrity, and authentication guarantees. Tools like Tamarin Prover are widely used for protocol analysis, especially in cryptographic settings. For example, Tamarin has been used to verify the Signal messaging protocol, showing that end to end encryption, forward secrecy, and authentication properties hold even under strong adversarial models.