Spezifikation und Verifikation von Informationsflüssen (InfoZert B)

点击翻译按钮获取中文摘要

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. Ziele dieses Projekts sind zunächst die Entwicklung von Spezifikationsnotationen, um solche Regeln ( Informationsflusspolitiken ) exakt zu formulieren, sowie die Bereitstellung von Algorithmen zur Verifikation einer solchen Politik bezüglich einer Systembeschreibung in bestehenden Beschreibungsformalismen wie UML und interacting state machines (ISMs). Darüber hinaus soll die Realisierung sicherer Systeme durch die Definition von Verfeinerungsbegriffen unterstützt werden. Diese setzen Implementierungen so mit Systembeschreibungen in Beziehung, dass sich die Einhaltung von Informationsflusspolitiken von der Beschreibungsebene auf die Implementierung überträgt. Vor allem das zuletzt genannte Themengebiet wird gemeinsam mit dem Schwesterprojekt ( InfoZert A ) bearbeitet, welches die Entwicklung von proof-carrying code (FCC) Technologie anstrebt, mittels derer Informationsfiusseigenschaften von Systemkomponenten in einer herstellerunabhängigen und automatisch überprüfbaren Form nachgewiesen werden können. Teilaspekte des Forschungsvorhabens werden von den Antragstellern in Kooperation mit den Forschungsabteilungen der Siemens AG, München, sowie der SAP AG, Sophia-Antipolis, Frankreich, durchgeführt.