Spezifikation und Verifikation von Informationsflüssen (InfoZert B)
Final Report Abstract
Das Projekt beschäftigt sich mit der Konstruktion sicherer Softwaresysteme, wobei das zugrundeliegende Verständnis von Sicherheit durch den Begriff der Informationsflusssicherheit gebildet wird. Ziel ist die Entwicklung einer Verifikations- und Zertifikationsarchitektur gemäß des Proof-Carrying-Code-Paradigmas. Dies bedeutet, dass der Hersteller von Software zusätzlich zum Code einen Beweis vorlegen muss, der in automatisch verifizierbarer Form belegt, dass der Code eine vom Konsumenten spezifizierte (in unserem Fall: Sicherheits-) Eigenschaft erfüllt. Konkretes Ziel des Projekts ist die Entwicklung von Typsystemen und anderen Verifikationskalkülen für die Eigenschaft Nichtinterferenz, welche fordert, dass vom Benutzer als geheim eingestufte Daten keinen Einfluss auf die Resultate der durch das übertragene Programm durchgeführten Berechnung haben dürfen. Neben einer prototypischen Implementierung eines Zertifikatgenerators und eines Zertifikatüberprüfers soll auch ein Spezifikationsformalismus entwickelt werden, mit dessen Hilfe Code-Konsument oder Code-Produzent Nichtinterferenzverhalten abstrakt beschreiben können. Teile der Verifikationsinfrastruktur werden exemplarisch in dem Theorembeweiser Isabelle/HOL implementiert, so dass die Gültigkeit der Zertifikate formal auf einer operationellen Semantik der ausführenden Maschine abgestützt ist.
