Type 1 Diabetes (T1D) is a metabolic disorder where an individual's pancreas stops producing insulin. To compensate, they inject synthetic insulin. Computer systems, called automated insulin delivery systems, exist that inject insulin automatically. However, insulin is a dangerous hormone, where too much insulin can kill people in a matter of hours and too little insulin can kill people in a matter of days. In this paper, we take on the challenge of building a new trustworthy automated insulin delivery system, called GlucOS. In our design, we apply separation principles to keep our implementation simple, we use formal methods to prove correct the most critical parts of the system, and we design novel security mechanisms and policies to withstand malicious components and attacks on the system. We report on real world use for one individual for 6 months using GlucOS. Our data shows that for this individual, our ML-based algorithm runs safely and manages their T1D effectively. We also run our system on 21 virtual humans using simulations and show that our security and safety mechanisms enable ML to improve their core T1D measures of metabolic health by 4.3\% on average. Finally, we show that our security and safety mechanisms maintain recommended levels of control over T1D even in the face of active attacks that would have otherwise led to death. GlucOS is open source and our code is available on GitHub.

翻译：1型糖尿病是一种代谢紊乱疾病，患者的胰腺停止产生胰岛素。为弥补这一缺陷，患者需注射合成胰岛素。现有计算机系统（称为自动化胰岛素输送系统）可自动注射胰岛素。然而，胰岛素是一种危险激素：过量胰岛素可在数小时内致人死亡，而胰岛素不足则可在数日内危及生命。本文致力于构建名为GlucOS的新型可信自动化胰岛素输送系统。在设计过程中，我们运用隔离原则保持实现简洁性，采用形式化方法验证系统最关键部分的正确性，并设计创新的安全机制与策略以抵御恶意组件和系统攻击。我们报告了单名患者使用GlucOS系统6个月的实际应用数据。数据显示，基于机器学习的算法可安全运行并有效管理该患者的1型糖尿病。通过在21个虚拟人体上进行模拟实验，我们证明安全防护机制能使机器学习算法将核心代谢健康指标平均提升4.3%。最后研究表明，即使在遭受原本会导致死亡的主动攻击时，我们的安全防护机制仍能维持对1型糖尿病的建议控制水平。GlucOS系统已开源，代码发布于GitHub平台。