Integrated formal modeling and automated analysis of computer network attacks

Abstract

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ändigere Sicht auf Computernetzwerkangriffsszenarien zu erhalten, müssen daher mehrere Ansätze, und damit auch Modelle, Formalismen und Werkzeuge, eingesetzt werden. Sowohl die Modellierungs- als auch die Analysearbeit fallen damit mehrfach an und Konsistenz zwischen den verschiedenen Modellen und Analyseergebnissen lä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 Modelle sind ausdrucksstark genug, um dynamische Änderungen zu beinhalten. Vielfältige Eigenschaften können über unterschiedliche Mechanismen spezifiziert werden. Da integrierte 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öglichkeiten auf allen Ebenen, die Modellierung mit einer objektorientieren und kompositionalen, aber trotzdem auf einer einfachen Struktur basierenden Sprache, und dem Einsatz eines dem aktuellen Stand der Forschung entsprechenden Analysewerkzeuges sind 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.

In the field of formal modeling and analysis as related to computer network security, existing approaches are highly specialized towards either a protocol, node, or network view. Typically, they are even further specialized towards a specific subset of one view (e.g., a certain class of protocols, interactions of local node components, or network propagation of predefined vulnerabilities). Thus, each approach covers only a small part of the aspects related to practical computer network attack scenarios. Often, further restrictions with respect to the dynamics allowed for the model, properties supported or user guidance required during analysis, have to be observed. Multiple approaches, and thus models, formalisms, and analysis tools, need to be employed to provide a more complete view of computer network attack scenarios. Both the modeling task and the analysis task have to be done multiple times and it is hard to ensure the consistency of the models and analysis results. We present a novel approach that comprehensively integrates the protocol, node, and network view on a middle level of detail. Furthermore, the models are expressive enough to support dynamic changes. A wide range of properties can be specified using different mechanisms. As integrated models naturally are of higher complexity than more specialized models limited to a single view, analysis is particularly challenging. Generally, automated analysis approaches quickly fail due to state space explosion effects. Nevertheless, by careful modeling, considering optimization possibilities at all stages, modeling using an object-oriented and compositional yet simple structured language, and employing a state of the art analysis tool we are able to achieve automated analysis. Our approach is based on the high-level specification language CTLA 2003, a framework for modeling computer network attack scenarios, a scheme for translating CTLA 2003 to PROMELA, the CTLA2PC translation and optimization tool, and the powerful model checker SPIN. For demonstrating the feasibility of our approach, the modeling and analysis of three case studies involving multi-node dynamic network scenarios is presented. In these case studies, precise attack sequences are automatically predicted as violations of abstract security properties.