Verification and Validation of Artificial Pancreas Systems Software

Abstract

The safety and privacy of medical devices is of utmost importance. As they affect users’ health and lives, it is crucial to ensure these devices meet established safety and privacy standards. This dissertation examines artificial pancreas systems (APSs) as an example of emerging open-source DIY medical software solutions. We focus on AndroidAPS, an Android-based APS implementation primarily written in Kotlin. We address the need for testing and validating the app's safety and privacy and ensuring compliance with coding standards. We present a comprehensive survey of research on software analysis and modeling techniques in the context of APSs and medical devices. Our findings indicate that, while interest in this area is growing, gaps remain in applying these techniques to real-world examples. Additionally, although Kotlin is increasingly used in Android app development, software analysis research has yet to address apps written in Kotlin. We conduct an in-depth study of AndroidAPS and propose approaches to detect safety and privacy concerns. We demonstrate the feasibility of modeling Kotlin apps and extracting structural information through statistical analysis techniques by developing and implementing a dedicated analysis framework. We show that this framework can detect implicit inter-app communication via broadcasts, logging vulnerabilities, and enforce safety properties such as limits and constraints on sensitive data. For broadcast vulnerabilities, we identified one instance in a plugin used in AndroidAPS. Generalizing our analysis to other Android apps, we found over 70% to be unsafe. We introduce a sensitivity-flagging approach at the file and class levels to detect sensitive data logging. Our analysis revealed 133 potential data flows into 48 targets, with about 68% precision. This is due to high-granularity flagging; our framework allows finer granularity, which improves precision. Finally, we evaluate how the app handles variable initialization in two user profiles. In the first profile, 12 variables are tested, and in the second, 15. All are verified and set within defined constraints, except for two lacking explicit validation. By tracking these variables' flow, we identify two source functions, one of which validates input, while the other does not.