| dbo:abstract
|
- Proof-Carrying Code (PCC) ist ein 1996 von und entwickelter, effizienter Algorithmus für Computer, mit dessen Hilfe die Eigenschaften von Anwendungssoftware und insbesondere die Einhaltung von Sicherheitsrichtlinien überprüft und verifiziert werden können. Der automatische Algorithmus benutzt ein Axiomensystem, um den Programmcode begleitende Metadaten zu analysieren. Dabei kann geschlussfolgert und gewährleistet werden, dass bestimmte sicherheitsrelevante Kriterien eingehalten werden. Zur Laufzeit müssen dann keine entsprechenden zusätzlichen Maßnahmen ergriffen werden, wie zum Beispiel die Ausnahmebehandlung bei kritischem Verhalten der Software. Proof-Carrying Code ist ferner besonders nützlich, um Sicherheitslücken, wie zum Beispiel Pufferüberläufe oder Mehrdeutigkeiten (beispielsweise Typverletzung, Überladen oder Polymorphie), zu verhindern, die häufig durch die Benutzung von unzureichenden Programmiersprachen bedingt sind. Mit dem Proof-Carrying Code kann auf einem Client bei der Installation und der Ausführung von Computerprogrammen die Zuverlässigkeit und Vertrauenswürdigkeit einer Programmquelle in einem Rechnernetz überprüft werden. Dabei werden Metadaten vom Host, dem sogenannten Programmcodeproduzenten abgerufen, mit deren Hilfe die Überprüfung auf dem Client, dem sogenannten Programmcodeverbraucher, stattfinden kann. (de)
- Proof-carrying code (PCC) is a software mechanism that allows a host system to verify properties about an application via a formal proof that accompanies the application's executable code. The host system can quickly verify the validity of the proof, and it can compare the conclusions of the proof to its own security policy to determine whether the application is safe to execute. This can be particularly useful in ensuring memory safety (i.e. preventing issues like buffer overflows). Proof-carrying code was originally described in 1996 by George Necula and Peter Lee. (en)
- Proof-Carrying Code – jedna z technik matematycznego dowodzenia poprawności programu komputerowego. 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, 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. (pl)
|
