The ACM Software System Award is a prestigious honour that recognises outstanding achievements in developing software systems that have had a lasting impact on the field of computing. We are thrilled to announce that Dr Dhammika Elkaduwe, a Senior Lecturer in the Department of Computer Engineering at the University of Peradeniya, has been awarded the ACM Software System Award for 2022.
The ACM Software System Award is an annual award presented by the Association for Computing Machinery (ACM) since 1983. It recognises individuals or organisations that have developed a software system that has had a lasting influence on the field of computing, reflected in contributions to concepts, commercial acceptance, or both. The award includes a cash prize of $35,000 sponsored by IBM. The past winners of the award include some of the most influential figures in computing, such as Dennis Ritchie, Ken Thompson (UNIX), Tim Bernes Lee (World Wide Web), Vint Cerf (TCP/IP), Donald Knuth (TeX), Richard Stallman (GCC), Paul Mockapetris (DNS), and James Gosling (Java).
Dr Elkaduwe’s contributions to developing the seL4 microkernel, which is the first industrial-strength, high-performance operating system to have undergone complete, mechanically-checked proof of full functional correctness were essential to the project’s success, making him an integral part of the team that received this honour. The team consists of 14 individuals including Gernot Heiser and Kevin Elphinstone (University of New South Wales), Gerwin Klein, Rafal Kolanski and June Andronick (Proofcraft), Harvey Tuch (Google), David Cock (ETH Zurich), Philip Derrin (Qualcomm), Kai Engelhardt, Toby Murray (University of Melbourne), Michael Norrish (Australian National University), Thomas Sewell (University of Cambridge) and Simon Winwood (Galois) along with Dr Dhammika Elkaduwe.
The seL4 microkernel was first presented by the team in 2009 and has since undergone several proofs of correctness and security, including the enforcement of core security properties such as integrity and confidentiality. The team extended the proof to the binary code of the kernel and performed the first sound and complete worst-case execution-time analysis of a protected mode OS.
The seL4 high-assurance microkernel has changed the research community’s perception of what formal methods can achieve. It has demonstrated that it is possible to complete a formal proof of correctness and security for an industrial-strength operating system without compromising performance or generality. The continuously maintained and growing proofs on seL4 have given rise to a new discipline of proof engineering, which involves the modelling of the proof process, estimation of effort, and systematic treatment of large-scale proofs. Dr Elkaduwe’s work on the seL4 project has significantly impacted the research community and has fundamentally changed the way formal methods are perceived in computing.
It is noteworthy that Dr Elkaduwe is the first Sri Lankan and second Asian to receive this award, highlighting his exceptional achievement and bringing pride to our department and the University of Peradeniya. Dr Ekladuwe graduated from Peradeniya with an Engineering degree in 2002 and joined the same University as a junior academic then. He is a senior lecturer of the Department of Computer Engineering since 2009 and was the Head of the Department from 2013-2019. This accomplishment is a testament to the calibre of talent and expertise within the Department of Computer Engineering at Peradeniya and underscores our commitment to cutting-edge research and innovation.
The recognition of Dr Elkaduwe’s work by the ACM underscores the importance of his contributions to the development of the seL4 microkernel and the impact of his work on the field of computing. We are incredibly proud of Dr Elkaduwe and his team’s achievement, and we look forward to his continued contributions to the field of computer engineering.
Reported by Isara Tilakerathne
