Verifikation und Zertifikation von Informationsflüssen (InfoZert A)

• Applicant: Lennart Beringer, Ph.D.
• Subject Area: Software Engineering and Programming Languages
• Term: from 2006 to 2009
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 15949872

Das Projekt beschäftigt sich mit der Konstruktion sicherer Systeme, wobei das zugrundeliegende Verständnis von Sicherheit durch den Begriff der Informationsflusssicherheit gebildet wird: einem externen Beobachter soll es unmöglich sein, ohne Einverständnis des Systembetreibers Rückschlüsse auf den internen Systemzustand oder auf ausgeführte Aktionen zu ziehen. Dabei legt der Betreiber mittels formaler Regeln selbst fest, welche Systemkomponenten und Aktionen als geheim gelten sollen. Ziel des Vorhabens ist die Entwicklung eines Zertifizierungsmechanismus für Informationsflusssicherheit gemäß dem ¿proof-carrying code¿ (PCC) Konzept: ein Hersteller von Softwarekomponenten soll in der Lage sein, diese mit formalen Beweisobjekten zu versehen, welche die Informationsflusssicherheit der Software belegen und vom Empfänger vollautomatisch daraufhin überprüft werden können, ob sie die Einhaltung einer lokal definierten Sicherheitspolitik implizieren. Da diese Konsistenzeigenschaft lediglich das Programm, den Beweis und die Sicherheitspolitik betrifft, ergibt sich ein Verifikationsbegriff, der unabhängig ist von der Autorschaft durch den Hersteller und von der Zuverlässigkeit des Übertragungsmediums. Das Verfahren kann somit unabhängig von kryptographischen Methoden oder digitalen Unterschriften angewandt werden. Das Projekt ergänzt existierende und geplante Forschungsvorhaben in den Bereichen Softwareerstellung und Programmverifikation der aufnehmenden Institution und wird teilweise in Kooperation mit den Forschungsabteilungen der Siemens AG, München, sowie der SAP AG, Sophia-Antipolis, Frankreich, durchgeführt.

• DFG Programme: Research Grants