Bevisbärande kod

Proof-carrying code ( PCC ) är en mjukvarumekanism som gör att ett värdsystem kan verifiera egenskaper om en applikation via ett formellt bevis som medföljer applikationens körbara kod. Värdsystemet kan snabbt verifiera bevisets giltighet, och det kan jämföra slutsatserna av beviset med sin egen säkerhetspolicy för att avgöra om applikationen är säker att köra. Detta kan vara särskilt användbart för att säkerställa minnessäkerhet (dvs. förhindra problem som buffertspill) .

Bevisbärande kod beskrevs ursprungligen 1996 av George Necula och Peter Lee .

Exempel på paketfilter

Den ursprungliga publikationen om korrekturbärande kod 1996 använde paketfilter som ett exempel: en applikation i användarläge överlämnar en funktion skriven i maskinkod till kärnan som avgör om en applikation är intresserad av att bearbeta ett visst nätverkspaket eller inte. Eftersom paketfiltret körs i kärnläge kan det äventyra systemets integritet om det innehåller skadlig kod som skriver till kärnans datastrukturer. Traditionella tillvägagångssätt för detta problem inkluderar att tolka ett domänspecifikt språk för paketfiltrering, infoga kontroller på varje minnesåtkomst ( programvarufelsisolering ) och skriva filtret på ett högnivåspråk som kompileras av kärnan innan det körs. Dessa tillvägagångssätt har prestandanackdelar för kod som ofta körs som ett paketfilter, med undantag för kompileringsmetoden i kärnan, som bara kompilerar koden när den laddas, inte varje gång den exekveras.

Med proof-bärande kod publicerar kärnan en säkerhetspolicy som anger egenskaper som alla paketfilter måste följa: kommer till exempel inte att komma åt minne utanför paketet och dess skrapminnesområde. Ett teorembevis används för att visa att maskinkoden uppfyller denna policy. Stegen i detta bevis registreras och bifogas till maskinkoden som ges till kärnprogramladdaren. Programladdaren kan sedan snabbt validera beviset, så att den därefter kan köra maskinkoden utan ytterligare kontroller. Om en illvillig part ändrar antingen maskinkoden eller beviset, är den resulterande bevisbärande koden antingen ogiltig eller ofarlig (uppfyller fortfarande säkerhetspolicyn).

Se även

• Maskinskrivet assemblerspråk
• Program härledning
• Formell verifiering
• Berkeley paketfilter

• George C. Necula och Peter Lee. Bevisbärande kod . Teknisk rapport CMU-CS-96-165, november 1996. (62 sidor)
•   George C. Necula och Peter Lee. Säkra, otillförlitliga agenter som använder bevisbärande kod . Mobile Agents and Security, Giovanni Vigna (Ed.), Lecture Notes in Computer Science, Vol. 1419, Springer-Verlag, Berlin, ISBN 3-540-64792-9 , 1998.
• George C. Necula. Sammanställning med bevis . Doktorsavhandling, School of Computer Science, Carnegie Mellon Univ., sept. 1998.