Document Type
Article
Date
Summer 6-20-2026
Keywords
Mission assurance, Systems security engineering (SSE), STORM-AI, Commander's intent, STPA-Sec, Trustworthiness, Access-Control Logic (ACL), HOL4 theorem proving, AI Risk Management Framework (AI RMF), PAGE
Language
English
Funder(s)
National Security Agency
Funding ID
CON06350
Disciplines
Electrical and Computer Engineering
Description/Abstract
A STORM-AI Primer with an Operationally Representative Example presents the Systems-Theoretic Technical and Operational Risk Management with Artificial Intelligence (STORM-AI) methodology, a transdisciplinary framework for establishing the trustworthiness of mission systems that may incorporate AI components. The core value proposition of STORM-AI is mission assurance—ensuring that mission systems behave with the predictability and proportionality required by senior leadership and demanded by international humanitarian law. STORM-AI achieves this by faithfully preserving commander's intent from high-level mission descriptions down to hardware-level behavioral specifications through a structured sequence of four formally grounded models: a Mission Model, a Protection (Loss Control) Model, a Security (Secure State Machine) Model, and a Behavior Model (High-Level State Machine). Each model pair is accompanied by a trustworthiness context that provides stakeholders with the evidence necessary to make informed decisions about residual risk. The framework integrates NIST SP 800-160v1 systems security engineering principles, STPA-Sec hazard analysis, Access-Control Logic (ACL), Certified Security by Design (CSBD), and the NIST AI Risk Management Framework, with all security properties formally verified in the HOL4 theorem prover. STORM-AI further incorporates the PAGE (Percepts, Actions, Goals, Environment) framework for the principled design and evaluation of AI agents. An operationally representative example applies STORM-AI to a fictitious collaborative combat aircraft, the FQ-X, situated within a Taiwan Strait scenario drawn from the Hudson Institute's Taiwan Bulwark Activation Force concept. The appendices supply the syntax, semantics, and inference rules of the Access-Control Logic and the complete set of HOL4-verified FQ-X theories.
Recommended Citation
Chin, Shiu-Kai; Clark, Matthew; Katz, Garrett; Oh, Jae C.; and Young, William, "A STORM-AI Primer with an Operationally Representative Example" (2026). Electrical Engineering and Computer Science - All Scholarship. 255.
https://surface.syr.edu/eecs/255
Creative Commons License
This work is licensed under a Creative Commons Attribution 4.0 International License.
