MAIS

Proof-Carrying-Code (Seminar)

Form: Blockseminar, 16. Mai 2008

Anmeldung: Anmeldungen nimmt Elisabeth Kraft entgegen. Falls Sie sie nicht antreffen sollten, wenden Sie sich bitte an Alexander Lux im Büro nebenan (S2-02-E317).

Literatur: Wird in der Vorbesprechung bekanntgegeben

Vorbesprechung: Donnerstag, 3. April 2008, 13:30 in S202/E202.

Kontakt: Bei Fragen bitte an Alexander Lux wenden.

Thema:

Bei einer gegebenen Software, die man zum Beispiel von einer Webseite heruntergeladen hat, lässt sich nicht ohne weiteres sagen, ob sie die Eigenschaften erfüllt, die der Hersteller für die Software verspricht.

Liegt eine formale Spezifikation dieser Eigenschaften vor, so kann mit mathematischen Methoden bewiesen werden, ob die Software diese Eigenschaften erfüllt. Solch einen Beweis zu entwickeln ist nicht einfach und benötigt normalerweise einen Spezialisten und viele Rechnerressourcen.

Die Idee des Proof-Carrying-Code (PCC) ist, die Software mit einem Beweis (semantisches Zertifikat) zu bündeln, anhand dessen gewisse Eigenschaften der Software überprüft werden können. Die Erstellung dieser Beweise sind eher schwierig, die Überprüfung der Software anhand des Beweises kann hingegen automatisch erfolgen.

In dem Seminar werden Artikel zu Anwendungsgebieten und Techniken des PCC-Prinzips behandelt, zum Beispiel zum Nachweis von Typsicherheit für Java Bytecode (ein Mechanismus aus der aktuellen Java Virtual Machine) oder zum Beispiel PCC durch Sicherheitsautomaten.

Das Seminar kann gemeinsam mit dem "PCC Praktikum" im gleichen Semester besucht werden. Es ist aber auch möglich und ebenso sinnvoll, am Seminar teilzunehmen, ohne das Praktikum zu belegen.