STING: Symbolische Taint-Analyse und Modell Inferenz für die Generierung von Exploits

• Antragsteller: Professor Dr. Falk Howar
• Subject Area: Softwaretechnik und Programmiersprachen ; Sicherheit und Verlässlichkeit, Betriebs-, Kommunikations- und verteilte Systeme
• Term: since 2022
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 495857894

Software definiert die Infrastruktur des einundzwanzigsten Jahrhunderts. Insbesondere Web-Anwendungen machen einen großen Teil dieser digitalen Infrastruktur aus, weshalb ihre Sicherheit von höchster Bedeutung ist. Eine formale Analyse der Sicherheit von Webanwendungen ist jedoch schwierig. Viele der bekannten Schwachstellen, die in der Liste der Common Vulnerability and Exposures (CVEs) aufgeführt sind, beziehen sich auf den Informationsfluss durch Webanwendungen von einer potenziell bösartigen Quelle zu einer geschützten Senke. Angreifer nutzen diese Datenflüsse aus, um bösartigen Code an Stellen zupropagieren, die er nicht erreichen sollte.Eine Mischung aus zustandsbehafteten und zustandslosen Programmierparadigmen, textbasierten Protokollen zwischen denSchichten und mehreren verschiedenen Programmiersprachen in den Schichten machen es schwierig, den kompletten Stack auf einmal zu analysieren. Bestehende Analysetechniken zur Entdeckung von Schwachstellen fallen meist in eine von zwei Klassen: Dynamische Analysen führen Web-Anwendungen aus, indem sie Eingaben und Anfragen bereitstellen und die Ausgaben beobachten. Diese Analysen können zwar reproduzierbare Testfälle für Schwachstellen liefern, explorieren jedoch nur einen Teil des möglichen Ausführungsraums. Überapproximierende statische Analysetechniken hingegen berechnen Informationen über das Programmverhalten und den Datenfluss einer Anwendung auf Grundlage des Quellcodes, meist für einzelne Anforderungsmethoden innerhalb einzelner Schichten einer Anwendung. Diese Analysen können keine Beweise für tatsächliche Schwachstellen liefern und produzieren falsch positive Alarme. Das Ziel des STING-Projekts ist die Entwicklung einer präzisen, skalierbaren, kompositionalen und automatisierten formalen Analyse zur Überprüfung der Sicherheit von mehrschichtigen webbasierten Anwendungen. Die vorgesehene Analyse zerlegt das zu analysierende Problem, indem zunächst Modelle der einzelnen Schichten und relevanter Teile von Frameworks generiert werden und dann verwendet werden, um Sicherheitslücken zu erkennen und Testfälle für gefundene Schwachstellen zu synthetisieren.Die Persistenzschicht z.B. besteht aus externen Ressourcen und wird mit Black-Box-Lerntechniken analysiert, die Modelle(z.B. Registerautomaten) des zustandsbehafteten Verhaltens erzeugen. Die Geschäftslogik besteht aus containerisierten Java-Komponenten, die durch eine kombinierte Concolic-Execution- und Taint-Analyse analysiert werden, was eine umfassende Erfassung des Verhaltens und eine Analyse des Datenflusses in der Schicht ermöglicht. Um schließlich das Verhalten der Anwendung über die Schichten hinweg zu prüfen, werden White-Box-Techniken verwendet, die das Verhalten für Sequenzen von Anfragen zu berechnen, indem die generierten Modelle über den gesamten Technologiestack hinweg integriert werden.

• DFG Programme: Sachbeihilfen