Scholarlink

<p>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.</p>

错误：搜索内容不能为空，请输入英文关键词
错误：关键词超出字数限制，请精简
高级检索

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

  • 期刊论文

  • 出版模式：

    开放获取

  • 发表日期：

    2026年7月30日

查看全文
  • Iman Akour,
  • Mohamed Nour,
  • Mohamed Elhoseny,
  • Mohanad A. Deif

摘要

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.