Proof-Carrying Code (Seminar)

 

Organisator: Prof. Dr. Heiko Mantel
Form: Blockseminar
Registrierung: im Sekretariat des Fachgebiets bei Frau Kraft (Sprechzeiten Frau Kraft)
Literatur: Wird in der Vorbesprechung bekanntgegeben
Vorbesprechung: 15. April 2010, 16:30 Uhr, S2/02 E302
Kontakt: Bei Fragen bitte an Dieter Schuster wenden.

Das Seminar gehört zu Foundations of Computing (Modulhandbucheintrag).

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.

Folgen Sie dem Link zu den Internen Webseiten.

A A A | Print | Imprint | Sitemap | Contact
zum Seitenanfang