Integrated formal modeling and automated analysis of computer network attacks

摘要

Die vorhandenen Ansätze zur formalen Modellierung und Analyse von Computernetzwerksicherheit sind entweder auf eine Protokoll-, Knoten-, oder Netzwerksicht ausgerichtet. Meist beschränken sie sich sogar auf einen speziellen Teilbereich einer dieser Sichten (z.B. eine bestimmte Art von Protokollen, die Interaktion zwischen den lokalen Komponenten eines Knotens, oder die Ausbreitung vordefininierter Verletzlichkeiten). Insgesamt wird von jedem Ansatz jeweils nur ein kleiner Teil der Aspekte, die in praktischen Computernetzwerkangriffsszenarien vorkommen, abgedeckt. Hinzu kommen oft weitere Einschränkungen in Bezug auf Unterstützung dynamischer Änderungen, modellier- und untersuchbare Eigenschaften, benötigte Unterstützung der Analyse durch den Benutzer, usw. Um eine vollständigereSicht auf Computernetzwerkangriffsszenarien zu erhalten, müssen daher mehrereAnsätze, und damit auch Modelle, Formalismen und Werkzeuge, eingesetzt werden.Sowohl die Modellierungs- als auch die Analysearbeit fallen damit mehrfachan und Konsistenz zwischen den verschiedenen Modellen und Analyseergebnissenlässt sich nur sehr schwer erreichen.In dieser Arbeit wird ein neuartiger Ansatz vorgestellt, der die Protokoll-, Knoten und Netzwerksicht auf mittlerer Detailebene übergreifend integriert. Die Modellesind ausdrucksstark genug, um dynamische Änderungen zu beinhalten. VielfältigeEigenschaften können über unterschiedliche Mechanismen spezifiziert werden. Daintegrierte Modelle deutlich komplexer als eingeschränkte Modelle für einen Teilbereich sind, ist die Analyse besonders schwierig. Im Allgemeinen schlagen Ansätze zur automatischen Analyse schnell durch Zustandsraumexplosion fehl. Durch eine intelligente Modellierung, die Berücksichtigung von Optimierungsmöglichkeitenauf allen Ebenen, die Modellierung mit einer objektorientieren und kompositionalen,aber trotzdem auf einer einfachen Struktur basierenden Sprache, und dem Einsatzeines dem aktuellen Stand der Forschung entsprechenden Analysewerkzeugessind wir trotzdem in der Lage, erfolgreich automatisiert zu analysieren.Unser Ansatz basiert auf der Spezifikationshochsprache CTLA 2003, einem Framework zur Modellierung von Computernetzwerkangriffsszenarien, einem Übersetzungsschema von CTLA 2003 nach PROMELA, dem CTLA2PC Übersetzungs- und Optimierungswerkzeug, und dem mächtigen Modellchecker SPIN. Die Durchführbarkeit unseres Ansatzes wird durch die Modellierung und Analyse von drei dynamischen Netzwerkszenarien zunehmender Komplexität aufgezeigt. In diesen Szenarien werden konkrete Angriffsfolgen als Verletzungen vorgegebener Sicherheitseigenschaften automatisch aufgedeckt.