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.
Volgens NICTA is het mogelijk om financiële software helemaal veilig te houden en tegelijkertijd ‘onbetrouwbare software’ op dezelfde computer te draaien. Ook zou seL4 bedrijfskritische defensiegegevens helemaal veilig kunnen opslaan, terwijl op hetzelfde systeem gebruik wordt gemaakt van aplicaties als e-mail. Ook kan het gebruikt worden om bijvoorbeeld levens ondersteunende apparaten van medische aard te beschermen tegen hackers. Computerworld Australia meldde dat het onderzoeksinstituut een samenwerkingsverband met Microsoft, de Australian National University (ANU) en de Commonwealth Scientific and Industrial Research Organisation (CSIRO) is aangegaan, dat er op is gericht onderzoekers te voorzien van Cloud Computing bronnen en ondersteuning. ‘The seL4 microkernel is a key enabler of our work. It provides a minimal and efficient lowest software level, and is the only part of our software that executes in the privileged mode of the hardware. It is a third-generation microkernel that builds on the strengths of the L4 microkernel architecture, such as small size, high performance, and policy freedom, and extends it with a built-in capability model, which provides a mechanism to enforce security guarantees at the operating system and application levels’, zo wordt op de website van NICTA bij SeL4 geschreven.
