science >> Wetenschap >  >> Elektronica

Nieuwe tools kunnen de ijzeren zekerheid bieden dat computerbugs tot het verleden behoren

Krediet:Stevens Institute of Technology

Het is al erg genoeg om een ​​uur werk te verliezen als je computer crasht, maar in instellingen zoals gezondheidszorg en luchtvaart, softwarestoringen kunnen veel ernstiger gevolgen hebben. In een berucht geval een computerbug zorgde ervoor dat kankerpatiënten dodelijke overdoses kregen van een bestralingsapparaat; in meer recente koppen, gebrekkige software kreeg de schuld van vliegtuigcrashes in Ethiopië en Indonesië.

Nu onderzoekers van Stevens Institute of Technology, in samenwerking met Yale University, ontwikkelen tools die catastrofale computerongelukken veel minder waarschijnlijk kunnen maken. Onder leiding van Eric Koskinen, een assistent-professor computerwetenschappen aan Stevens, het werk heeft niet alleen tot doel ervoor te zorgen dat programma's in specifieke situaties correct worden uitgevoerd, maar gebruikt ook algoritmen om te bepalen of het logisch mogelijk is, onder welke omstandigheden dan ook, voor software om ongewenste resultaten te produceren.

"Waar we naar streven is een 100 procent garantie dat je nooit een bug tegenkomt, ' zei Koskinen.

Het Koskinen-team, ondersteund door meer dan $ 2,5 miljoen van het Office of Naval Research, modellen verschillen tussen twee versies van een programma. Dat is handig omdat programmeurs vaak voortbouwen op bestaande software, in plaats van helemaal opnieuw code te schrijven, en bugs kunnen van de ene versie naar de andere worden geïntroduceerd. Deze benadering is vooral waardevol voor het leger, aangezien defensiebureaus vaak software kopen van particuliere aannemers, breng vervolgens intern wijzigingen aan voordat u ze toepast in bedrijfskritieke situaties.

"Ze hebben een manier nodig om te bevestigen dat ze intern de juiste wijzigingen hebben aangebracht, en geen nieuwe problemen hebben geïntroduceerd, ' zei Koskinen.

Om wiskundig te bewijzen dat een computerprogramma nooit een bug kan hebben, ongeacht de omstandigheden, verwacht of onvoorstelbaar, Het team van Koskinen gebruikt een strategie die temporele logica wordt genoemd. In plaats van afzonderlijke coderegels te onderzoeken om syntactische verschillen te zoeken, het team, waaronder assistent-professor Jun Xu, een expert in binaire analyse bij Stevens, kijkt naar hoe een programma zich in de loop van de tijd gedraagt. Het idee is om te bewijzen dat hoe lang het programma ook duurt, er is geen logische manier om ooit een ongewenst resultaat te retourneren.

De structuur en het gedrag van een programma modelleren, in plaats van zich te verdiepen in afzonderlijke coderegels, is belangrijk omdat exact dezelfde regels code verschillende effecten kunnen hebben in verschillende contexten, net zoals regels code die er heel anders uitzien, hetzelfde kunnen bereiken. Het is als het bestuderen van een juridisch document, Koskinen legt uit:het veranderen van een enkel woord lijkt misschien triviaal, maar kan de hele betekenis van het document veranderen. Temporele logica helpt om het potentieel van een programma te modelleren, het verkrijgen van krachtige inzichten in de real-world mogelijkheden van het programma.

De aanpak van het team maakt het ook mogelijk om bugs in kant-en-klare commerciële software te elimineren waarvoor de broncode niet beschikbaar is. Zonder de broncode, het team wordt overgelaten om computerprogramma's te vergelijken met behulp van de binaire versie van de broncode. "Het is moeilijk om te zien of de kwetsbaarheid echt is geëlimineerd als je de broncode niet kunt zien. " zei hij. "De technieken die we aan het bouwen zijn, zullen dat doen:als je een versie van de software hebt die je vertrouwt, onze technieken zullen je kunnen helpen om veranderingen op te sporen - kwetsbaarheden in software-updates of malware die in uitvoerbare programma's is ingevoegd - en om te beslissen of je de nieuwe versie vertrouwt."

Het team van Koskinen ontwikkelt ook een toolkit die andere onderzoekers en leden van het publiek kunnen gebruiken om software te testen - en ze schalen hun aanpak op om met grotere programma's en complexere storingen te werken. "Dit zijn grote problemen die moderne computersystemen teisteren, ", zei Koskinen. "Deze problemen zullen alleen maar kritischer worden - op gebieden als gezondheidszorg, luchtvaart, autonome voertuigen, en nog veel meer - dus het is van vitaal belang dat we praktische technieken ontwikkelen om computergestuurde systemen bugvrij en veilig in gebruik te maken."