Formale Spezifikation, Verifikation und Umsetzung von rollenbasierten Sicherheitsrichtlinien

• Antragsteller: Privatdozent Dr. Karsten Sohr
• Fachliche Zuordnung: Softwaretechnik und Programmiersprachen
• Förderung: Förderung von 2006 bis 2009
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 25616799

Die zunehmende elektronische Speicherung von sensiblen Daten und die Abbildung von Geschäftsprozessen auf IT-Systeme machen in vielen Organisationen ein systematisches Berechtigungsmanagement erforderlich. Um einen angemessenen Schutz von sensiblen Daten zu gewährleisten, sind organisationsweit verbindliche Sicherheitsrichtlinien für die Zugriffskontrolle festzulegen. Allerdings werden diese Richtlinien gerade in größeren Organisationen schnell unübersichtlich, so dass es zu Inkonsistenzen und unerlaubten Zugriffen kommen kann. In ForRBAC soll ein System entwickelt werden, mit dem Sicherheitsrichtlinien spezifiziert, analysiert und umgesetzt werden können. Schwerpunktmäßig wird die rollenbasierte Zugriffskontrolle betrachtet, weil diese in vielen Organisationen weit verbreitet ist. In der ersten Phase wird das System auf Basis einer Temporallogik entwickelt, um auch dynamische Sicherheitsrichtlinien behandeln zu können, die z.B. im Kontext von Workflows auftreten. Die Temporallogik wird dann in den Theorembeweiser Isabelle eingebettet. Hierdurch können Beweise über die Sicherheitsrichtlinien maschinell geführt werden. Damit das System auch in der Praxis genutzt werden kann, wird eine Eingabesprache für Sicherheitsverantwortliche entwickelt, die in die Temporallogik übersetzt wird. In der zweiten Phase wird eine rollenbasierte Autorisierungskomponente formal spezifiziert, und es wird eine Implementierung dieser Komponente zumindest teilweise formal verifiziert.

• DFG-Verfahren: Sachbeihilfen
• Beteiligte Person: Professor Dr. Till Mossakowski