Ausgewählte Themen des Modellbasierten Sicherheits-Engineerings
Themen-Liste

JIF

Ähnlich wie MAKS kann man mit JIF den sicheren Informations-Fluss sicherstellen. JIF nutzt dazu ein typen-basiertes System, mit dem man den Code statisch prüfen kann.

Literatur:

Modular Assembly Kit for Security (MAKS)

Vertrauliche Daten sollen nicht aus einem System geleaked werden. Ein System dieses zu modellieren und zu analysieren bietet MAKS.

Literatur:

  • Diss Mantel (Kap. 2-3)

KIV - Ein (semi)-automatisches Beweissystem

Im Security-Bereich müssen immer wieder Aussagen bewiesen werden. Für die Anwendung is Laufenden System bieten sich Theoremprover an, diese Arbeit halbautomatisch zu übernehmen. In diesen Vortrag soll das System KIV als Beispiel vorgestellt werden.

Literatur:

A Domain-Specific Language for Computing on Encrypted Data

In Cloud Computing Umgebungen können Berechnung auf nicht vrtrauenswürdige Server ausgelagert werden. Mit homomorpher Verschlüsselung und sicheren Multiparty Computation stehen entsprechende kryptographische Primitive zur Verfügung, die eine vertrauenswürdige Berechnung leisten können. Entsprechende Software muss allerdings sorgfäaltig aufgebaut sein, um Vertrauenswürdigekeit zu garantieren. Alex Bain et al. schlagen eine auf Haskell basierende domain-specific language (DSL) für Cloud Computing vor. Ziel des Vortrags ist eine kurze Einführung in (e)DSLs und die Vorstellung der DSL für die Berechnung auf verschlüsselten Daten.

Literatur:

Homomorphic Encryption

Die Auslagerung von Prozessen und Berechnungen in Cloud Computing Umgebungen birgt insbesondere in Hinsicht auf Datenschutz und Compliance zahlreiche Risiken. Eine Möglichkeit diesen Risiken entgegenzuwirken ist die Verschlüsselung von Daten in der Cloud Computing Umgebung. Wählt man ein homomorphes Verschlüsselungsverfahren, so können in der Cloud trotz der Verschlüsselung noch hinreichend sinnvolle Berechnungen ausgeführt werden. Der Vortrag soll das Prinzip der homomorphen Verschlüsselung erklären und mindestens ein konkretes Verfahren wie bspw. Verfahren die auf dem „ring learning with errors“ (Ring LWE) Problems beruhen oder das original Verfahren von Gentry vorstellen und derzeitige Einsatzmöglichkeiten sowie Probleme beim Einsatz homomorpher Verschlüsselung aufzeigen.

Literatur:

Modell-getriebene Test-Generierung (DW)

Um die Erstellung von Tests für Systeme zu automatisieren, gibt es eine Reihe von modellbasierten Ansätzen, unter anderem MODEST.

Literatur:

Ontologien für Sicherheit und Compliance in Clouds

Die Verarbeitung vertraulicher Daten stellt Sicherheits- und Complianceanforderungen an die Cloud. Diese Anforderungen ans Cloud Computing sollen erläutert und bestehende Ontologien und Referenzmodelle diskutiert werden.

Literatur:

Artefakt-basierte Modellierung von Geschäftsprozessen

Geschäftsprozesse werden i.d.R. entweder Ereignis-basiert oder Artefakt-basiert modelliert. In diesem Vortrag soll eine Gegenüberstellung der beiden Ansätze erfolgen und eine mögliche Kombination beider diskutiert werden.

Literatur:

  • A. Nigam, N.S. Caswell; Business artifacts: an approach to operational specification, IBM Sys.J. 42(3), 2003

Compliance-Checking auf BPMN-Modellen

Die Abfragesprache BPMN-Q erlaubt eine einfache Prüfung von Compliance-Anforderungen oder anderen Kriterien auf BPMN-Modellen. Im Vortrag sollen BPMN-Q und die damit verbundenen Möglichkeiten vorgestellt werden.

Literatur:

Model Checking in der Praxis

Aufgrund der Komplexität ist der Einsatz von Model Checking in praktischen Systemen eingeschränkt. In diesem Vortrag soll zum Einen dargestellt werden, in welchen Bereichen Model Checking einsetzbar ist, zum Anderen werden hierfür geeignete Ansätze und Tools vorgestellt.

Literatur:

Grundlagen des expliziten Model Checkings

Model Checking bietet die Möglichkeit, für ein gegebenes System geforderte Eigenschaften formal nachzuweisen. Ziel des Vortrags ist die Darstellung des grundsätzlichen Vorgehens beim Model Checking, der möglichen Formalismen sowie der praktischen Grenzen der Anwendbarkeit.

Literatur z.B.:

Einführung ins Refinement Checking

Refinement Checking erlaubt den Vergleich verschiedener Spezifikationen in Bezug auf funktionale Äquivalenz. Der Vortrag stellt die Grundlagen des Verfahrens vor, sowie ggf. deren praktische Umsetzung, z.B. anhand des Refinement Checkers FDR2.

Literatur:

Modelling security goals in business processes

Geschäftsprozessmodelle (BPMN) werden in Unternehmen eingesetzt um die Abläufe, verwendete Dokumente und Informationsflüsse zu visualisieren. Dabei können dabei auch Sicherheitseigenschaften modelliert werden, welche später in einer konkreten Implementierung berücksichtigt werden können. Der Vortrag soll einen Überblick über die zur Verfügung stehenden Sicherheitserweiterungen geben und deren jeweiligen Fokus sowie die Stärken und Schwächen aufzeigen.

Literatur:

Modelling security goals in business processes

Service orientierte Architekturen sind ein Paradigma für die Orchestrierung von verteilten Diensten zu einem gemeinsamen Geschäftsprozess. Um die dabei zwangsläufig durchzuführenden Datenübertragungen zwischen den beteiligten Diensten vor unbefugtem Zugriff zu schützen, existieren Ansätze, die in diesem Vortrag behandelt werden sollen.

Modellierung von Sicherheitsanforderungen in einer SOA-Umgebung.

Literatur:

Model-based risk assessment with CORAS

Eine Sicherheitsrisikoanalyse liefert Antworten auf Sicherheitsfragen, wie „Wie sicher ist ein Internetbankkonto?“ oder „Wie gefährlich kann ein Fehler einer einzelnen Person für die Firma sein?“. CORAS ist eine Methode um Sicherheitsrisikoanalysen durchzuführen. Es verwendet UML Profile zur Analyse und Darstellung und stellt ein Tool für Dokumentation, Wartung und Analysereport zur Verfügung.

Literatur:

System Modelling and Simulation with Core Gnosis/Demos2k

Core Gnosis basiert auf Demos2k und ist eine ausführbare Modellierungssprache. Mit Hilfe dessen komplexe Systeme mit stochastischen Eingängen und ortsbezogene Ressourcen modelliert und simuliert werden können. Basierend auf SCCS und (L)SCRP existiert ein sematischer Calculus zur mathematischen Darstellung der Sprache.

Literatur:

Kontakt

Zum Profil von Prof. Dr. Jan Jürjens