Nye værktøjer kan give jernbeklædt vished om, at computerfejl hører fortiden til

Det er slemt nok at miste en times arbejde, når din computer går ned - men i indstillinger som sundhedspleje og luftfart, softwarefejl kan have langt mere alvorlige konsekvenser. I et berygtet tilfælde, en computerfejl fik kræftpatienter til at modtage dødelige overdoser fra en strålebehandlingsmaskine; i nyere overskrifter, mangelfuld software fik skylden for flystyrt i Etiopien og Indonesien.

Nu forskere ved Stevens Institute of Technology, i samarbejde med Yale University, udvikler værktøjer, der kan gøre katastrofale computeruheld langt mindre sandsynlige. Anført af Eric Koskinen, en assisterende professor i datalogi ved Stevens, arbejdet sigter ikke kun på at sikre, at programmer kører korrekt i specifikke situationer, men bruger også algoritmer til at bestemme, om det er logisk muligt, under alle omstændigheder, for software til at producere uønskede resultater.

"Det, vi sigter efter, er en 100 procent garanti for, at du aldrig vil støde på en fejl, " sagde Koskinen.

Koskinens hold, støttet af over $2,5 millioner fra Office of Naval Research, modellerer forskelle mellem to versioner af et program. Det er nyttigt, fordi programmører ofte arbejder ved at bygge på eksisterende software, i stedet for at skrive kode fra bunden, og fejl kan introduceres fra den ene version til den næste. Denne tilgang er især værdifuld for militæret, da forsvarsagenturer ofte køber software fra private entreprenører, foretag derefter ændringer internt, før du implementerer dem i missionskritiske situationer.

"De har brug for en måde at bekræfte, at de har foretaget ændringer korrekt internt, og har ikke introduceret nye problemer, " sagde Koskinen.

For at bevise matematisk, at et computerprogram aldrig kunne have nogen form for fejl, uanset hvilke omstændigheder, forventet eller uventet, Koskinens team bruger en strategi kaldet tidsmæssig logik. I stedet for at granske individuelle kodelinjer for at se efter syntaktiske forskelle, holdet, herunder adjunkt Jun Xu, en ekspert i binær analyse hos Stevens, ser på, hvordan et program opfører sig over tid. Ideen er at bevise, at uanset hvor længe programmet kører, der er ingen logisk måde for det nogensinde at returnere et uønsket resultat.

Modellering af et programs struktur og adfærd, i stedet for at gennemsøge individuelle kodelinjer, er vigtigt, fordi nøjagtig de samme kodelinjer kan have forskellige effekter i forskellige sammenhænge, ligesom kodelinjer, der ser meget forskellige ud, kan udrette det samme. Det er som at studere et juridisk dokument, Koskinen forklarer:at ændre et enkelt ord kan virke trivielt, men kan ændre hele betydningen af ​​dokumentet. Temporal logik hjælper med at modellere et programs potentiale, få kraftfuld indsigt i programmets muligheder i den virkelige verden.

Holdets tilgang tillader også, at man kan eliminere fejl i kommerciel software fra hylden, hvor kildekoden ikke er tilgængelig. Uden kildekoden, teamet er overladt til at sammenligne computerprogrammer ved hjælp af den binære version af kildekoden. "Det er svært at se, om sårbarheden virkelig er blevet elimineret, hvis du ikke kan se kildekoden, " sagde han. "De teknikker, vi bygger, vil gøre det:hvis du har en version af softwaren, som du stoler på, vores teknikker vil være i stand til at hjælpe dig med at opdage ændringer – sårbarheder i softwareopdateringer eller malware indsat i eksekverbare programmer – og beslutte, om du vil stole på den nye version."

Koskinens team er også ved at udvikle et værktøjssæt, som andre forskere og medlemmer af offentligheden vil være i stand til at bruge til at teste software – og de opskalerer deres tilgang til at arbejde med større programmer og mere komplekse fejl. "Dette er store problemer, der plager moderne computersystemer, " sagde Koskinen. "Disse problemer vil kun blive mere kritiske - inden for områder som sundhedspleje, luftfart, autonome køretøjer, og mange flere – så det er vigtigt, at vi udvikler praktiske teknikker til at gøre computerstyrede systemer fejlfrie og sikre at bruge."