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 combines algorithmic security, driver security, and end-to-end verification to protect against malicious ML models, vulnerable pump drivers, and drastic changes in 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. 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 source code is open source.

翻译：本文提出GlucOS，一种新型可信自动胰岛素输送系统。本文核心内容是我们设计、实现并在真实人体上部署的系统，以及从实践中获得的经验教训。GlucOS通过算法安全、驱动安全与端到端验证相结合，防范恶意机器学习模型、脆弱的泵驱动程序以及人体生理状态的剧烈变化。我们采用形式化方法证明关键组件的正确性，并将人体纳入防御策略体系。评估工作包含对七名受试者的真实场景部署以及仿真实验结果，证明了所提技术的普适性。结果表明，即使在遭受攻击的情况下，GlucOS仍能维持安全性并改善血糖控制水平。本研究展示了构建安全、个性化、自动化医疗系统的潜力。系统源代码已开源。