Work-in-Progress: Formal Verification of Resource-Constrained Cyber Strategies across Macro, Meso, and Micro Scales

ABSTRACT

Defensive cybersecurity strategies are governed by rigid operational constraints, primarily limited maintenance windows and finite budgetary allocations. Current decision-support tools lack the formal machinery to prove that a generated strategy is logically consistent with these constraints or provide traceability across
macro (budgetary), meso (policy), and micro (technical) scales. This work-in-progress paper introduces a verification pipeline utilizing a new cyber-domain ontology extension to the Suggested Upper Merged Ontology (SUMO) [22]. We suggest the combination of game-theoretic strategy generation with automated theorem proving (ATP) to perform proof-by-refutation on candidate strategies, which are verifiably safe under an Adversarial Knapsack constraint model[14].

BIO

Jonathan A. Goohs Jr. is a U.S. Navy Maritime Cyber Warfare Officer and Master of Computer Science candidate at the Naval Postgraduate School, where he specializes in Artificial Intelligence. He holds a Bachelor of Science in Cyber Operations from the United States Naval Academy. His operational background includes serving at U.S. Cyber Command. His research spans game-theoretic models of cyber operations, formal ontology engineering, and automated reasoning, with publications at IEEE MILCOM, arXiv, and CSET.

He is co-developing the SUMO cyber domain ontology extension with Dr. Adam Pease at the Naval Postgraduate School, who is the author of SUMO and has a portfolio page linked at: https://www.ontologyportal.org and www.adampease.com .

 

Submitted by Katie Dey on