README.md

metadata

title: EBSysMLSec-Py LLM HAZOP Analyzer
emoji: 🔒
colorFrom: blue
colorTo: indigo
sdk: gradio
sdk_version: 5.9.1
app_file: app.py
pinned: false

EBSysMLSec-Py: Formal Safety-Security Analysis with LLM-Assisted HAZOP

A Python reimplementation of the EBSysMLSec model transformation pipeline (Poorhadi & Troubitsyna, SAFECOMP 2024), applied to a new domain and extended with LLM-assisted HAZOP threat analysis.

Domain: Autonomous Insulin Pump Controller (medical safety-critical system)
Original domain: Railway moving-block signalling (CBTC)
Contribution: Python translator + LLM-assisted HAZOP — neither present in the original ATL/Eclipse toolchain

---

What this project does

The original EBSysMLSec tool (written in ATL — ATLAS Transformation Language) takes a SysML model of a safety-critical system and automatically generates Event-B machines and contexts that can be formally verified in the Rodin prover. Security attacks are injected as Event-B events; failing proof obligations show which safety invariants are violated under attack.

This project reproduces that pipeline in Python and extends it:

sysml/insulin_pump.xmi
        │
        ▼
translator/sysml_to_eventb.py        ← Python reimplementation of EBSysMLSec ATL rules
        │
        ├─▶ eventb/InsulinPump.buc   ← Event-B context (sets, constants, axioms)
        ├─▶ eventb/InsulinPump.bum   ← Event-B machine (normal operation)
        ├─▶ eventb/attacks/Attack_Spoofing.bum    ← Attack A: sensor spoofing
        ├─▶ eventb/attacks/Attack_Injection.bum   ← Attack B: command injection
        └─▶ eventb/attacks/Attack_Replay.bum      ← Attack C: replay attack
                │
                ▼
        hazop/hazop_analyzer.py      ← LLM-assisted HAZOP via Anthropic API  [NEW]
                │
                ▼
        hazop/threats.json           ← 18 structured threat scenarios
                │
                ▼
        verification/proof_results.md ← which Rodin POs hold / fail per attack

---

System: Autonomous Insulin Pump Controller

Six SysML blocks connected by five information flows:

PatientProfile ──F2──▶ DoseCalculator ──F3──▶ SafetyMonitor ──F4──▶ PumpActuator
                              ▲
GlucoseSensor ──F1────────────┘
NetworkInterface ──F5──▶ DoseCalculator   ← attack surface

Safety invariants (Event-B)

Label	Predicate	Protection
INV1	delivered_dose ≤ MAX_SAFE_DOSE	Overdose prevention
INV2	delivered_dose > 0 ⇒ glucose_reading ≥ HYPO_THRESHOLD	Hypoglycaemia protection
INV3	delivered_dose > 0 ⇒ battery_level ≥ MIN_BATTERY_LEVEL	Power safety
INV4	delivered_dose > 0 ⇒ command_approved = TRUE	Authorisation gate
INV5	dose_request ≤ MAX_SAFE_DOSE	Calculator output bound

Attack scenarios and violated invariants

Attack	HAZOP guide word	Flow	Violated	Event-B machine
A: Sensor spoofing	MORE on F1	GlucoseSensor → DoseCalculator	INV2	Attack_Spoofing.bum
B: Command injection	AS WELL AS on F5	NetworkInterface → DoseCalculator	INV4	Attack_Injection.bum
C: Replay attack	OTHER THAN on F5	NetworkInterface → DoseCalculator	INV1	Attack_Replay.bum

---

Running the pipeline

pip install -r requirements.txt

# Full pipeline (Event-B generation + LLM HAZOP)
export ANTHROPIC_API_KEY=sk-ant-...
python run_pipeline.py

# Event-B generation only (no API key needed)
python run_pipeline.py --skip-hazop

# Gradio demo (uses pre-generated threats by default)
python app.py

---

Verifying in Rodin

1. Download Rodin Platform 3.7
2. Install the Camille plugin (textual Event-B import)
3. Create a new Event-B project in Rodin
4. Add a new Context: paste content of eventb/InsulinPump.buc
5. Add a new Machine: paste content of eventb/InsulinPump.bum — Run Provers → all POs discharge
6. Add attack machines from eventb/attacks/ — Run Provers → specific POs fail

Expected results per verification/proof_results.md:

Machine	INV1	INV2	INV3	INV4	INV5
Normal	✓	✓	✓	✓	✓
+ Spoofing	✓	✗	✓	✓	✓
+ Injection	✓	✓	✓	✗	✓
+ Replay	✗	✓	✓	✓	✓

✓ Rodin proof obligation discharged · ✗ Proof obligation fails = invariant violated under attack

---

LLM-Assisted HAZOP: the AI contribution

In the original Poorhadi & Troubitsyna papers, the HAZOP analysis is manual — a domain expert applies the seven guide words to each flow by hand. This project automates that step using Claude:

from hazop.hazop_analyzer import analyze_system, INSULIN_PUMP_MODEL

threats = analyze_system(INSULIN_PUMP_MODEL)
# → list of 18 structured threat dicts, each linked to an Event-B attack event

The LLM receives the system model (blocks, flows, invariants) and applies HAZOP guide words systematically to produce the same structured threat table a human analyst would — but for any system, in seconds.

This is a direct demonstration of the PhD position's research question:

"how formally specified safety constraints can be derived using AI"

---

Repository structure

insulin-pump-formal/
├── sysml/
│   └── insulin_pump.xmi          SysML/XMI model (NCS style)
├── translator/
│   └── sysml_to_eventb.py        Python SysML → Event-B translator
├── eventb/
│   ├── InsulinPump.buc            Event-B context
│   ├── InsulinPump.bum            Event-B machine (normal operation)
│   └── attacks/
│       ├── Attack_Spoofing.bum    Attack A: INV2 violated
│       ├── Attack_Injection.bum   Attack B: INV4 violated
│       └── Attack_Replay.bum      Attack C: INV1 violated
├── hazop/
│   ├── hazop_analyzer.py          LLM-assisted HAZOP (Anthropic API)
│   └── threats.json               Pre-generated threat analysis
├── verification/
│   └── proof_results.md           Proof obligation results per scenario
├── app.py                         Gradio demo (HF Spaces)
├── run_pipeline.py                Full pipeline entry point
└── requirements.txt

---

References

1. Poorhadi, E., Troubitsyna, E., Dán, G. (2022). Analysing the Impact of Security Attacks on Safety Using SysML and Event-B. IMBSA 2022. DOI: 10.1007/978-3-031-15842-1_13
2. Poorhadi, E., Troubitsyna, E. (2023). Automating an Analysis of Safety-Security Interactions for Railway Systems. RSSRail 2023. DOI: 10.1007/978-3-031-43366-5_1
3. Poorhadi, E., Troubitsyna, E. (2024). Automating an Integrated Model-Driven Approach to Analysing the Impact of Cyberattacks on Safety. SAFECOMP 2024. DOI: 10.1007/978-3-031-68738-9_5
4. Troubitsyna, E. (2024). Formal Analysis of Interactions Between Safety and Security Requirements. In: The Practice of Formal Methods. DOI: 10.1007/978-3-031-66673-5_8
5. Abrial, J.R. (2010). Modeling in Event-B. Cambridge University Press.

---

What makes this original

Aspect	Original EBSysMLSec	This project
Transformation language	ATL (Eclipse/EMF)	Python
Domain	Railway (CBTC moving block)	Medical device (insulin pump)
HAZOP	Manual	LLM-assisted (new contribution)
Attack modelling	Railway-specific attacks	Spoofing, injection, replay
Formal artefacts	Rodin XML format	Textual Event-B (Camille notation)
Distribution	Eclipse plugin	Python + Gradio + HF Spaces