The seL4 open microkernel project has received the ACM Software System Award, an annual award given by the Association for Computing Machinery (ACM), the most respected international organization in the field of computer systems. The award is given for achievements in the field of mathematical proof of operation, which indicates full compliance with specifications given in a formal language and recognizes readiness for use in mission-critical applications. The seL4 project has shown that it is not only possible to fully formally verify reliability and security for projects at the level of industrial operating systems, but also to achieve this without sacrificing performance and versatility.
The ACM Software System Award is presented annually to recognize the development of software systems that have had a defining impact on the industry, introducing new concepts or opening up new commercial applications. The amount of the award is 35 thousand US dollars. In past years, ACM awards have been given to the GCC and LLVM projects, and their founders Richard Stallman and Chris Latner. Other projects and technologies that were also awarded were UNIX, Java, Apache, Mosaic, WWW, Smalltalk, PostScript, TeX, Tcl/Tk, RPC, Make, DNS, AFS, Eiffel, VMware, Wireshark, Jupyter Notebooks, Berkeley DB and eclipse.
The architecture of the seL4 microkernel is notable for the removal of parts for managing kernel resources in user space and for applying the same means of access control for such resources as for user resources. The microkernel does not provide out-of-the-box high-level abstractions for managing files, processes, network connections, and the like, instead it provides only minimal mechanisms for controlling access to the physical address space, interrupts, and processor resources. High-level abstractions and drivers for interacting with hardware are implemented separately on top of the microkernel in the form of user-level tasks. The access of such tasks to the resources available to the microkernel is organized through the definition of rules.
Source: opennet.ru