Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Analyzing Healthcare Interoperability Vulnerabilities: Formal Modeling and Graph-Theoretic Approach

Jawad Mohammed, Gahangir Hossain

Abstract

In a healthcare environment, the healthcare interoperability platforms based on HL7 FHIR allow concurrent, asynchronous access to a set of shared patient resources, which are independent systems, i.e., EHR systems, pharmacy systems, lab systems, and devices. The FHIR specification lacks a protocol for concurrency control, and the research on detecting a race condition only targets the OS kernel. The research on FHIR security only targets authentication and injection attacks, considering concurrent access to patient resources to be sequential. The gap in the research in this area is addressed through the introduction of FHIR Resource Access Graph (FRAG), a formally defined graph G = (P,R,E, λ, τ, S), in which the nodes are the concurrent processes, the typed edges represent the resource access events, and the race conditions are represented as detectable structural properties. Three clinically relevant race condition classes are formally specified: Simultaneous Write Conflict (SWC), TOCTOU Authorization Violation (TAV), and Cascading Update Race (CUR). The FRAG model is implemented as a three-pass graph traversal detection algorithm and tested against a time window-based baseline on 1,500 synthetic FHIR R4 transaction logs. Under full concurrent access (C2), FRAG attains a 90.0% F1 score vs. 25.5% for the baseline, a 64.5 pp improvement.

Analyzing Healthcare Interoperability Vulnerabilities: Formal Modeling and Graph-Theoretic Approach

Abstract

In a healthcare environment, the healthcare interoperability platforms based on HL7 FHIR allow concurrent, asynchronous access to a set of shared patient resources, which are independent systems, i.e., EHR systems, pharmacy systems, lab systems, and devices. The FHIR specification lacks a protocol for concurrency control, and the research on detecting a race condition only targets the OS kernel. The research on FHIR security only targets authentication and injection attacks, considering concurrent access to patient resources to be sequential. The gap in the research in this area is addressed through the introduction of FHIR Resource Access Graph (FRAG), a formally defined graph G = (P,R,E, λ, τ, S), in which the nodes are the concurrent processes, the typed edges represent the resource access events, and the race conditions are represented as detectable structural properties. Three clinically relevant race condition classes are formally specified: Simultaneous Write Conflict (SWC), TOCTOU Authorization Violation (TAV), and Cascading Update Race (CUR). The FRAG model is implemented as a three-pass graph traversal detection algorithm and tested against a time window-based baseline on 1,500 synthetic FHIR R4 transaction logs. Under full concurrent access (C2), FRAG attains a 90.0% F1 score vs. 25.5% for the baseline, a 64.5 pp improvement.

Paper Structure

This paper contains 34 sections, 3 theorems, 6 figures, 5 tables.

Table of Contents

  1. Introduction
  2. Contributions
  3. Related Work
  4. Concurrency detection in systems software
  5. Healthcare interoperability security
  6. The gap
  7. Background
  8. The critical section problem
  9. FHIR architecture and the concurrency model
  10. Real-world prevalence of the three concurrency conditions
  11. Why existing synchronization approaches are insufficient
  12. The FHIR resource access graph
  13. Formal definition
  14. Formal propositions
  15. FRAG visualization
  16. ...and 19 more sections

Key Result

Proposition 1

If $\text{SWC}(p_i, p_j, r)$ exists --- both $p_i$ and $p_j$ hold concurrent WRITE edges to $r$ with no synchronization constraint --- then $RC(p_i, p_j, r)$ holds under Definition 2. $\blacktriangleleft$$\blacktriangleleft$

Figures (6)

  • Figure 1: Cyber threat landscape in FHIR-based healthcare interoperability. Multiple independent systems access shared patient resources concurrently with no synchronization protocol ($S = \emptyset$), giving rise to race condition classes SWC, TAV, and CUR.
  • Figure 2: FRAG showing $RC(p_1,p_2,r_1)$ between EHR READ and Lab WRITE on AllergyIntolerance, and a $\text{CUR}(p_1,p_2,p_3)$ chain where CDS acts on EHR's stale read. $S = \emptyset$ throughout.
  • Figure 3: The three healthcare race condition classes formally defined in FRAG: (a) Simultaneous Write Conflict (SWC) --- two concurrent WRITE operations with no synchronization; (b) TOCTOU Authorization Violation (TAV) --- permission revoked inside the vulnerability window; (c) Cascading Update Race (CUR) --- a stale-read dependency chain of depth $\geq 2$.
  • Figure 4: FRAG vs. Baseline detection performance under C2 (concurrent, unsynchronized access). Lines show Precision, Recall, and F1 per race class. The shaded region highlights the detection gap between FRAG and the Baseline F1.
  • Figure 5: F1 score comparison between conditions C2 and C3. Arrows and labels show the recall-driven F1 drop under partial ETag synchronization. Baseline performance remains flat across both conditions.
  • ...and 1 more figures

Theorems & Definitions (7)

  • Definition 1: FRAG
  • Definition 2: Race condition
  • Definition 3: TOCTOU window
  • Definition 4: Cascading update race
  • Proposition 1: SWC is a race condition
  • Proposition 2: TAV implies TOCTOU window
  • Proposition 3: CUR detectability