Towards a Trustworthy Stack: Formal Verification of Low-Level Hardware and Software

QC 20231221

Abstract

Datorsystem, bestående av hårdvara och mjukvara, har fått stor betydelse i den digitaliserade världen.Dessa datorsystem är beroende av kritiska komponenter för att tillhandahålla grundläggande funktionalitet och hantera känslig information. Ett grundläggande krav för dessa kritiska komponenter är funktionell korrekthet, vilket säkerställer att komponenterna fungerar som deras specifikationer föreskriver. Till exempel kommer en pipelineprocessor att exekvera instruktioner samtidigt i olika steg, till exempel hämtning, dekodning och utförande, och måste producera resultat som specificeras i instruktionsuppsättning (ISA) manualen. Utöver funktionell korrekthet är säkerhetsegenskaper som konfidentialitet och integritet också viktiga. Särskilt kräver konfidentialitet att känslig information endast är tillgänglig för auktoriserade användare. För att konstruera en korrekt och säker dator (dvs. en pålitlig stack), fokuserar denna avhandling på den funktionella korrektheten och konfidentialiteten hos periferiutrustningar och pipelined-processorer med hjälp av det interaktiva bevisprogrammet HOL4.

För funktionell korrekthet använder vi ett verifieringssätt baserat på för-fining där utförandet av ett målsystem begränsas av ett referenssystem. Vi har studerat detta för två olika målsystem, en synkron seriell peripheral interface (SPI) tillsammans med dess drivrutin, och en 5-stegs pipelined processor. Specifikt formaliserar vi en SPI-anordning och dess drivrutin, och presenterar en abstrakt modell som referenssystemet. Den abstrakta modellen säkerställer korrekt kommunikation i SPI:s halv- och hel-duplexlägen. Förfiningen mellan den abstrakta och SPI-modellerna fastställs med hjälp av svag bisimulering. För det andra implementerar och verifierar vi en 5-stegs in-order pipelined processor Silver-Pi för RISC ISA Silver. Korrektheten hos Silver-Pi bevisas genom att uppvisa ett förfiningsförhållande mellan processorernas exkveringsspår och Silver ISA.Silver-Pi är implementerad med det verifierade HOL4 Verilog-biblioteket, vilket säkerställer processorns korrekthet ner till dess Verilog-implementation.

För SPI-fallstudien säkerställer svag bisimulering att SPI-modellen har samma informationsflöden som den abstrakta modellen, vilket förhindrar skadliga drivrutinsoperationer, t.ex. en oändlig loop baserad på ett hemligt värde.

I allmänhet, för att förhindra läckage av hemligheter orsakade av fenomen som instruktionspipelining och omordnad (OoO) exekvering, kompletteras mål- och referenssystemen med observationer som extraherar synliga delar av maskinens tillstånd för angripare. Detta möjliggör att en mängd informationskanaler baserat på exempelvis tid och cacheåtkomstbeteende kan fångas upp. Som säkerhetspolicy använder vi begreppet konditionell icke-interferens (CNI), vilket garanterar att ett målsystem inte läcker ut mer information än vad referenssystemet tillåter.

För att analysera tidkanalen hos Silver-Pi, extraherar observationsfunktionen delar av ISA-tillståndet som kan påverka exekveringstiden för ett program.Med detta referenssystem bevisar vi att Silver-Pi uppfyller CNI.

För OoO-utförande presenterar vi formaliseringen av ett maskinoberoende språk, MIL, som använder en liten uppsättning primitiva händelser för att beskriva både in-order och OoO-utförande på en mikroarkitekturliknande nivå. Ett begrepp av CNI i MIL utesluter spårdrivna cache-sidokanaler genom att jämföra OoO och in-order utförande av ett program. En verifierad körbar semantik beräknar resultat och genererar observationer av MIL-program. Vi presenterar en semi-automatiserad verifieringsstrategi för CNI med hjälp av den körbara semantiken och demonstrerar denna strategi med flera exempel.

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