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

TL;DR

GlucOS is a secure, personalized automated insulin delivery system that uses formal methods and adaptive security to ensure safety and effectiveness in real-world diabetes management.

Contribution

This paper introduces GlucOS, a novel architecture enabling personalized insulin dosing with security against malicious models, validated through real-world deployment and formal proofs.

Findings

Maintains safety under attack conditions

Improves glucose control in daily life

Generalizes from simulation to real-world use

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.