Microsoft Research kunngjorde i forrige uke at en gruppe forskere har gjort en stor oppdagelse innen informatikk, nemlig utviklingen av en metode som gjør det mulig å bygge distribuerte programvaresystemer som kan bevises at er feilfrie.
– Programverifisering har vært en hellig gral for informatikk i 40 eller 50 år, sier Bryan Parno, en Microsoft-forsker som har deltatt i prosjektet og er medforfatter av den vitenskapelig artikkelen, som i går ble presentert under konferansen 25th ACM Symposium on Operating Systems Principles i Monterey, California.
Leste du denne? Nytt filsystem garanterer mot datatap etter krasj
IronFleet
Prosjektet kalles for IronFleet og er rettet mot systemer som spenner på tvers av flere datamaskiner. Feil kan lett oppstå i slike systemer dersom ikke utviklerne tar hensyn til alle de ulike, komplekse måtene systemene må kunne samhandle på.
Forskerne nevner som eksempel at en bank kan ha et distribuert system som lar bankens mange servere koordinere seg med hverandre. Det er ikke rom for feil i dette systemet, siden en kundes innskuddsforespørsel kan komme inn på én server, mens en senere uttaksforespørsel kan bli sendt til en annen server. Banken må vite at begge transaksjoner blir registrert på en konsistent måte.
Les også: Dette skjer når kunstig intelligens får dagdrømme
I det små
Forskerne er nøye med å fortelle at man fortsatt er langt unna en verden hvor man på en realistisk måte kan bygge store og kompliserte programmer, for eksempel omfattende operativsystemer, som kan garanteres å være feilfrie.
Men ifølge Microsoft mener forskerne at de nylige framskrittene har gjort det mulig å skrive mindre programvare som matematisk kan bevises å ha feil som kan utgjøre en sårbarhet eller få programmet til å henge.
Ifølge forskerne kreves vil det være dyrere å utvikle slik feilfri kode, men at dette likevel kan forsvares i systemer hvor feilfrihet er svært viktig, som i det nevne banksystemet.
– I begynnelsen vil vi konsentrere oss om små, men kritiske biter med programvare, hvor sikkerhet og pålitelighet er viktig, sier Parno.
Mer forskning hos Microsoft: Forsker på ordentlig smarte batterier
Ikke mennesker
Kollegaen Jay Lorch legger til at forskerne dessuten kun jobber med systemer som samhandler med andre datamaskiner. Årsaken til dette er at mennesker er så lite forutsigbare.
– Mennesker er veldig komplekse, så å forsøke å spesifisere hvordan et menneske samhandler med et program, er temmelig komplekst, sier Lorch.
Mangedoblet fart
Ifølge en tredje forsker som deltar i prosjektet, Chris Hawblitzel, er det kombinasjonen av forbedre maskinvare og programvare, sammen med raskere algoritmer som har blitt utviklet ved Microsoft Research, som har gjort verifiseringsarbeidet mulig.
Han forteller at det for et tiår siden kunne ha tatt en menneskealder å kjøre de verifiseringsverktøyene som er nødvendige for å avgjøre om systemet til forskerne er korrekt. Nå tar det bare seks timer på en enkelt datamaskin.
– Disse verktøyene har endelig begynt å nærme seg det punktet hvor utviklere kan begynne å skrive kode på denne måten, sier Lorch.
Les gjerne også denne: – Ingen ulemper ved å utvikle universelle Windows-apper
Revolusjon
– Dersom vi lykkes, vil folk om 10 eller 15 år fra nå se seg tilbake og si «Jeg kan ikke tro at de pleide å skrive kode på den måten», sier Parno.
– Det er som leger som utfører kirurgi uten anestesi eller å sterilisere utstyret.
Fikk du med deg denne saken? I 1969 var det première for digitale valgprognoser
