Formal methods for socio-technical security in eXtended Reality (XR): state-of-the-art and research agenda

Abstract The revolutionary opportunities presented by eXtended Reality (XR) technologies will only materialize if modeling and analysis activities, undertaken during the engineering process of XR systems, are directed towards ensuring their social acceptance. By this, we mean integrating human and technical aspects during system development to ensure that the system guarantees communication security and data privacy, and is trusted by end users. One approach to achieve these guarantees is through rigorous, formal specification and verification during system modeling and analysis, explicitly considering the human factor. Accordingly, in this survey, we systematically investigate 6 mainstream formalisms for modeling and analyzing socio-technical security concerns, encompassing privacy and trust, in XR systems. We consider both desired concerns (e.g., requirements, properties) and undesired ones (e.g., threats, attacks). Our investigation incorporates 34 state-of-the-art approaches comprising languages, techniques, frameworks, and tools, leveraging these formalisms, which we compare against a diverse set of criteria: (1) expressivity, (2) modeling and analysis complexity, (3) modeling and analysis constructs, (4) power of inference, (5) user-friendliness, (6) applicability. Based on our findings, we identify the current gaps and considerable challenges and suggest an agenda for future research. To guide our investigation from a more practical perspective, we also present two real-world pilot studies that illustrate the potential application of formal methods in specific XR applications. This work thus aims to provide insights from a twofold perspective: for formal methods researchers seeking to learn more about socio-technical security in XR systems, and for security practitioners focused on socio-technical aspects in XR who are interested in formal approaches.