Australiërs ontwikkelen superveilige kernel

28 augustus 2009

De zogeheten Secure Embedded L4-kernel is getest met een geautomatiseerd testsysteem. Nicta heeft ruim vier jaar gewerkt aan de kernel met een team wiskundigen en de open-sourceverficatietool Isabelle, die aan de Technische Universiteit van München is ontwikkeld.

De seL4-kernel is een kleine, high-performance kernel van de derde generatie die bestaat uit rond de 9000 regels C-code. Alle privileges voor toegang tot hardware zijn vastgelegd in de kernel, die de toegang regelt tot die hardware voor de rest van het systeem. Een vergelijkbare kernel, de OKL4 van Open Kernel Labs, wordt in veel smartphones gebruikt.

De onderzoekers hebben aangetoond dat seL4 voldoet aan de afgesproken abstracte, wiskundige specificaties. Nicta heeft daartoe alle ruim 7500 regels code geautomatiseerd getest aan de hand van formele wiskundige methoden. De specificaties waaraan de regels moeten voldoen zijn volgens deze formele wiskundige methoden vastgesteld en vervolgens formeel geverifieerd. Daarmee is bewezen dat elke regel consistent is met de specificaties. Een en ander resulteert in een kernel die niet bevattelijk is voor een groot aantal veelgebruikte digitale aanvalsmethoden, zoals bufferoverflowaanvallen.

De tests zijn uitgevoerd met Isabelle. Isabelle is een interactief programma waarmee wiskundige stellingen (theorema’s) getest kunnen worden. Voor de seL4-kernel werden 7500 regels code getest op meer dan 10.000 theorema’s, wat meer dan 200.000 regels formeel bewijs opleverde. Daarmee is het een van grootste geautomatiseerde testen die ooit werd uitgevoerd. Eerder ging het hoogstens om programma’s van enkele honderden regels code. Bovendien gaat het om een kernel, wat veel complexere software is dan een gemiddeld programma.

De onderzoekers benadrukken wel dat de kernel niet gegarandeerd foutloos is. Zij garanderen slechts dat de kernel niet afwijkt van de specificaties. Er kunnen nog altijd lekken zitten in de implementatiedetails onder het niveau van de programmeertaal C.

De kernel is geschikt als basis voor allerhande applicaties, maar Nicta mikt er vooral mee op kritische toepassingen voor de luchtvaartindustrie, zorg en defensie. Uitgangspunt voor de onderzoekers was tevens dat de prestaties van de kernel hoogstens 10 procent lager zouden liggen dan in vergelijkbare kernels. Reden hiervoor is dat de kernel ook echt bedoeld is voor commercieel gebruik.
Het intellectueel eigendom zal overgebracht worden naar Open Kernel Labs, dat een spin-off is van Nicta. Op diens embedded hypervisorsoftware draaien al honderden miljoenen consumentenapparaten.

Nicta verwacht rond 2011 producten te kunnen aanbieden die gebruikmaken van seL4. Volgens de onderzoekers is L4 ook zeer geschikt voor gebruik in gevirtualiseerde omgevingen. Data kunnen veilig apart worden opgeslagen op dezelfde fysieke server, maar logisch en veiligheidstechnisch op gescheiden virtuele servers.

 
Lees het hele artikel
Je kunt dit artikel lezen nadat je bent ingelogd. Ben je nieuw bij AG Connect, registreer je dan gratis!

Registreren

  • Direct toegang tot AGConnect.nl
  • Dagelijks een AGConnect nieuwsbrief
  • 30 dagen onbeperkte toegang tot AGConnect.nl

Ben je abonnee, maar heb je nog geen account? Neem contact met ons op!