Syntes och verifiering av enhetsdrivrutiner

Enhetsdrivrutinen .

Enhetsdrivrutiner är program som tillåter programvara eller datorprogram på högre nivå att interagera med en hårdvaruenhet . Dessa programvarukomponenter fungerar som en länk mellan enheterna och operativsystemen, kommunicerar med vart och ett av dessa system och utför kommandon. De tillhandahåller ett abstraktionslager för programvaran ovan och förmedlar även kommunikationen mellan operativsystemets kärna och enheterna nedan.

Vanligtvis levereras operativsystemen med stöd för de vanliga drivrutinerna och vanligtvis tillhandahåller hårdvaruleverantörerna drivrutinen för sina hårdvaruenheter för de flesta plattformar. Den aggressiva skalningen av hårdvaruenheterna och de komplexa mjukvarukomponenterna har gjort utvecklingsprocessen för drivrutiner besvärlig och komplex. När storleken och funktionaliteten på drivrutinerna började öka blev drivrutinerna en nyckelfaktor för att definiera systemets tillförlitlighet . Detta har skapat ett incitament till automatisk syntes och verifiering av drivrutiner. Den här artikeln belyser några metoder för syntes och verifiering av drivrutiner.

Motivation för automatisk förarsyntes och verifiering

Drivrutiner är den huvudsakliga felkomponenten i de flesta system. Berkeley Open Infrastructure for Network Computing (BOINC)-projektet fann att OS-krascher huvudsakligen orsakas av dåligt skriven drivrutinskod. I Windows XP står drivrutiner för 85 % av de rapporterade felen. I Linux -kärnan 2.4.1 står drivrutinskoden för cirka 70 % av kodstorleken. Drivrutinsfelet kan krascha hela systemet när det körs i kärnläget . Dessa resultat resulterade i olika metoder och tekniker för verifiering av drivrutiner. Ett alternativ var att utveckla tekniker som kan syntetisera enhetsdrivrutiner robust. Mindre mänsklig interaktion i utvecklingsprocessen och korrekt specifikation av enheten och operativsystemen kan leda till mer pålitliga drivrutiner.

Den andra motivationen för drivrutinsyntes är det stora antalet varianter av operativsystem och enhetskombinationer. Var och en av dessa har sin egen uppsättning av in-/utgångskontroll och specifikationer som gör stöd för hårdvaruenheter på vart och ett av operativsystemen svårt. Så möjligheten att använda en enhet med ett operativsystem kräver tillgången till motsvarande enhetsdrivrutinkombination. Hårdvaruleverantörer tillhandahåller vanligtvis drivrutiner för Windows, Linux och Mac OS men på grund av de höga utvecklings- eller porteringskostnaderna och tekniska supportsvårigheterna kan de inte tillhandahålla drivrutiner på alla plattformar. En automatiserad syntesteknik kan hjälpa leverantörerna att tillhandahålla drivrutiner för att stödja alla enheter på alla operativsystem.

Verifiering av enhetsdrivrutiner

Det finns två utmaningar som begränsar testning av drivrutiner.

Det är mycket svårt att bestämma den exakta operationen eller tiden när det finns ett fel i interaktionen mellan drivrutinen och kärnan. Systemet kan gå in i något inkonsekvent tillstånd och kraschen rapporteras efter en lång tid, vilket suddar ut den verkliga orsaken till kraschen.
De drivrutiner som fungerar korrekt under normala omständigheter kan gå fel i sällsynta och exceptionella fall och de traditionella testteknikerna kanske inte hjälper till att upptäcka förarnas beteende i hörnfall.

Vågen av verifiering av enhetsdrivrutiner initierades av Microsoft genom deras SLAM-projekt redan år 2000. Motivationen för projektet var att 500 000 krascher som rapporterades om dagen visade sig vara orsakade av en videodrivrutin, vilket ledde till oro över den stora sårbarhet vid användning av komplexa drivrutiner. Mer detaljer finns här , i talet som hölls av Bill Gates. Ett stort antal statiska och runtime-tekniker har sedan dess föreslagits för feldetektering och isolering.

Statisk analys

Statisk analys innebär att man analyserar programmet för att kontrollera om det överensstämmer med de säkerhetskritiska egenskaper som anges. Till exempel bör systemprogramvaran följa regler som "kontrollera användarbehörigheter innan du skriver till kärndatastrukturer", "referera inte till nollpekare utan kontroll", "förbjud överfull buffertstorlek" etc. Sådana kontroller kan göras utan att faktiskt exekvera koden som kontrolleras. Att använda den traditionella testprocessen (dynamisk exekvering) kräver att man skriver många testfall för att utöva dessa vägar och driva systemet till feltillstånd. Denna process kan ta lång tid och ansträngning och är ingen praktisk lösning. Ett annat teoretiskt möjligt tillvägagångssätt är manuell inspektion, men detta är opraktiskt i moderna system där miljontals rader kod är inblandade, vilket gör logiken för komplex för att kunna analyseras av människor.

Kompilatortekniker

Reglerna som har en enkel mappning till källkoden kan kontrolleras med en kompilator. Regelöverträdelser kan hittas genom att kontrollera om källoperationen inte är meningsfull. Till exempel kan regler som "att aktivera ett avbrott efter att ha inaktiverats" kontrolleras genom att titta på ordningen på funktionsanrop. Men om källkodstypsystemet inte kan specificera reglerna i sin semantik, kan kompilatorerna inte fånga fel av det slaget. Många typsäkra språk tillåter minnessäkerhetsbrott som är ett resultat av osäker typcasting att upptäckas av kompilatorn.

Ett annat tillvägagångssätt är att använda kompilering på metanivå (MC) , . Metakompilatorer konstruerade för detta ändamål kan utöka kompilatorerna med lätta, systemspecifika checkers och optimerare. Dessa tillägg måste skrivas av systemimplementörer på ett högnivåspråk och dynamiskt länkade till kompilatorerna för att göra strikt statisk analys.

Programvarumodellkontroll

Programvarumodellkontroll är den algoritmiska analysen av program för att bevisa egenskaperna hos deras körningar. Detta automatiserar resonemanget om programmets beteende med hänsyn till de givna korrekta specifikationerna. Modellkontroll och symbolisk exekvering används för att verifiera de säkerhetskritiska egenskaperna hos enhetsdrivrutiner. Indata till modellkontrollen är programmet och de tidsmässiga säkerhetsegenskaperna. Utdata är beviset på att programmet är korrekt eller en demonstration av att det finns ett brott mot specifikationen med hjälp av ett motexempel i form av en specifik exekveringsväg.

Verktyget SDV (Static Driver Verifier) från Microsoft använder statisk analys för Windows enhetsdrivrutiner. Den bakre analysmotorn SLAM använde modellkontroll och symbolisk exekvering för statisk verifiering av kompileringstid. Reglerna som ska följas av drivrutinerna för varje API är specificerade i ett C-liknande språk SLIC (Specification Language for Interface Checking). Analysmotorn hittar alla sökvägar som kan leda till brott mot API-användningsreglerna och presenteras som felsökvägar på källnivå genom drivrutinens källkod. Internt abstraherar den C-koden till ett booleskt program och en uppsättning predikat som är regler som ska följas i detta program. Sedan använder den den symboliska modellkontrollen för att validera predikaten på det booleska programmet.

Modellkontrollen BLAST (Berkeley Lazy Abstraction Software verification Tool) används för att hitta minnessäkerhet och felaktiga låsningsfel i Linux-kärnkoden. Den använder en abstraktionsalgoritm som kallas lazy abstraction för att bygga modellen från drivrutinen C-koden. Det har lyckats verifiera tidsmässiga säkerhetsegenskaper för C-program med upp till 50K kodrader. Den används också för att avgöra om en ändring i källkoden påverkar egenskapsbeviset i den tidigare versionen och visas på en Windows-enhetsdrivrutin.

Avinux är ett annat verktyg som underlättar den automatiska analysen av Linux-enhetsenheter och är byggt ovanpå den avgränsade modellcheckaren CBMC. Det finns metoder för fellokalisering för att hitta felplatsen eftersom dessa modellkontrollverktyg returnerar en lång räknarexempelspårning och det är svårt att hitta den exakta felaktiga platsen.

Kör tidsanalys

Dynamisk programanalys utförs genom att programmet körs med tillräckliga testingångar för att producera intressanta beteenden. Safe Drive är ett system med låg overhead för att upptäcka och återhämta sig från typsäkerhetsöverträdelser i enhetsdrivrutiner. Med endast 4 % ändringar av källkoden för Linux-nätverksdrivrutiner kunde de implementera SafeDrive och ge bättre skydd och återställning till Linux-kärnan. Ett liknande projekt som använder hårdvara för att isolera drivrutinerna från huvudkärnan är Nook. De placerar enhetsdrivrutiner i en separat domän för hårdvaruskydd som kallas "nooks" och de har separata behörighetsinställningar för varje sida och ser till att en drivrutin inte ändrar sidor som inte finns i dess domän utan kan läsa all kärndata eftersom de delar samma adressutrymme .

Ett annat liknande arbete inom detta område är automatisk återställning av operativsystem på grund av drivrutinsfel. MINIX 3 är ett operativsystem som kan isolera större fel, defekter upptäcks och felaktiga komponenter byts ut i farten.

Syntes för enhetsdrivrutiner

Ett alternativ till verifiering och isolering av fel är att implementera tekniker i utvecklingsprocessen för drivrutiner för att göra den mer robust. Med tanke på en enhetsspecifikation och operativsystemfunktioner är en metod att syntetisera enhetsdrivrutiner för den enheten. Detta hjälper till att minska de mänskliga felen samt kostnaden och tiden som är involverad i att utveckla systemprogramvaran. Alla syntesmetoder förlitar sig på någon form av specifikation från maskinvaruenhetstillverkare och operativsystemfunktioner.

Gränssnittsspecifikationsspråk

Maskinvarudriftkoden är vanligtvis låg och är benägen att fel. Kodutvecklingsingenjören litar på hårdvarudokumentationen som vanligtvis innehåller oprecis eller felaktig information. Det finns flera Interface Definition Languages (IDL) för att uttrycka hårdvarufunktionerna. De moderna operativsystemen använder dessa IDL:er för att limma komponenter eller för att dölja heterogenitet, som fjärrstyrda proceduranrop IDL. Detsamma gäller hårdvarufunktioner. I det här avsnittet diskuterar vi att skriva enhetsdrivrutiner på domänspecifika språk som hjälper till att abstrahera lågnivåkodningen och använda specifika kompilatorer för att generera koden.

Devil tillåter högnivådefinition av kommunikationen med enheten. Hårdvarukomponenterna uttrycks som I/O-portar och minnesmappade register. Dessa specifikationer konverteras sedan till en uppsättning C-makron som kan anropas från drivrutinskoden och därmed eliminerar felet som induceras av programmeraren när man skriver lågnivåfunktioner. NDL är en förbättring av Devil, som beskriver föraren i termer av dess operativa gränssnitt. Den använder definitionssyntaxen för Djävulens gränssnitt och inkluderar en uppsättning registerdefinitioner, protokoll för åtkomst till dessa register och en samling enhetsfunktioner. Enhetsfunktioner översätts sedan till en serie operationer på det gränssnittet. För generering av enhetsdrivrutiner måste man först skriva drivrutinsfunktionerna i dessa gränssnittsspecifikationsspråk och sedan använda en kompilator som genererar drivrutinskoden på låg nivå.

HAIL (Hardware Access Interface Language) är ett annat domänspecifikt enhetsdrivrutinspecifikationsspråk. Drivrututvecklaren måste skriva följande.

Registerkartabeskrivning, som beskriver olika enhetsregister och bitfält från enhetens datablad.
Adressutrymmesbeskrivning för åtkomst till bussen.
Instantiering av enheten i det specifika systemet.
Invariant specifikation, som begränsar åtkomst till enheten.

HAIL-kompilatorn tar dessa ingångar och översätter specifikationen till C-kod.

Hårdvara Software Co-design

I samdesign av hårdvaruprogramvara specificerar konstruktören strukturen och beteendet hos systemet med hjälp av finita tillståndsmaskiner som kommunicerar sinsemellan. Sedan görs en serie tester, simuleringar och formell verifiering på dessa tillståndsmaskiner innan man bestämmer vilka komponenter som går in i hårdvaran och vilka av dessa i mjukvaran. Hårdvaran görs vanligtvis i fältprogrammerbara grindmatriser (FPGA) eller applikationsspecifika integrerade kretsar (ASIC), medan mjukvarudelen översätts till programmeringsspråk på låg nivå. Detta tillvägagångssätt gäller mestadels i inbyggda system som definieras som en samling programmerbara delar som interagerar kontinuerligt med miljön genom sensorer. Befintliga tekniker är avsedda för att generera enkla mikrokontroller och deras drivrutiner.

Fristående drivrutinssyntes

I den fristående syntesen görs både enheten och systemmjukvaran separat. Enheten är modellerad med vilket som helst Hardware Description Language (HDL) och mjukvaruutvecklaren har inte tillgång till HDL-specifikationerna. Hårdvaruutvecklarna lägger fram enhetsgränssnittet i databladet för enheten. Från databladet extraherar drivrutinsutvecklaren register och minneslayout för enheten och beteendemodellen i form av finita tillståndsmaskiner. Detta uttrycks i de domänspecifika språken som beskrivs i avsnittet Gränssnittsspråk. Det sista steget innebär att generera koden från dessa specifikationer.

Verktyget Termite kräver tre specifikationer för att generera drivrutinen.

Enhetsspecifikation: Specifikationen för enhetsregister, minne och avbrottstjänster hämtad från enhetens datablad.
Enhetsklassspecifikation: Detta kan erhållas från relevant enhets I/O-protokollstandard. Till exempel, för Ethernet beskriver Ethernet LAN-standarden det vanliga beteendet för dessa styrenheter. Detta kodas vanligtvis som en uppsättning händelser som paketöverföring, slutförande av automatisk förhandling och länkstatusändring etc.
OS-specifikation: Detta beskriver OS-gränssnittet med drivrutinen. Mer specifikt den begäran som OS kan göra till föraren, ordningen på dessa förfrågningar och vad OS förväntar sig av föraren i utbyte mot dessa förfrågningar. Den definierar en tillståndsmaskin där varje övergång motsvarar en drivrutinsanrop från OS, återuppringningen som görs av föraren eller en protokollspecifik händelse.

Med dessa specifikationer kommer Termite att generera drivrutinsimplementeringen som översätter alla giltiga sekvenser av OS-begäranden till en sekvens av enhetskommandon. På grund av den formella specifikationen av gränssnitten kan Termite generera förarkoden som håller egenskaperna för säkerhet och livlighet .

En annan mycket intressant hackningsinsats har gjorts av RevNIC, som genererar en drivrutinstillståndsmaskin genom att omvända en befintlig drivrutin för att skapa interportabla och säkra drivrutiner för nya plattformar. För att bakåtkonstruera en drivrutin avlyssnar den maskinvaru-I/O-operationerna genom att exekvera drivrutinen med symboliska och konkreta exekveringar. Utsignalen från telefonavlyssningen matas till en synthesizer, som rekonstruerar en kontrollflödesgraf för den ursprungliga drivrutinen från dessa multipla spår tillsammans med mallen för motsvarande enhetsklass. Med hjälp av dessa metoder har forskarna porterat vissa Windows-drivrutiner för nätverksgränssnitt till andra Linux och inbyggda operativsystem.

Kritik

Även om många av de statiska analysverktygen används i stor utsträckning, har många av drivrutinsyntes- och verifieringsverktygen inte fått någon bred acceptans i praktiken. En av anledningarna är att drivrutiner tenderar att stödja flera enheter och drivrutinssyntesarbetet genererar vanligtvis en drivrutin per enhet som stöds, vilket potentiellt kan leda till ett stort antal drivrutiner. En annan anledning är att förare också bearbetar en del och tillståndsmaskinmodellen av förare kan inte avbilda bearbetning.

Slutsats

De olika verifierings- och syntesteknikerna som undersöks i denna artikel har sina egna fördelar och nackdelar. Till exempel har runtime-felisolering prestandaoverhead, medan den statiska analysen inte täcker alla klasser av fel. Den fullständiga automatiseringen av syntes av enhetsdrivrutiner är fortfarande i ett tidigt skede och har en lovande framtida forskningsriktning. Framsteg kommer att underlättas om de många språk som är tillgängliga idag för gränssnittsspecifikation så småningom kan konsolideras till ett enda format, som stöds universellt av enhetsleverantörer och operativsystemteam. Vinsten från en sådan standardiseringsansträngning kan vara realiseringen av helt automatiserad syntes av pålitliga drivrutiner i framtiden.

externa länkar