GlucOS: Security, correctness, and simplicity for automated insulin delivery

TL;DR

GlucOS addresses secure, automated insulin delivery for Type 1 Diabetes by coupling a lightweight, formally verifiable BioKernel with a flexible, external predictive component. The core idea is to separate predictive dosing from safety logic and bound the predictor via a reactive safe model, reinforced by a biological invariant that end-to-end checks a patient’s physiology with a 30 mg/dl threshold over a 30-minute window, expressed as $\Delta G^{C} - \Delta G^{A} \leq T$ and $S \leq \frac{0.9 \cdot G_{t+\Delta t}^{M} - 1.1 \cdot G_{t}^{M} + T}{B \cdot \Delta t - 0.99 \cdot \Delta IOB^{M} + 0.01 \cdot \Sigma I_{i}^{M}}$. The system is formally verified for key insulin-delivery components, validated in simulations with 21 virtual humans, and deployed in a real-world study with seven participants, showing improved safety and glucose control under attack scenarios. Notably, biological invariants capture unmodeled physiology changes, and human-driven predictive alerts augment security without undue burden. The work demonstrates that secure, personalized automated healthcare systems can be realized through a combination of simple, domain-specific security, formal verification, and careful consideration of real-world use and ethics.

Abstract

We present GlucOS, a novel system for trustworthy automated insulin delivery. Fundamentally, this paper is about a system we designed, implemented, and deployed on real humans and the lessons learned from our experiences. GlucOS introduces a novel architecture that allows users to personalize diabetes management using any predictive model (including ML) for insulin dosing while simultaneously protecting them against malicious models. We also introduce a novel holistic security mechanism that adapts to unprecedented changes to human physiology. We use formal methods to prove correctness of critical components and incorporate humans as part of our defensive strategy. Our evaluation includes both a real-world deployment with seven individuals and results from simulation to show that our techniques generalize. We highlight that our results are not from a lab study, with people using GlucOS to manage Type 1 Diabetes in their daily lives. Our results show that GlucOS maintains safety and improves glucose control even under attack conditions. This work demonstrates the potential for secure, personalized, automated healthcare systems. Our entire source code is available at this link.

Figures (15)

• Figure 1: Overview of automated insulin delivery devices, closed-loop architecture, and GlucOS.
• Figure 2: Overall architecture for the BioKernel.
• Figure 3: Algorithmic security mechanism for GlucOS.
• Figure 4: GlucOS predicts hypoglycemia and notifies the user before it happens so they can proactively prevent it.
• Figure 5: Average proportion of time spent in range (TIR) across 21 virtual humans with a reactive safe model, a predictive ML model, and clamping the predictive ML with the reactive safe model for security.