Proof-Carrying Code

Z Wikipedii

Proof-Carrying Code to jedna z technik matematycznego dowodzenia poprawności programu. Koncepcję tę po raz pierwszy w takim sformułowaniu wyraził w 1998 roku George Ciprian Necula.

PCC polega na dołączeniu do skompilowanego programu dowodu spełnialności tzw. warunku weryfikacyjnego tego programu. Weryfikacja tego dowodu może odbyć się po stronie klienta i jej przebieg nie zależy od źródła pochodzenia kodu.

System korzystający z proof-carrying code składa się z:

• Trusted Computing Base (zaufana baza obliczeniowa), czyli część infrastruktury, której klient ufa. W miarę możliwości powinna zawierać jak najmniej. Zwykle w skład wchodzą:
  • Fizyczny procesor bądź też maszyna wirtualna
  • Generator warunków weryfikacyjnych (Verification Condition Generator)
  • Weryfikator dowodów (w niektórych systemach nie wchodzi on w skład TCB)
  • System operacyjny, biblioteka standardowa, inny wykorzystywany sprzęt itd.
• Security Policy (polisa bezpieczeństwa), czyli formalny system logiczny złożony z aksjomatów, reguł oraz twierdzenia o bezpieczeństwie mówiącego, że każdy program, którego warunek weryfikacyjny (formuła logiczna powstała przez przeskanowanie kodu binarnego programu, zbudowana według algorytmu, do którego odwoływać się musi twierdzenie) jest spełnialny można uznać za bezpieczny według tej polisy. Klient infrastruktury PCC musi albo przestudiować dowód twierdzenia o bezpieczeństwie albo mu zaufać - każdy błąd w dowodzie jest potencjalną luką w bezpieczeństwie PCC.

[edytuj] Gwarancje bezpieczeństwa

Podstawowe trudności w przemysłowym sformułowaniu PCC polegają na tym, że formalizacje polis bezpieczeństwa są zwykle bardzo trudne lub dyskusyjne. Dość dobrze wyraża się polisy gwarantujące bezpieczeństwo typów czy poprawne kontraktowanie ale wiele innych ciekawych formalizmów (m.in. Non-Interference) ma charakter bardziej teoretyczny, możliwy do zaaplikowania do algebraicznych modeli procesów, a nie ich konkretnych instancji wyrażonych w językach niskiego poziomu.

Ponadto definicja algorytmu generatora warunków weryfikacyjnych i dowód twierdzenia o bezpieczeństwie musi być powtórzony dla każdej pary polisa bezpieczeństwa - kod maszynowy. Dowody takie są trudne, żmudne i niemożliwe do automatycznej weryfikacji. To mocno ogranicza badania nad tą techniką - na przykład formalizacja PCC dla jakiejkolwiek polisy bezpieczeństwa dla maszyny wirtualnej Javy musiałaby być powtórzona niemal od zera w dla środowiska uruchomieniowego .NET, assemblera x86 i każdego innego języka, w którym wyrażony mógłby być analizowany kod.

Jednym z testowych zastosowań są operujące w kernelspace filtry pakietów IP dla prostej polisy bezpieczeństwa sprawdzającej poprawność typowania się kodu.

Gwarancje bezpieczeństwa udzielane przez PCC są silniejsze niż te udzielane przez inne popularne techniki, takie jak audyty bezpieczeństwa, podpisy elektroniczne, separacja przywilejów, ponieważ opierają się na poprawności dowodu twierdzenia o bezpieczeństwie wskazanego wariantu PCC. W przypadku innych technik gwarancje mają charakter uznaniowy - na przykład podpis cyfrowy gwarantuje wyłącznie potwierdzenie tożsamości producenta kodu, co wcale nie wyklucza że tenże producent, celowo lub nieumyślnie, opublikował kod błędny lub wręcz niebezpieczny.

Z tych powodów PCC jest bardzo obiecującą techniką i badania nad nią trwają.