Omfatta kraften i formella metoder i min kodningsresa: Hur jag blev en Dafny-evangelist

blogg 1NyheterUtvecklareFöretagBlockchain förklaradeHändelser och konferenserPressNyhetsbrev

Prenumerera på vårt nyhetsbrev.

E-postadress

Vi respekterar din integritet

HomeBlogDevelopers

Omfatta kraften i formella metoder i min kodningsresa: Hur jag blev en Dafny-evangelist

av ConsenSys 22 december 2020 Upplagt 22 december 2020

Skärmdump 2020 12 15 kl 6 46 32 1

Av Joanne Fuller

Jag vill börja med att säga att jag skriver detta blogginlägg i hopp om att andra kan uppleva det uppenbarande ögonblick som jag hade när jag lärde mig Dafny som en del av min utforskning av formella metoder. Vidare är det mitt hopp att detta inlägg kommer att fungera som en katalysator för andra att betrakta formella metoder som en kritisk och nödvändig färdighet inom arsenalen för alla som skriver kod. Som en del av Automatiserat verifieringsteam inom R&D på ConsenSys, Jag använder Dafny i den formella verifieringen av Ethereum 2 fas 0-specifikationen, och jag vill berätta varför jag tycker det är användbart.

Min bakgrund

Jag bör göra det klart att jag inte är programvaruutvecklare utan snarare anser mig vara en matematisk programmerare med viss kunskap om programvaruutveckling. Jag lärde mig först att skriva program som en del av min matematiklek under mitt sista år på gymnasiet och jag borde nog nämna att även om jag ganska gillade att använda datorer vid den tiden, var möjligheten att lära mig att programmera skrämde mig till den punkt där jag nästan tappade just den matematikklassen. Efter att ha beslutat att möta min rädsla för misslyckande (med avseende på att lära mig programmera och potentiellt förstöra mitt resultat i den här klassen) fortsatte jag med att uppleva mitt första epifani-ögonblick i samband med programmering. Jag kan fortfarande tydligt komma ihåg att jag satt i klassen och insåg att det inte var någon magisk och mystisk process att skriva ett program för att lösa ett matematikproblem, det var nästan som att skriva ner hur jag skulle arbeta igenom ett problem i mitt huvud. Det var ingen blick tillbaka efter det! 

Programmering har varit en viktig aspekt av allt jag har gjort sedan dess. Min doktorsexamen i kryptografi litade starkt på förmågan att utveckla algoritmer och sedan programmera optimala implementeringar. Mina program var skrivna för experiment och även om jag inte gjorde det vi nu skulle beteckna som formell testning skulle jag informellt kontrollera gränser och testa fall med logiskt resonemang om den avsedda utdata. Jag arbetade också i många år som akademisk forskning inom finans och ekonomi. Återigen inkluderade detta skrivprogram, och igen använde jag mina egna tekniker för att informellt testa och resonera om deras korrekthet. 

Det är rättvist att säga att även om jag uppskattade det faktum att testning alltid skulle vara ofullständig i den meningen att det var omöjligt att testa varje fall; att jag var ganska övertygad om att mitt matematiska tänkande var ganska bra när det gällde informell testning på ett noggrant sätt. Som sådan hade jag definitivt inte en fullständig uppskattning av skillnaden mellan att testa och bevisa riktighet eller konsekvenserna av sådana! Under min karriär innan jag gick med i ConsenSys var jag nöjd med att lita på mina egna informella tekniker för att bestämma vad jag tyckte var riktighet via testning. 

Min bakgrund är därför en del av berättelsen, eftersom jag själv är lite förvånad över att jag inte upptäckte formella metoder tidigare. Jag anser mig vara en matematiker; Jag älskar matematik, algoritmer och logik. Det verkar nu galet att helt enkelt förlita sig på ofullständig testning, men det verkar också galen för alla som programmerar att inte åtminstone uppskatta vad formella metoder kan erbjuda och de potentiella konsekvenserna av att missa ett fel med tanke på de många sätt som datorprogram är integrerade i våra liv. Formella metoder gör det möjligt för oss att gå utöver testning, för att bevisa att ett program är korrekt mot en specifikation som innehåller förhållanden före och efter. 

Ett första Dafny-exempel

Som ett enkelt exempel överväga heldelningen av en icke-negativ utdelning n med en positiv delare d; 

n / d

visas nedan:

Även om vi i ett skrivet programmeringsspråk kan begränsa ingångsparametrarna något är det inte alltid tillräckligt. I detta exempel betyder specifikationen av n och d som naturliga tal att båda ingångarna måste vara icke-negativa heltal men det föreskriver inte begränsningen av d till att vara ett positivt heltal. Användningen av ett förhandsvillkor genom kravförklaringen föreskriver en sådan begränsning och innebär att denna metod endast kan anropas om d > 0. Följaktligen, om någon annan del av programmet skulle orsaka att div anropas utan att en sådan förutsättning är uppfylld, kommer programmet inte att verifiera. Säkerhetsuttalandet ger sedan postvillkoret och ger en formell specifikation av vad metodutmatningen måste uppfylla.

Detta exempel är skrivet med Dafny: “Ett språk- och programverifierare för funktionell korrekthet” och tar mig till min nästa punkt, det vill säga varför jag är ett sådant fan av Dafny. Jag tycker att det är rättvist att säga att tanken på att använda ”formella metoder” för att verifiera programmets riktighet är för många programmerare något skrämmande och uppfattas ofta som ”för” svår. Oavsett om detta beror på brist på exponering för teknikerna, bristande uppskattning av fördelarna eller till och med brist på utbildning inom detta område; oavsett orsakerna tror jag att Dafny har förmågan att låta alla programmerare snabbt uppnå framgång när de tillämpar formella metoder i sitt arbete. Om jag tittar på kodavsnittet ovan, förväntar jag mig att alla med viss programmeringskunskap kan läsa denna Dafny-kod; Dafny är väldigt mycket ett programmerarvänligt språk. När du väl har lärt dig lite av Dafny är det väldigt enkelt att börja experimentera och sedan i princip lära dig när du går. Och om du är intresserad av att lära dig Dafny, är det ett bra ställe att börja handledningsserie av Microsoft. Webbplatsen innehåller också en online-redaktör, så det är väldigt enkelt att prova handledningsexemplen. De Verification Corner YouTube-kanal är en annan källa till användbara referenser.

Mitt epiphany ögonblick

Äntligen ville jag dela mitt epifani-ögonblick från när jag lärde mig Dafny. Jag har säkert hört historier om korta och enkla kodbitar, från stora ansedda företag, som har fel som missades och i slutändan kostade många miljoner dollar; men jag tror att det är först när du själv inser hur lätt det skulle vara att oavsiktligt skapa en bugg i en enkel funktion som allt är vettigt! Det ögonblick när du säger till dig själv “Åh, det skulle vara så lätt att göra det misstaget!”

Mitt ögonblick kom när jag tittade på en av Verification Corner-videor

I den här självstudien går Rustan Leino igenom en SumMax-metod som tar två heltal, x och y, och returnerar summan respektive max, s och m. Detta exempel är relativt enkelt och Dafny-koden visas nedan.

Ingångarna x och y specificeras som heltal genom att skriva och inga andra förutsättningar krävs. De tre postförhållandena ger kontroller om att utdata verkligen uppfyller specifikationerna, nämligen att s gör lika med x + y, och att m är lika med antingen x eller y och att m inte överstiger x och y. SumMaxBackwards-metoden presenteras sedan som en övning och det är här det blir mer intressant. Specifikationen är det motsatta av SumMax, dvs med tanke på summan och den maximala avkastningen som heltal x och y. Ok, så ett första försök kan vara med samma postvillkor; eftersom relationerna mellan ingångar och utgångar fortfarande kvarstår. Om vi ​​låter x vara det maximala, säger en snabb bit algebra oss att y ska vara lika med summan minus det maximala. Att lägga in detta i online-redigeraren ger följande.

Skärmdump 2020 12 15 kl 6 38 37 1 Skärmdump 2020 12 16 kl

Det verifierar inte. Så vad gick fel? Vi får höra att en postcondition inte höll och specifikt postconditionen på rad 3 (säkerställer x<= m && y <= m) kanske inte håller. När vi tittar närmare ser vi att detta postvillkor anger att x <= m och y <= m. Vi vet att x är mindre än eller lika med m eftersom vi ställer x lika med m, så det betyder att y <= m del verifierar inte. Hur kan detta hända? Vår algebra berättade att y: = s – m. Låt oss säga att s är 5 och m är 3, då y = 5 – 3 = 2 vilket säkerställer y <= m; men låt oss säga att vi kallar den här metoden med s lika med 5 och m lika med 1. Ingenting hindrar oss från att anropa metoden med dessa ingångsparametrar men att göra det kommer att orsaka ett problem som y = 5 – 1 = 4 och sedan y > m. I grund och botten är det vi ser här att även om ingångsparametern är avsedd att vara högst två heltal som skapar summan, så finns det inget som hindrar oss från att försöka ringa metoden med en inmatning som inte är giltig. Om inte en förutsättning är inkluderad för att begränsa ingångarna för s och m till giltiga heltal som kommer att resultera i utgångar x och y som uppfyller specifikationen, kan vår metod ge felaktiga resultat. Vilket förhållande behöver vi mellan s och m för att ge giltiga ingångar? Lite mer algebra visar oss att det är <= m * 2 för att det ska finnas en giltig lösning av x och y. Om vi ​​lägger till detta som en förutsättning kan Dafny nu verifiera koden enligt nedan. 

Skärmdump 2020 12 15 kl 6 46 32 1 Skärmdump 12 12 16 kl. 5 37 39

Detta var exemplet där jag kunde se hur enkelt det är att införa ett fel i koden. Bara för att vi kallar ingångsparametrarna ‘s’ för summa och ‘m’ för maximalt betyder inte att metoden kommer att anropas på lämpligt sätt och som sådan som en del av ett större program kan det bli många oavsiktliga konsekvenser som följer av detta typ av fel. Jag hoppas att det är användbart för någon annan som lär sig mer om Dafny eller formella metoder mer generellt.

Vad jag jobbar med nu

Det leder mig till slutet av mitt inlägg. Om du vill se vad jag för närvarande arbetar med Dafny, kolla in det här GitHub repo. Jag är en del av Automated Verification Team inom R&D vid ConsenSys och vi använder Dafny i den formella verifieringen av Ethereum 2 fas 0-specifikationen. Användningen av formella metoder i blockchain-utrymmet är ett spännande nytt forskningsområde som har anammats av ConsenSys och jag skulle uppmuntra alla som är intresserade av att lära sig mer om Eth 2.0 att titta på de resurser som finns tillgängliga i vårt projektrepa.

Prenumerera på vårt nyhetsbrev för de senaste Ethereum-nyheterna, företagslösningar, utvecklarresurser och mer.

Mike Owergreen Administrator
Sorry! The Author has not filled his profile.
follow me
Like this post? Please share to your friends:
map