Proof-Carrying Code

Proof-Carrying Code (PCC) ist ein 1996 von George Necula und Peter Lee 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.