Onderzoekers van de Yale Universiteit hebben een nieuw besturingssysteem genaamd CertiKOS onthuld dat als een doorbraak op het gebied van "hackerbestendige" besturingssystemen wordt omschreven. CertiKOS controleert of een programma zich op de bedoelde manier gedraagt.

Een belangrijk onderdeel van CertiKOS is dat het "concurrency" ondersteunt. Dit houdt in dat het gelijktijdig meerdere threads (kleine series van geprogrammeerde instructies) op meerdere processorkernen kan uitvoeren. Dit is een groot verschil ten opzichte van eerdere geverifieerde systemen en zorgt ervoor dat CertiKOS op moderne multicoresystemen kan draaien.

Voor de ontwikkeling van CertiKOS zijn verschillende nieuwe verificatietechnieken gebruikt. Zo hebben de onderzoekers de verschillende onafhankelijke onderdelen van de kernel losgekoppeld, de code in een grote verzameling van hiërarchische modules georganiseerd en vervolgens voor elke kernelmodule een wiskundige specificatie voor het beoogde gedrag van de module opgesteld. Dit gedrag is vervolgens te controleren.

Volgens de onderzoekers is een systeem zoals CertiKOS pas sinds kort mogelijk. Het bewijs voor een gecertificeerde kernel is namelijk onmogelijk door een mens te controleren. De laatste jaren zijn er echter krachtige computerprogramma's ontwikkeld die automatisch het bewijs kunnen genereren en controleren. "Dit is een fantastische ontwikkeling", zegt Greg Morrisette van de Cornell Universiteit. "Tien jaar geleden had niemand kunnen voorspellen dat we de correctheid van een single-threaded kernel konden bewijzen, laat staan van een multicorekernel."