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.

• George C. Necula und Peter Lee: Safe, Untrusted Agents Using Proof-Carrying Code, Mobile Agents and Security, Giovanni Vigna (Herausgeber), Lecture Notes in Computer Science, Volume 1419, Springer-Verlag, Berlin, ISBN 3-540-64792-9, 1998
• George C. Necula: Compiling with Proofs (PDF; 1,6 MB). PhD thesis, School of Computer Science, Carnegie Mellon University, September 1998
• Proof-Carrying Code im Projekt MOBIUS