Verifiable Software Diversity

Abstract

Programvarudiversitet erbjuder feltolerans genom att ersätta beroendet av en enskild programvarulösning med en population av alternativ som kan jämföras och användas för växling eller majoritetsomröstning. För att infria detta löfte krävs mer än nominell variation: alternativen måste uppfylla ett gemensamt beteendekontrakt och uppvisa tillräckligt åtskilda felbeteenden under relevanta förhållanden. I distribuerade driftsättningar kan diversiteten dessutom vara skenbar om deltagarna inte kan visa att de uppgivna varianterna faktiskt har byggts eller körts. Det första problemet kräver empirisk validering; det andra kräver verifierbar proveniens.

Denna avhandling föreslår ett ramverk för verifierbar programvarudiversitet uppbyggt kring en evidenskedja. Kedjan består av fyra länkar: belägg för att skilda varianter existerar för en given specifikation; belägg för att de är utbytbara för ett definierat ändamål; mätningar av sambanden mellan deras fel under relevanta förhållanden; samt provenienskontroller som knyter de uppgivna varianterna till de artefakter som faktiskt har producerats och driftsatts. Varje länk underbygger ett eget påstående och kan inte ersätta de andra. Proveniens bevisar i synnerhet inte korrekthet eller tillförlitlighet, medan diversitet på källkodsnivå inte bevisar beteendeekvivalens eller feloberoende.

De fem ingående delarbetena utvecklar metoder för att samla in och validera belägg för varje länk. De studerar naturligt förekommande diversitet bland blockkedjeklienter och diversitet som genereras av stora språkmodeller och kodningsagenter. Kompilering, testning, ekvivalenskontroll och diversitetsmätning avgör om kandidatversioner är utbytbara. Sammanfallande fel, felkorrelationer och majoritetsomröstningars beteende beskriver separationen mellan felutfall. Betrodd exekvering och nollkunskapsbevis gör påståenden om programvaruanvändning och kompilering kontrollerbara oberoende av varandra. Studierna granskar även de driftskostnader, tillitsantaganden och incitament som avgör om metoderna kan införas.

Resultaten visar att verifierbar programvarudiversitet är genomförbar och användbar, men att fördelarna har ett pris. Oberoende utvecklade och genererade varianter kan ge meningsfull diversitet, redundant exekvering kan förbättra tillgängligheten eller minska antalet observerade fel, och verifierbar proveniens kan göra påståenden om användningen av olika programvaruvarianter oberoende kontrollerbara. Dessa vinster kräver dock ytterligare resurser för redundant exekvering, arbete med att generera och validera varianter samt beräkningsresurser för att producera och verifiera belägg för proveniens. Med dessa avvägningar tydliggjorda erbjuder verifierbar programvarudiversitet en praktisk väg mot programvarusystem som är både mer tillförlitliga och mer granskningsbara.

Link to DiVA