Modellbasierte Entwicklung sicherer Software Flashcards
Was ist die Motivation für IT-Sicherheit?
- Wirtschaft, Unternehmen und Gesellschaft hängen zunehmend ab von Computernetzwerken für
- Kommunikation, Finanzen, Energieversorgung, Transport…
- Angriffe können großen finanziellen Schaden verursachen.
- Vernetzte Systeme anonym und aus Entfernung angreifbar.
- Computersysteme müssen sicher sein.
Sicherheit
Definition
Schutz von Daten/Systemen gegen mutwillige Angriffe. Inhärent schwierig (zielorientierter Angreifer).
Was sind Ursachen von Sicherheitslücken?
- Korrektes Entwerfen sicherer Systeme schwierig.
- Selbst Experten irren sich
- Designern fehlt es an Erfahrung in Sicherheit.
- Sicherheit im Nachhinein.
- Angriffs-Informationen verbreiten sich schnell.
- Keine Rückmeldung über Sicherheit aus Kundensicht.
- Blindes Vertrauen in Mechanismen
- Sicherheitsvorkehrungen können umgangen werden, ohne diese zu brechen
*
- Sicherheitsvorkehrungen können umgangen werden, ohne diese zu brechen
Was ist das Ziel Modellbasierter Entwicklung sicherer Systeme ?
Sicherheit erhöhen, bei begrenzter Investition an Zeit und Kosten.
Modellbasierte Entwicklung sicherer Systeme
Lösungsansatz
- Aus Artefakten in industrieller Entwicklung und Betrieb sicherheitskritischer Software: Modelle extrahieren (UML, Quellcode, Konfigurationen).
- Werkzeugunterstützung für theoretisch fundierte, effiziente (automatische) Sicherheitsanalyse.
- Modell-basierte Entwicklung sicherer Systeme.
Modellbasierte Entwicklung sicherer Systeme
Einsatzfelder
- Systementwurf:
- z.B. Architekturbewertung, Plattformenwahl, Altsystemeinbindung.
- Autom. Sicherheits- und Risikoanalyse modellierter GP und Softwarearchitekturen unter Einbezugnahme des Systemkontexts.
- Implementierung:
- Quellcodeanalyse, Testfolgengenerierung.
- Laufender Betrieb:
- Konfigurationsmanagement, Überprüfung von Berechtigungen, Einrichtungen von Firewalls…
- Autom. Checks von Systemkonfigurationen (z.B. SAP Berechtigungen, …).
- Sichere GP/WF: Berücksichtigung von Sicherheit ab Geschäftsprozessentwurf.
- Einsatz in Sicherheitsaudits: Erhöht Vertrauen in Korrektheit und Vollständigkeit.
Modellbasierte Sicherheitsanalyse von GP und Softwarearchitekturen mit Unified Modeling Language (UML)
Warum UML?
- De-facto Standard in industrieller Modellierung. Große Anzahl von Entwicklern in UML ausgebildet
- Einfache, intuitive Notation, relativ genau definiert.
- Weitgehende Werkzeugunterstützung (auch für Code-Generierung, Analyse, Reverse Engineering, Simulation, Transformation).
Was ist UMLsec?
- Erweiterung für Entwicklung sicherer Systeme:
- Auswertung von UML-Spezifikationen für Sicherheitsanalyse während Entwicklung.
- Beinhaltet etablierte Sicherheits-Regeln als Checkliste.
- Nicht auf sichere Systeme spezialisierte Entwicklern zur Verfügung gestellt.
- Berücksichtigt Sicherheitsanforderungen von Beginn der System-Entwicklung und im -Kontext.
- Sicherer Entwurf durch Modellanalyse.
- Sichere Implementierung durch modellbasierte Testgenerierung.
- Macht Zertifizierung kostengünstiger.
UMLsec
Umsetzung
- Wiederkehrende Sicherheitsanforderungen, Angriffs-Szenarien, und Sicherheits-Konzepte als Stereotypen und Tagged Values angeboten.
- [Stereotypen: Markierungen an UML-Modellelementen, z.B. «secrecy»
- Tagged Values: Annotationen der Form (tag=value), mit denen weitere Informationen übergeben werden.
- Verwenden Constraints, um Spezifikationen unter Verwendung automatischer Werkzeuge zu verifizieren und mögliche Schwächen anzuzeigen.
- [Stereotypen können mit vordefinierten Constraints verbunden werden.]
- Garantiert, dass UML Spezifikation gewünschtes Niveau der Sicherheitsanforderungen liefert.
- Verbindung zum Code über Round-Trip.
Sicherheitsanforderungen
- Vertraulichkeit
- Integrität
- Verfügbarkeit
- Authentizität
- Nichtabstreitbarkeit
- Anonymität
Was ist Link Encryption?
- Nur direkte Knotenverbindungen verschlüsselt.
- Einfache Konstruktion.
- Unterstützt durch Controller-Hardware, transparent für Software.
- Daten in Netzwerkknoten als Plaintext.
Was ist End to End Encryption
- Daten durchgehend verschlüsselt.
- Komplexer zu implementieren.
- Intransparent für Software, separate Behandlung von Adressen und Daten
Vorteile von Metamodellierung
- Vorteile im Allgemeinen:
- • Präzise Definition von Modellierungsnotation
- Vorteile von MOF:
- Wohlverstandene Notation für Definition der Modellierungsnotation (UML-Klassendiagramme)
- Weitgehende Werkzeugunterstützung (Modelltransformation, Codegenerierung etc)
Nachteile von Metamodellierung
- Einschränkungen im Allgemeinen:
- Erstellung / Anpassung Metamodell: Benötigt Aufwand und Expertise.
- Nachteile von MOF:
- Dieselbe Notation (Klassendiagramme) auf verschiedenen Ebenen evt. verwirrend.
- Logisch zirkulär (definiere Klassendiagramme mit Klassendiagrammen).
UML-Profil
Tagged Values
- Werte beschreiben Eigenschaften eines Stereotypen (fachliches Konzept).
- Tagged Values: Name-Wert Paare. Einsatz von Tagged Values im Modell:
- Kommentarfeld, das mit Element verbunden ist oder
- Geschweifte Klammern {Name = Wert} direkt in Element geschrieben.
UML Profil
Stereotypen
Definition von Stereotypen:
Definition neuer Stereotypen gemäß Metamodell:
(NB: Der Pfeil ist eine Spezialisierung.)
Was deckt UMLsec ab?
- Sicherheitsanforderungen: «secrecy»,…
- Bedrohungsszenarien: Vewende Threatsadv(ster).
- Sicherheitskonzepte: Zum Beispiel «smartcard».
- Sicherheitsmechanismen: Z.B. «guarded access».
- Grundlegende Sicherheit: eingebaute Verschlüsselung
- Physikalische Sicherheit: Im Verteilungsdiagramm.
- Sicherheitsmanagement: Im Aktivitätsdiagramm.
- Technologie spezifisch: Java, CORBA Sicherheit.
UMLsec
Unterstützte Modelle
- Aktivitätsdiagramm: Sicherer Kontrollfluss, Koordination
- Klassendiagramm: Austausch von Daten; hält Sicherheitslevel bereit
- Sequenzdiagramm: Sicherheitskritische Interaktion
- Zustandsdiagramm: Sicherheit innerhalb eines Objekts
- Verteilungsdiagramm: Physikalische Sicherheitsanforderungen
- Package: Ganzheitliche Betrachtung der Sicherheit
UMLsec
Definition von Stereotypen und Tags
- Constraints nutzen sicherheitsbewusste Interpretation von UML Diagrammen.
- «fair exchange», «provable», «secure links», «data security»:
- Parametrisiert über Gegnerart bzgl. Anhalten der Sicherheitsbedingungen.
- {adversary}: Werte in Form von (T;C).
- T: Gegnerart, z.B. T = default für Gegner später definiert, welches selbst definiert werden könnte.
- Falls ausgelassen T = default.
- C: Logische Bedingung auf Vorkenntnisse KpA des Gegners.
- Falls ausgelassen, C sichert das die in {secrecy} Tag von «critical» einbezogene Werte nicht als Teilausdruck in KpA erscheinen.
- T: Gegnerart, z.B. T = default für Gegner später definiert, welches selbst definiert werden könnte.
UMLsec
Sicherheitsanforderung: Fair Exchange
Definition
- Elektronische Handelsware, Anforderung der fair exchange setzt voraus, dass der Handel so durchgeführt wird, sodass beteiligte Parteien vom Betrug verhindert werden.
- Wenn z.B. der Käufer eine Anzahlung machen muss, sollte der Käufer in der Lage sein die Zahlung zu beweisen und das Geld zurückzufordern, falls die Ware danach nicht geliefert wurde.
UMLsec
Fair-Exchange im Use-Case Diagramm
- Ausführung der Transaktionen: Beide Parteien vom Betrug verhindern.
- Anwendbar in Teilsystemen durch ein Anwendungsfalldiagramm.
- Kann durch anderes Teilsystem verfeinert werden, falls es auch mit stereotypiert ist.
- Nur informelle Bedeutung, im Gegensatz zu unteren Stereotypen.
- Zeigt, wie die Sicherheitsanforderungen (wie Stereotypen) auch in anderen Arten von Diagrammen wie folgende in Anwendungsfalldiagrammen passend enthalten sein können.
UMLsec
Fair Exchange
Aktivitätsdiagramm
- Bedingung: Wenn im Aktivitätsdiagramm ein {start} Punkt erreicht wurde, wird immer ein {stop} Punkt erreicht.
- assoziierte Tags
- {start}, {stop}, {adversary}.
- {start}, {stop} nehmen Paare (good; state) als Werte,
- good ist der Name einer Ware, der verkauft werden soll, kann entfallen
- State: Name eines States.
- {adversary} Gegnerart relativ zu der die Sicherheitsanforderung halten soll.
UMLsec
Fair Exchange
Formal
- Formal für ein gegebenes Subsystem S:
- S erfüllt die Bedingung von «fair exchange» für einen Angreifertyp A wenn für jedes Gut, das verkauft wurde, folgende Bedingung eingehalten wird:
- Für jede Ausführung e von [[S]]A existiert ein n ∈ N ,sodass für jede Sequenz I1,……..,In einer Eingabe von Multimengen eine Ausführung e’ existiert, welche eine Erweiterung von e ist und dann die Eingaben von I1,……..,In, hinsichtlich des relevanten Guts, so verarbeitet, dass mindestens so viele {stop} Zustände in e’ sind, wie {start} Zustände in e.
UMLsec
«provable»
- Ein Subsystem S kann mit «provable» markiert werden.
- Tags: {action},{cert} und {adversary}.
- {cert} enthält einen Ausdruck d.h. einen Nachweis, dass die Aktion in dem Zustand in {action} ausgeführt wurde.
- {adversary} spezifiziert einen Angreifertyp, welchen die Sicherheitsanforderungen standhalten sollten.
- S gibt womöglich einen Ausdruck E ∈ Exp in {cert} aus, aber nur dann wenn der Zustand in {action} erreicht ist und er in Anwesenheit eines in {adversary} spezifizierten Angreifers vom Typ A ausgeführt worden ist.
- Tags: {action},{cert} und {adversary}.
Das Zertifikat in {cert} ist eindeutig für jede Subsystem-Instanz.
UMLsec
Rollenbasierte Zugriffkontrolle
«rbac»
- Verwendbar auf Subsystemen, die Aktivitätsdiagramme enthalten.
- Erzwingt rollenbasierte Zugriffskontrolle im durch das Aktivitätsdiagramm spezifizierten Geschäftsprozess.
- Tags: {protected}, {role}, und {right}.
- {protected} enthält Zustände im Aktivitätsdiagramm, bei denen der Zugriff kontrolliert werden soll.
- {role} Liste von Paaren (actor; role)
- actor ist ein Akteur im Aktivitätsdiagramm,
- role ist eine Rolle.
- {right} Liste von Paaren (role; right) role ist eine Rolle.
- right repräsentiert das Zugriffsrecht zu einer geschützten Ressource.
- Setzt voraus, dass Akteure (actors) im Aktivitätsdiagramm nur die Aktivitäten ausführen für die sie die Rechte (rights) haben.
UMLsec
Kommunikationsarten
- s ∈ {«wire»; «encrypted»; «LAN»; «smart card»; «POS device»; «Internet» «issuer node»; }
UMLsec
Kommunikation
Bedrohungen
ThreatsA(s) ⊆ {delete; read; insert; access}:
UMLsec
Kommunikation
Beispielangreifer
UMLsec
Kommunikation
secrecy
- «secrecy», {secrecy}
- markiert Ausdrücke, Attribute oder Argumentvariablen von Objekten deren Geheimhaltung sichergestellt werden soll; markiert Operationen, bei denen sichergestellt werden soll, dass deren Argumente und Rückgabewerte geheim gehalten werden sollen.
- s = «secrecy», dann read ∉ Threats (t).
UMLsec
Kommunikation
integrity
- {integrity}
- hat als Wert Paare (v;E)
- v: Variable eines Objekts, bei welchem die Integrität geschützt werden soll.
- E: Menge von in Verbindung zu v stehenden Ausdrücken, die akzeptiert werden
- s = «integrity», dann insert ∉ Threats (t).
UMLsec
Kommunikation
fresh
- {fresh}
- atomare Daten (Elemente der Menge Data ⋃ Keys) die neu generiert werden sollten.
UMLsec
Sichere Kommunikation
«secure links»
Stellt sicher, dass unter Beachtung des Angreifermodells die Sicherheitsanforderungen bei der Kommunikation zwischen den Komponenten von der physikalischen Ebene unterstützt werden.
UMLsec
Sichere Kommunikation
«secure dependencies»
- Kennzeichnet Subsystem welches statische Strukturdiagramme beinhaltet
- Stellt sicher, dass «call»- und «send»-Abhängigkeiten zwischen Komponenten Sicherheitsanforderungen für versendete Daten respektieren.
- Mit Tags {secrecy}, {integrity} vom Stereotyp «critical».
- Genauer: für «call»- oder «send»-Abhängigkeiten zwischen einem Objekt oder Subsystem C und einem Interface I eines Objekts oder Subystems D müssen folgende Bedingungen erfüllt sein:
- Nachricht in I ist mit {secrecy} (bzw. mit {integrity} oder {high}) in C markiert gdw. sie auch in D markiert ist.
- Wenn Nachricht in I als {secrecy} (bzw. als {integrity} oder {high}) in C markiert ist, dann ist die Abhängigkeit mit«secrecy» (bzw. mit «integrety» oder «high») markiert.
UMLsec
Sichere Kommunikation
«data security»
Stellt sicher, dass die Sicherheit auf der Verhaltensebene gegeben ist
Java
Guarded Objects
- Zugriffschutz auf bestimmte Objekte
- GuardImplementierung gibt an ob der Anfragende Zugriffsrecht hat
- Zugang über getObject Methode.
- checkGuard Methode in java.security.Guard kontrolliert Zugang.
- Gibt Referenz oder SecurityException zurück
UMLsec
«guarded access»
- Stellt sicher: in Java «guarded» Klassen nur durch {guard} Klassen aufrufbar.
- Constraints:
- Referenzen der «guarded» Objekte: geheim.
- Jede «guarded» Klasse durch zugehörige {guard} Klasse abgesichert.
UMLsec
«guarded access»
Guarded Objekt
- Jedes «guarded» Objekt im Teilsystem kann nur durch {guard} spezifizierte Objekte an den «guarded» Objekt angebracht, zugegriffen werden
- Formal: Nehme an name ∉ KpA für Gegnertyp A unter Berücksichtigung das jeder Name name einer Instanz von einem «guarded» Objekt ist bedeutet, dass eine Referenz öffentlich nicht verfügbar ist.
- Annahme: für jeden «guarded» Objekt gibt es eine Statechart Spezifikation eines Objekts dessen Name in {guard} gegeben ist. => Um Weitergabe von Referenzen zu modellieren.
UMLsec
«no down-flow»
- Stelle sicheren Informationsfluss sicher. Bedingung
- Jeder als {secrecy} spezifizierter Datenwert beeinflusst nur als {secrecy} spezifizierte Datenwerte.
- Man kann keine Informationen über mit secrecy definierte Dateien durch nicht secrecy Variablen erhalten.
UMLsec
«data security»
- Sicherheitsanforderungen der als <<critical>> markierten Daten gegen Bedrohungsszenarien von Verteilungsdiagramm durchgesetzt.</critical>
- Einschränkungen: Als {secrecy}, {integrity}, {authenticity}, {fresh} markierte Daten erfüllen jeweilige formalisierte Sicherheitsanforderungen.
- Einschränkung mit «data security» erfordert, dass diese Anforderungen bzgl. Angegebenes Gegnermodell erfüllt sind.
Kryptographische Protokolle
Sicherheitsprotokolle
Probleme
- Schwache Kryptographie.
- Zentraler Nachrichten-Austausch.
- Schnittstellen,
- Prologe,
- Epiloge.
- Verwendung.
- Implementierungsfehler.
Kryptographische Protokolle
ISO/OSI 7-Schichten-Modell
- Application
- Presentation
- Session
- Transport
- Network
- Data Link
- Physicak
Kryptographische Protokolle
Auf welchen Schichten des ISO/OSI Modells findet welche Verschlüsselung statt?
Kryptographie: Schlüssel
Eigenschaften
- Keys: Folge mit partieller injektiver Abbildung:
- ( )-1 : Keys → Keys
- Schlüssel: unabhängig (Keine Gleichungen wie K = K’ + 1 für zwei verschiedene Schlüssel K, K’ ε Keys).
- Öffentlicher Schlüssel für Verschlüsselung und Überprüfung der Signatur benutzbar.
- Schlüssel, die für sicher gehalten werden, für Entschlüsselung und Unterzeichnung benutzbar.
- Schlüssel: entweder Verschlüsselungs- oder Entschlüsselungs-schlüssel (asymmetric), oder beides falls k k-1 = k0 zufriedenstellt (symmetric).
- Zahlen von symmetrischen & asymmetrischen Schlüssel: unendlich.
Kryptographie
Var
Definition
eine unendliche Folge von Variablen.
Kryptographie
Data
Definition
eine unendliche Folge von Datenwerten
Kryptographische Ausdrücke
- Exp: Menge der Krypto-Terme
- Bildung aus Symbolen in Mengen Data, Keys, Var
- Unter Verwendung der Operationen:
- _::_ (Konkatenation), head(_), tail(_),
- (_)-1 (K-1: zum Verschlüsselungsschlüssel K gehöriger Entschlüsselungsschlüssel).
- { _ }_ ({M}K: Verschlüsselung der Nachricht M mit Schlüssel K) .
- Dec_( ) (DecK(C): Entschlüsselung der Daten C mit Schlüssel K).
- Sign_( ) (SignK(M): Signatur der Nachricht M mit Schlüssel K).
- Ext_( ) (ExtK(S): Extrahieren der Signatur S mit Schlüssel K).
Kryptographische Ausdrücke
Konkatenation
- _::_
- A::B ⇒ AB
- Assoziativität gilt
- E1::E2::E3 für E1::(E2::E3) und fst(E1::E2) für head(E1::E2) etc.
Kryptographische Ausdrücke
Entschlüsselungsschlüssel
- (_)-1 (K-1: zum Verschlüsselungsschlüssel K gehöriger Entschlüsselungsschlüssel).
- ∀E,K. DecK-1({E}K)=E
Kryptographische Ausdrücke
Verschlüsselung
- {_}_ ({M}K: Verschlüsselung der Nachricht M mit Schlüssel K
- ∀E,K. DecK-1({E}K)=E
Kryptographische Ausdrücke
Signatur
- Sign_( ) (SignK(M): Signatur der Nachricht M mit Schlüssel K).
∀E,K. ExtK(SignK-1(E))=E
Kryptographische Ausdrücke
Extrahieren
- Ext_( ) (ExtK(S): Extrahieren der Signatur S mit Schlüssel K).
- ∀E,K. ExtK(SignK-1(E))=E
Kryptographische Ausdrücke
head
- ∀E1,E2. head(E1::E2)=E1
- fst(E) =def head(E)
- snd(E) =def head(tail(E))
- thd(E) =def head(tail(tail(E)))
Kryptographische Ausdrücke
tail
- ∀E1,E2. tail(E1::E2)=E2
- snd(E) =def head(tail(E))
- thd(E) =def head(tail(tail(E)))
Kryptographische Protokolle
Protokollablauf
Erklaren Sie die Unterschiede zwischen Secure Links und Secure Dependencies. Geben Sie dazu auch jeweils ein Beispiel an.
- Secure Links wird verwendet, um die Sicherheit physikalischer Verbindungen zu modellieren. Ein Beispiel dafur findet sich in Deployment-Diagrammen, in denen die tatsachliche Verteilung von Softwarekomponenten auf Teilsysteme modelliert wird.
- Secure Dependency wird dazu verwendet die Sicherheitsanforderungen zwischen einzelnen Klassen und deren Interaktion, mit anderen Worten deren Aufrufe und den Informationsfluss zu modellieren. Ein typisches Beispiel ist das Erzeugen von Zufallszahlen uber eigene Klassengrenzen hinweg. Dabei muss die Zufallszahl geheim bleiben.
Wie unterscheiden sich die in der Vorlesung genannten IT-Datensicherheitsanforderungen von System-Sicherheitsanforderungen an verlässliche Systeme in Domänen wie Avionik, Automobil etc.?
In den Avionik- oder Automobil- Domänen bedeutet der Begriff Sicherheit eher Zuverläßig- keit und die einwandfreie Funktionsweise. Diese Anforderungen dienen dazu, das menschliche Leben zu schützen bzw. nicht zu gefährden.
In der IT-Sicherheit bedeutet Sicherheit eher Schutz von Informationen, z.B. durch die Verschlüsselung von Nachrichten zum Schutz vor unbefugtem Lesezugriff. Im Englischen existieren dazu auch die beiden Begriffe “Safety” und “Security”.
Warum ist Datensicherheit in der digitalen Welt schwieriger zu erreichen als in der physikalischen?
Es geht hier um die unterschiedlichen physikalischen Gesetze in der realen und der digitalen Welt. Für das Kopieren oder das Manipulieren von Objekten in der realen Welt braucht man normalerweise spezielle Geräte und Materialien/Ersatzteile. Sogar dann ist es gar nicht so einfach eine exakte Kopie zu erstellen (Es sei hier auf das Fa ̈lschen von Geld hingewiesen).
In der digitalen Welt dagegen ist alles auf 0 und 1 aufgebildet, was das Erstellen von identischen Kopien ermöglicht. Diese Eigenschaft macht z.B. die Gewährleistung von Zu- rechenbarkeit und Nichtabstreitbarkeit zu einer schwierigen Aufgabe.
Erläutern Sie die Funktionsweise von hybrider Verschlüsselung. Das Verfahren als solches ist deutlich komplizierter als jeweils nur symmetrische oder asymmetrische Verschlüsselung einzusetzen. Warum wird es dennoch verwendet?
Bei hybrider Verschlüsselung wird mittels asymmetrischer Verschlüsselung ein Session-Key (symmetrischer Schlüssel) ausgetauscht. Die eigentliche Datenverbindung wird dann mit dem symmetrischen Schlüssel verschlüsselt. Auf diese Art kann man die Vorteile asymmetrischer Verschlüsselung beim Schlüsselmanagement mit den Performanzvorteilen symme- trischer Verfahren kombinieren. Da die Datenverbindung dann mit einem symmetrischen Schlüssel erfolgt, erhält der Angreifer so auch nur recht wenig Daten mit denen er versu- chen kann das asymmetrische Verfahren zu brechen.
