Skip to main content
The University of New South Wales

PhD Research Project

User- and Developer-Friendly Secure Operating System for IoT

Description

IoT applications need security, as many of them handle privacy-sensitive data or have the potential to harm people, such as medical devices. Or are part of critical infrastructure, where compromising one IoT device provides a foothold for attacking the whole critical system.

At the same time, these devices have high usability requirements, as many of them are operated by end-users or skilled experts who are not IT-savy, medical devices (wearable devices operated by the patient or clinical devices operated by nurses and doctors) are again a representative example. Furthermore, developers of such devices tend to be domain experts (again, medical) rather than IT experts, and expect an easy-to-use development environment.

These requirements pose demands on operating systems (OSes) are presently at odds. On the one hand, popular OSes like Android are easy to use, are well supported and are easy to develop for, but in terms of security is unsuitable for such critical systems. The fundamental reason for its lack of security is the huge trusted computing base (TCB), which consists of many millions of lines of code (LOC), and an inherent complexity that makes it prone to failure and security compromises. On the other hand, highly secure OSes tend to be expensive niche products that are cumbersome to use and program for. An example is seL4, the world’s first OS with a mathematical proof of correctness and security, which was developed at UNSW and Data61, and is arguably the world’s most secure OS.

This project will combine the strong security of seL4 with the convenience of Android to provide a secure, yet user- and developer-friendly OS that is suitable for a wide range of IoT applications. The idea is the run Android in a virtual machine on top of seL4, so the latter becomes responsible for enforcing security. To maintain the user- and developer-friendliness of Android, the system will support a secure category of Android apps, where all critical operations are performed outside the Android environment in seL4-provided sandboxes. These communicate with the user via seL4-protected secure paths to user-interface (UI) devices (touchscreen, microphone, speaker) and with the internet via seL4-protected encryption that allows secure tunneling of data through Android’s networking infrastructure.

Technical challenges include the design of abstractions allowing the partitioning of apps into the critical (seL4-based) core and non-critical (Android-based) functionality, the secure multiplexing of UI devices, the secure re-use of the Android development environment and app store, and the secure loading of the core from a secure Android app.

Required knowledge/skills

This topic requires a strong background in operating-system design and implementation, and strong systems skills, in particular the ability to understand and work with large code bases. Experience with seL4 or other microkernels is a strong plus.

Supervisors

Served by Apache on Linux on seL4.