Formal verification of integrity attacks on connected medical devices in battlefield hospitals

Abstract

Abstract Field hospitals in battlefield settings increasingly rely on connected medical devices, including monitors, ventilators, infusion pumps, patient-identification services, and gateway-based communication. In such environments, integrity attacks may create patient-safety hazards even when the system appears operational, by tampering with data, replaying old messages, injecting false information, or swapping patient identities. This work presents a formal framework for analyzing these attacks as a stochastic clinical–cyber system that integrates patient-state evolution, intermittent communication, attacker actions, and gateway-centered defense policies. Safety is evaluated using bounded unsafe reachability, supported by formal verification and resource-aware strategy synthesis. A synthetic digital twin is used to generate benign and attacked traces without real patient data; therefore, the findings are interpreted as model-based and simulation-based evidence rather than clinical validation. Confirmatory Monte Carlo evaluation used 5000 trajectories per configuration under 20 fixed root seeds. Patient-ID swapping reached an empirical unsafe reachability of 0.297 (95% CI 0.284–0.310) at the largest evaluated per-step attack-capacity limit, while the combined adaptive attacker reached 0.384 (95% CI 0.371–0.397). Evaluation of the synthesized combined gateway policy reduced empirical model-estimated unsafe reachability from 0.392 (95% CI 0.378–0.406) to 0.119 (95% CI 0.110–0.128) in the evaluated synthetic scenario, corresponding to a 69.6% relative reduction in this formal safety proxy, but with increased workflow burden. A separate PRISM-games worst-case query returned 0.410 under the disclosed finite abstraction. Verification remained tractable at the evaluated scales, with median PRISM runtime increasing from 0.90 to 28.70 s as the abstract state space expanded. Overall, the study supports formal verification as an analytical framework for safety-aware cyber-defense evaluation in connected field-hospital medical systems under explicit modeling assumptions; it does not establish clinical risk reduction or deployment readiness.