Spaces:
Sleeping
Sleeping
| 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 | |
| ```bash | |
| 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](http://www.event-b.org/install.html) | |
| 2. Install the [Camille plugin](https://wiki.event-b.org/index.php/Camille) (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: | |
| ```python | |
| 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 | | |