Nooit meer blauwe schermen of het installeren van beveiligingsupdates lijkt misschien toekomstmuziek, maar onderzoekers van Microsoft zeggen een manier te hebben gevonden om bugvrije software te produceren. "Programmaverificatie is de afgelopen 40 of 50 jaar de heilige graal in de informatica", aldus Bryan Parno, onderzoeker bij Microsoft die een paper over het project heeft gepubliceerd (pdf).

De onderzoekers waarschuwen dat ze nog ver verwijderd zijn van een wereld waar grote computerprogramma's, zoals besturingssystemen, bugvrij worden gebouwd. Recente ontwikkelingen hebben het echter mogelijk gemaakt om kleinschaligere software te schrijven waarvan wiskundig kan worden bewezen dat er geen fouten aanwezig zijn waardoor het programma vastloopt of beveiligingslekken bevat.

"Deze tools bereiken eindelijk het punt zodat ontwikkelaars op deze manier software kunnen programmeren", zegt Jay Lorch, een andere onderzoeker die aan het project meewerkt. Het gaat dan om betere hardware en snellere algoritmen. Op dit moment is het volgens de onderzoekers nog te kostbaar en onpraktisch om bijvoorbeeld een besturingssysteem op deze manier te ontwikkelen, aangezien dit soort systemen miljoenen regels code bevatten die vaak op ouder werk zijn gebaseerd.

In eerste instantie wordt er dan ook vooral gekeken naar systemen waar veiligheid en betrouwbaarheid erg belangrijk zijn. Ook richten de onderzoekers zich op systemen die alleen met andere computers communiceren, omdat ze voorspelbaarder zijn. "Mensen zijn zeer gecompliceerd, dus het specificeren van hoe een mens met een programma omgaat is zeer complex", aldus Lorch.

"Als we succesvol zijn, zullen mensen over 10 tot 15 jaar terugkijken en zeggen dat ze het niet kunnen geloven dat erop deze manier werd geprogrammeerd. Het wordt vergeleken met artsen die zonder verdoving of gesteriliseerde apparatuur opereren", voegt Parno toe. Het project, dat de naam IronFleet draagt, zal deze week tijdens het 25ste ACM Symposium over Operating Systems Principles worden gepresenteerd.