Proving Safety and Security of Binary Programs

QC 20230509

Abstract

Med datorer och inbyggda system förekommande överallt i dagens samhälle blir dessas korrekthet och säkerhet allt viktigare. I synnerhet måste mjukvarukomponenter som bidrar med viktig funktionalitet eller hanterar känslig data fungera som avsett. Exempel på komponenter är operativsystem som måste isolera applikationer, drivrutiner som måste kommunicera med hårdvaran på ett tillförlitligt sätt, kryptografiska rutiner som inte får läcka känslig information och fundamentala säkerhetsmekanismer vars resultat beror starkt på implementationens korrekthet. Alla dessa komponenter involverar hårdvaruaspekter som normalt sett inte involveras vid exekvering av applikationsprogram. För korrekt verifiering bör därför dessa komponenter analyseras på binär nivå.

Att verifiera binärkodsegenskaper är utmanande då kontrollflöden och minnesrepresentationer saknar struktur i binärkod, och för att verifieringen involverar komplexa hårdvarudetaljer. I denna avhandling förbättrar vi precisionen och tillförlitligheten i binärkodsanalys med hjälp av en interaktiv bevisassistent. Vi presenterar ramverket HolBA för binärkodsanalys, som vi har implementerat i den interaktiva bevisassistenten HOL4. HolBA möjliggör implementation av analysalgoritmer så att algoritmerna producerar maskinkontrollerade korrekthetsbevis för dessas beräknade resultat. Vi har använt HolBA för att implementera översättningsprocedurer från binärkod till det mer abstrakta programspråket BIR för att underlätta formell analys. HolBA har två bevisproducerande analysrutiner för att möjliggöra programverifiering: en rutin för symbolisk exekvering och en rutin som beräknar det minst restriktiva villkoret som garanterar att programets resultat satisfierar ett givet villkor. Vi utvärderar HolBA med hjälp av ett antal binära program, och en större fallstudie bestående av ett program som styr en självbalanserande robot. Robotmjukvarans exekveringstider har analyserats med symbolisk exekvering för att verifiera dess övre och undre tidsgränser.

Verifieringsresultatens tillförlitlighet beror på hur precist hårdvarumodellerna återspeglar den faktiska hårdvaran. Denna aspekt har fått begränsad uppmärksamhet i samband med säkerhet, där subtila hårdvaruoperationer kan utnyttjas vid angrepp. Vi presenterar Scam-V, en metod och ett verktyg för differentiell testning, som upptäcker skillnader i beteende mellan modell och hårdvara som kan ge upphov till säkerhetssårbarheter. I ett antal fallstudier med riktiga processorer hittades, tidigare okända, typer av informationsläckage.

urn.kb.se/resolve?urn=urn:nbn:se:kth:diva-326719