Microsoft onderzoekt ontwikkeling van bugvrije software
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.
Daar moet ik om lachen. Als programmas bugvrij zijn, kunnen ze juist goed om gaan met onvoorspelbare situaties, want die brengen de bugs doorgaans aan het licht. Door zich deze limitering op te leggen, schrijven ze eigenlijk dat ze zelf niet 100% overtuigd zijn dat alles bugvrij is..
Iemand overigens al het pdf doorgelezen en een (gefundeerde) waarde oordeel kunnen geven?
Op het eerste gezicht lijkt het alsof er vooral om één functionaliteit wordt behandeld. Ofwel, bouw je een brok software waar deze functionaliteit in zit, dan geeft dit document handvatten om dat onderdeel bug vrij te bouwen. Maar ik beken onderhevig te zijn aan een TLDR (Too long, didn't read), dus ik kan ernaast zitten.
Afgezien van de personen die hiervoor hebben gereageerd: het blijft natuurlijk makkelijk om zo te reageren. jammer...
@karma4, ter info: IEFBR14 is een aantal maal herschreven, niet omdat er bugs in het programma zaten, maar 1. omdat JCL er niet goed mee om kon gaan en 2. omdat er extra, onvoorziene (meta)functionaliteit benodigd was. In essentie was IEFBR14 bug-vrij en zo gebleven.
Iemand overigens al het pdf doorgelezen en een (gefundeerde) waarde oordeel kunnen geven?
Op het eerste gezicht lijkt het alsof er vooral om één functionaliteit wordt behandeld. Ofwel, bouw je een brok software waar deze functionaliteit in zit, dan geeft dit document handvatten om dat onderdeel bug vrij te bouwen. Maar ik beken onderhevig te zijn aan een TLDR (Too long, didn't read), dus ik kan ernaast zitten.
Niet helemaal correct, ze hebben voor de bewijsvoering gefocussed op kleine, singlethreaded code geschreven in dafny. Er worden nog een aantal randvoorwaarden beschreven, maar vervolgens werkt de methodiek op iedere soortgelijke code. Wat ze wel beschrijven is dat er nog een stap te maken is bij complexe (miljoenen regels aan code) en multithreaded code.
De stap die nog gemaakt moet worden is de methode om snel te kunnen bewijzen dat de verschillende brokken geverifieerde code samen te voegen zijn, en hiervoor ook te bewijzen dat deze foutloos werkt.
LBRI (Long but read it)
"First bug: A program indicates its successful completion by zeroing register 15 before returning; this version of the null program "failed" every time." De returncode (R15) heeft niets met JCL te maken. Het is de conventie om aan te geven dat iets goed verwerkt is ja/(boel) nee's. Dat mag niet afhankelijk zijn van een onbekende registerstatus.
De tweede en derde zijn ook gewoon bugs.
Met de aangetrokken eisen door de tijd in het OS traden die fouten op. Het was woekeren met de ruimte in de antieke tijden https://en.wikipedia.org/wiki/IBM_System/360, sommige shortcuts werkten maar bleken later foutief te zijn. Het is de zelfde menselijke mentaliteit, die is niet veranderd. Dat is het meest kenmerkend De techniek wel, dat is minder van belang.
Testen is een vak je kan via http://www.istqb.org/ het nodige over gangbare systematische aanpak terug vinden. Door de genoemde PDF worstelend:
- Het gaat om distributed systemen die NIET multi-threaded zijn.
- In par 2.5 worden een aantal aannames gedaan van wat men correct verondersteld zonder verdere bewijsvoering
- Met dafny / Ironfleet wordt een test framework opgezet van automatisch testen met een 3 tal lagen waarin vaste mogelijke toestanden gedefinieerd worden.
Redelijk hoog niveau (zeer lastig te begrijpen) document wat echt een onderzoeks omgeving weergeeft.
Voor het meten in distributed systemen had ik https://logging.apache.org/ op het netvlies. Ook die is daarvoor bedoeld.
Ook wel eens kleine schoonheidsfoutjes,wat dus als onmerkbare bugs worden gezien.
Weet jij dan wel een leverancier die bug vrije software kan leveren? Dit zijn er niet zoveel.....
Ook wel eens kleine schoonheidsfoutjes,wat dus als onmerkbare bugs worden gezien.
daar gaat het nu juist om."nu bestaat bewezen bug free nog niet. Wat deze onderzoekers nu hebben gedaan is een grote stap gezet om code te kunnen schrijven waarvan wiskundig bewezen is dat deze geen bugs bevatten.
vandaar ook de term "heilig graal".
De stap die nog gemaakt moet worden is de methode om snel te kunnen bewijzen dat de verschillende brokken geverifieerde code samen te voegen zijn, en hiervoor ook te bewijzen dat deze foutloos werkt.
LBRI (Long but read it)
The LBRI made me smile. En nog bedankt voor de toelichting!
Deze posting is gelocked. Reageren is niet meer mogelijk.
Junior DevOps Engineer
Certified Secure is op zoek naar een Junior DevOps Engineer. Deze functie is een stuk interessanter dan de term doet vermoeden! Om jou als potentiële nieuwe collega meteen te laten zien wat we doen hebben we speciaal voor jou een selectie gemaakt van een aantal leuke security challenges. Are you ready for a challenge?
Cybersecurity Trainer / Streamer
Toe aan een nieuwe nieuwe job waarmee je het verschil maakt? In de Certified Secure trainingen laat je deelnemers zien hoe actuele kwetsbaarheden structureel verholpen worden. Ook werk je actief mee aan de ontwikkeling van onze gamified security challenges. Bij het maken van challenges kom je telkens nieuwe technieken tegen, van Flutter tot GraphQL, van Elastic Search tot Kubernetes.
