Formale Spezifikation, Verifikation und Umsetzung von rollenbasierten Sicherheitsrichtlinien

Die zunehmende elektronische Speicherung von sensiblen Daten and Die Abbildung von Geschäftsprozessen auit - system machine in vielen Organisationen systematisches berechtigunsmanagement erforderlich。在德国，verinen angemessenen Schutz von sensiblen Daten zu gewährleisten，我们的组织sweit ververindliche Sicherheitsrichtlinien fr die zugriffskcontrolle festzulegen。Allerdings werden disese richtlinen gerade in größeren Organisationen schnell unbersichtlich, so dass zu inconsistent and unerlaubten Zugriffen kommen kann。在ForRBAC中，有System entwickelt werden， mitdem Sicherheitsrichtlinien speziziert, analyert and umgesetzt werden können。Schwerpunktmäßig风尘尘尘尘，尘尘尘，尘尘尘，尘尘尘，尘尘尘，尘尘尘。在dersten Phase wind - as System auf based iner Temporallogik entwickelt中，每个dynamische Sicherheitsrichtlinien behandeln zu können， die z.B. im context von Workflows autrene。我的天，我的天，我的天。Hierdurch können Beweise <e:1> berdie sicherheitsrichtlinen maschinell gefhrt werden。Damit das System auch in der Praxis genutzt werden kann, wird eingabesprachhe fr Sicherheitsverantwortliche entwickelt, die in die Temporallogik bersetzt wind。在此阶段中，风力发电机组采用了自定义组件形式化验证器，风力发电机组采用了实现组件形式化验证器。

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.