4 februari 2011
Australische onderzoekers hebben software ontwikkeld die computers beschermt tegen falen of aanvallen van buitenaf. De seL4 microkernel is een klein besturingssysteem dat de toegang regelt tot de hardware van een computer. SeL4 kan onderscheid maken tussen betrouwbare en onbetrouwbare software. De software is de afgelopen zeven jaar ontwikkeld door National ICT Australia (NICTA) samen met Open Kernel Labs (OK Labs). De software is nu beschikbaar voor fabrikanten en onderzoekers om te testen. Volgens onderzoeker Gerwin Klein werd vorig jaar door de University of New South Wales (UNSW) voor het eerst bewezen dat een ‘general-purpose operating system kernel’ mogelijk was, de seL4. ‘Our seL4 microkernel is the subject of last year’s proof’, aldus Klein in een verklaring. ‘It is the only operating system kernel in existence whose source code has been mathematically proven to implement its specification correctly. Under the assumptions of the proof, the seL4 kernel for ARM11 will always do precisely what its specification says it will do’. Hierdoor kan de software niet falen, aldus de onderzoekers. Al sinds de jaren ’70 is er gezocht naar zulke software. ‘Verification of operating-system kernels has been attempted since the 1970s – we pulled it off !’, aldus Gernot Heiser, oprichter van OK Labs.