Formal Analysis of Vulnerabilities in Mixed-Reality Systems

With the proliferation of mixed-reality (MR) systems in aerospace and defense, there is increased potential for adversarial exploitation of system vulnerabilities and/or properties in the human cognitive process in order to reduce mission-effectiveness. This paper presents our preliminary work on the Modeling and Analysis Toolkit for Realizable Intrinsic Cognitive Security (MATRICS), a formal methods-based approach to provide a mathematically rigorous design and verification framework for protecting MR systems and operators in mission-critical applications from cognitive attacks. We describe our approach and present initial results, including formal models of the human operator, MR device, and mission environment, and apply existing formal methods tools to prove the holistic cognitive security of MR systems.