Modeling and Formal Analysis of High-Assurance Mixed-Reality Systems

Mixed-reality (MR) systems are seeing increased deployment in high-assurance aerospace applications, necessitating rigorous analyses of the complex interactions with their human operators and the surrounding environment. Traditional verification methods often neglect operator behavior or assume overly simplistic interactions, leaving MR systems vulnerable to attacks involving human cognition. This paper introduces the Modeling and Analysis Toolkit for Realizable Intrinsic Cognitive Security (MATRICS), aimed at formally assuring MR systems against cognitive adversarial threats. MATRICS integrates cognitive, environmental, and device modeling techniques to comprehensively address four categories of cognitive attacks: physiological, perceptual, attentional, and status-based. Our preliminary models and verification efforts validate the feasibility of our approach to provide essential cognitive security assurance, thereby enhancing operational effectiveness in adversarial contexts.