Proof-Carrying Code
Z Wikipedii
Proof-Carrying Code to jedna z technik matematycznego dowodzenia poprawności programu.
Metoda polega na dołączeniu do skompilowanego programu dowodu, że spełnia on pewne założenia. Dzięki temu weryfikacji może dokonać użytkownik i nie musi w najmniejszym stopniu ufać twórcy kodu. Taka metoda weryfikacji wymaga operowania na niższym poziomie. Z tych powodów metoda ta jest używana głównie dla uzyskania pełnego bezpieczeństwa przy wymaganej dużej wydajności.
System korzystający z proof-carrying code składa się z:
- Trusted Computing Base, czyli części systemu, której ufamy. W miarę możliwości powinna zawierać jak najmniej. Zwykle w skład wchodzą:
- Fizyczny procesor bądź też maszyna wirtualna
- 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, czyli aksjomatu mówiącego, że program, który spełnia pewne warunki, jest bezpieczny
- Kodu, który musi spełniać security policy.
[edytuj] Gwarancje bezpieczeństwa
System taki jest absolutnie bezpieczny, o ile błędów nie zawiera Trusted Computing Base, chociaż może wykonywać obcy kod nawet w kernelspace ! (jednym z testowych zastosowań są operujące w kernelspace filtry pakietów IP).
Gwarancje bezpieczeństwa udzielane przez PCC są silniejsze niż te udzielane przez inne techniki, takie jak audyty bezpieczeństwa, podpisy elektroniczne, separacja przywilejów, sandboxy, dowody przeprowadzane przez kompilator itd.
Jak wiadomo, audyt może nie wykryć pewnych problemów, podpis gwarantuje co najwyżej, że podpisujący wierzy, że kod jest bezpieczny, a ilość kodu któremu musi się ufać w przypadku innych technik jest znacznie większa niż w przypadku PCC.
Z tych powodów PCC jest bardzo obiecującą techniką, jednak badania nad nią są we wczesnych stadiach i nie jest pewne, w jakim stopniu może się ona skalować na większe systemy.
