Hora: High Assurance Periodic Availability Guarantee for Life-Critical Applications on Smartphones

Body-worn medical devices benefit from having a companion mobile application to monitor them and even program them. For example, the companion application for an insulin pump can be used to automatically monitor blood sugar level throughout the day and administer insulin without user input [1]. Unfortunately, the operating systems of modern smartphones cannot provide adequate security guarantees for these applications. Existing Trusted Execution Environment (TEE) solutions aim to alleviate these problems by removing the system software (and even most of the hardware [19]) from the TCB. However, no existing TEE solution provides a critical guarantee needed for these applications: periodic availability. This is needed to ensure that the application is executed according to a requested schedule, e.g., multiple times a day to read the patient's blood sugar and administer insulin. We present our ongoing work on Hora1, a high assurance TEE solution for smartphones that guarantees periodic availability of CPU and I/O with a minimal and formally-verified scheduler. We present the design of Hora as well as its scheduler, which is implemented fully in Rust (in 1583 lines of code) and (partially) formally verified using the Kani model checker [7].