Proof-Carrying Code

Proof-Carrying Code(PCC) ist ein 1996 vonGeorge NeculaundPeter Leeentwickelter, effizienterAlgorithmusfürComputer,mit dessen Hilfe die Eigenschaften vonAnwendungssoftwareund insbesondere die Einhaltung vonSicherheitsrichtlinienüberprüft und verifiziert werden können.

Der automatische Algorithmus benutzt einAxiomensystem,um denProgrammcodebegleitendeMetadatenzu analysieren. Dabei kann geschlussfolgert und gewährleistet werden, dass bestimmte sicherheitsrelevante Kriterien eingehalten werden. ZurLaufzeitmüssen dann keine entsprechenden zusätzlichen Maßnahmen ergriffen werden, wie zum Beispiel dieAusnahmebehandlungbei kritischem Verhalten der Software. Proof-Carrying Code ist ferner besonders nützlich, umSicherheitslücken,wie zum BeispielPufferüberläufeoderMehrdeutigkeiten(beispielsweiseTypverletzung,ÜberladenoderPolymorphie), zu verhindern, die häufig durch die Benutzung von unzureichendenProgrammiersprachenbedingt sind.

Mit dem Proof-Carrying Code kann auf einemClientbei derInstallationund der Ausführung vonComputerprogrammendie Zuverlässigkeit und Vertrauenswürdigkeit einer Programmquelle in einemRechnernetzüberprüft werden. Dabei werden Metadaten vomHost,dem sogenanntenProgrammcodeproduzentenabgerufen, mit deren Hilfe die Überprüfung auf dem Client, dem sogenanntenProgrammcodeverbraucher,stattfinden kann.

Weblinks

• 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