Dr. Dhammika Elkaduwe, an eminent figure in Computer Science, is part of a team that has been bestowed with the prestigious ACM Software System Award for groundbreaking innovation in Embedded Systems. The award is a testament to his contribution and the wider seL4 team, which hails from different backgrounds and nations, coming together to advance operating systems that can change the backend of software across several industries.
The ACM Software System Award has a long and storied history recognizing pioneers in the field of computing. Past recipients include the inventor of the Domain Name System, Dr. Paul Mockapetris, creator of the Wireshark network protocol analyzer, Gerald Combs, and the developers of Berkeley DB, Margo Seltzer, Michael Olson, and Keith Bostic, to name a few. The ACM Software System Award 2022 was received by the team that developed the seL4 microkernel, the first Industry Strength High-Performance Operating System (OS) kernel.
Such robust collaborative efforts are made possible today, largely because academics are better connected today than ever before. NRENs (National Research and Education Network) are crucial enablers of these efforts, which support researchers through connectivity and helpful services. The Lanka Education And Research Network (LEARN), which is Sri Lanka’s NREN connects higher education institutions across the island and supports them in maximizing the value of their digital infrastructure. As an experienced academic, Dr. Elkaduwe shares that LEARN has been an invaluable pillar connecting Sri Lankan academia with the world.
What is the ACM Software System Award?
The Association for Computer Machinery (ACM) is a renowned international organization dedicated to advancing computing as a science and profession. It recognizes several teams or individuals who have made exceptional contributions to the development and innovation of Computer Science and Information Technology.
Accordingly, the ACM Software System Award is a distinguished accolade that acknowledges the profound impact of newly developed software systems in shaping the future of computing and technology. Moreover, the prestigious Award inspires the broader computer science community, encouraging innovation and further exploration in the field. It highlights exemplary work that serves as a basis for future research and motivates fresh minds to strive for excellence in their respective areas of software development.
Understanding the Winning seL4 Microkernel
Introducing the seL4 Microkernel, Dr. Elkaduwe explains, “A kernel is defined as the part of the software that runs in the privileged mode of the CPU. Typical applications we run, say your word processing app, run in the CPU’s user mode. If a fault occurs in a user-mode application, or if a user-mode application does something bad, the kernel will be notified and take corrective actions. But when you are in kernel mode, you do not have that luxury. If there is a fault in the kernel, it will take down the whole system with it.”
Hence, the primary objective of this research, recognized by the ACM Software System award, was to create an OS whose behaviour can be predicted using formal mathematics. “Unlike in other scientific applications, software tests find bugs but cannot prove that there are no bugs in the system. Therefore, our ultimate goal was to use formal mathematical models to ensure that certain specifications like infinite loops and crashes do not happen when the system runs,” Dr. Elkaduwe elaborates. Such a feat wasn’t attempted in the past due to the size of its problem and the level of complication.
According to Dr. Elkaduwe, two significant concerns at the time were the correct API or kernel design that would facilitate building a secure system and how it would be connected to the code. Hence, by stripping a kernel to its bare minimum, the seL4 team proved this is possible and connected the mathematical proof to the C code. Dr. Elkaduwe shares, “We started with the L4 microkernel, identified the shortcomings to develop a fully secure system on top of it, and developed a new API called seL4. The seL4 microkernel has sufficient mechanisms to facilitate the construction of secure systems on top of it and has a formal mathematical proof which connects a higher-level specification of seL4 to the low-level C implementation. .”
Unleashing Innovation Close to a Decade of Research
Dr. Elkaduwe began his work in kernel design in 2004 with the OS Research Group for Embedded Systems at the University of New South Wales, Australia. Over the years, his work has been focused on access control and high-level protection models. Accordingly, he actively designed the seL4 microkernel alongside several other developers.
During the development process, one of the biggest challenges faced by the team was memory management within the kernel itself. “the kernel is expected to provide services to user-mode applications. While doing so, the kernel consumes resources – in particular, memory is consumed to record what is happening in the system. A malicious user-mode application can exploit this and run a denial of service attack against the kernel,” Dr. Elkaduwe explains. Thus, emphasizing the need for visible consumption of kernel memory and communication channels.
Dr. Elkaduwe conveys that the Australian Government has funded the project through NICTA and has now come to a stage where companies are interested in commercializing the system. “The seL4 microkernel is a game-changer for mission-critical embedded systems, as it serves as a base for software-sensitive applications such as automotive, aviation, and military use cases.”
The potential real-world applications of the seL4 microkernel
The seL4 microkernel, which received the ACM Software System award, is known for its strong emphasis on formal verification, has several potential real-world applications due to its high performance and robust design. Notably, it has several potential use cases for embedded systems in several domains, particularly those utilized in mission-critical environments with a low margin of error. Here are a few examples of such use cases:
- Safety-Critical Systems: The seL4 microkernel’s high assurance properties make it well-suited for safety-critical applications such as aerospace, automotive, medical devices, and industrial control systems. These domains require dependable and secure operating systems to ensure the safety of humans and physical infrastructure. By providing strong isolation guarantees, seL4 can prevent faults in one component from affecting the entire system, thus enhancing overall system reliability.
- Secure Communication Systems: The microkernel’s emphasis on security and isolation makes it suitable for secure communication systems, particularly in scenarios where confidentiality, integrity, and authentication are critical. Applications like secure messaging platforms, encrypted voice or video communication, and secure data transfer can leverage seL4’s capabilities to protect sensitive information from unauthorized access or tampering.
- Internet of Things (IoT): The seL4 microkernel’s small size and minimalistic design make it a good fit for resource-constrained IoT devices. These devices often have limited processing power, memory, and energy capacity and require an efficient and secure operating system. SeL4 can enable IoT devices to function reliably and securely despite resource limitations by providing strong isolation and security features while being resource-efficient.
How LEARN connects Sri Lankan academics with the world
The LEARN network services have helped Dr. Elkaduwe, associated with the University of Peradeniya, connect and collaborate with universities worldwide. The network provides an exclusive leased line fibre connection to the University of Peradeniya, providing a remarkable bandwidth of 2Gbps. This high-speed internet connectivity is immensely beneficial for the university’s academic community. It facilitates the seamless transmission and analysis of vast volumes of data associated with research undertakings.
Moreover, this robust network infrastructure is a crucial foundation for fostering collaborative research initiatives among the centre and its partners by availing Ph.D. positions and student internships. Reflecting on the impact of LEARN’s many initiatives, Dr. Elkaduwe conveyed, “The world is opening up, and knowledge is everywhere. LEARN promotes enthusiasm among university students to self-learn and do their research through links to the outside world.”
Ultimately, NRENs like LEARN and other National Research and Education Networks are vital in empowering researchers to pursue knowledge and connect them with the world. NRENs enable researchers to collaborate more effectively and efficiently with colleagues across different institutions and countries by offering high-speed internet connectivity and access to diverse digital resources. These networks serve as bridges, connecting researchers to a global community of peers and experts, facilitating the exchange of ideas, and fostering international collaborations. Thereby enabling the advancement of knowledge, addressing pressing global challenges, and promoting a worldwide collaborative effort of research excellence.