Our Secure Systems Research Center (SSRC) has entered a research partnership with the University of New South Wales (UNSW Sydney), which is the inventor of seL4. In line with the synergy, UNSW and SSRC will research ways to enhance, improve and scale the adoption of seL4 on edge devices including mobile smartphones, drones, and IoT devices used in cyber-physical systems.
A small, trusted computing base (TCB) is required to ensure the security guarantees that a system can enforce. Strong isolation guarantees offered by virtualization help to define the boundaries of an operating system. Through a collaborative effort between UNSW and SSRC, we aim to extend the formally verified seL4 microkernel to support dynamic virtualization. Combining the two security assurances of minimal TCB and strong isolation together creates a world-class baseline for the most demanding environments.
The heterogeneous nature of edge computing requires supporting a broad range of hardware architectures (ARM, RISC-V, x86, etc.) and software solutions - ranging from control systems to demanding user centric devices. These high assurance systems are deployed at the edge where environmental factors, battery constraints, performance, and usability all add additional complexity. SSRC has undertaken to solve these challenges and through our collaboration with UNSW, we will enable a paradigm shift in what we expect from security solutions at the edge.
Dr. Shreekant (Ticky) Thakkar, Chief Researcher, SSRC, said: “We look forward to collaborating with UNSW to define a secure foundation for Zero-Trust, secure, resilient, cyber-physical and autonomous systems.”
