Die fragile Sicherheit der heutigen IT-Infrastruktur ist das Ergebnis eines ständigen Wettrüstens zwischen Angreifern und Verteidigern. Während die Verteidiger ihre Fähigkeiten Angriffe zu bewältigen, entwickeln die Angreifer immer neue böswillige Methoden, verfeinern klassische Angriffe auf Programmierfehler und nutzen eine immer breitere Angriffsfläche, einschließlich Router, Firmware und das Internet der Dinge.
Formale Methoden bieten einen Ausweg aus diesem Wettrüsten. Basierend auf mathematisch präzisen System- und Angreifermodellen können wir ganze Klassen von Angriffsstrategien systematisch eliminieren. Mit den jüngsten Fortschritten in der Logik und der automatisierten Entscheidungsfindung kann die Anwendung sogar weitgehend automatisiert werden. Allzu oft basieren die formalen Methoden jedoch auf abstrakten Systemmodellen und lassen daher Lücken, die in diesen Modellen nicht berücksichtigt werden. Dieser Forschungsbereich zielt auf einen phasenweisen Übergang in der Reichweite und praktischen Anwendbarkeit von formalen Methoden und strebt eine computergestützte Analyse und Konstruktion sicherer Systeme mit den bestmöglichen formalen Garantien an. Dazu gehört die Entwicklung von Methoden zur Erlangung strenger Sicherheitsgarantien für Systeme und Software, Laufzeitmethoden zur Überwachung und Umsetzung, Methoden in der Entwicklungs-Zeit für statische Analyse und Programmreparatur sowie eine umfassende Methodik zum Aufbau sicherer großer Systeme aus kleinen sicheren Bausteinen.
National Conference of the American Association for Artificial Intelligence (AAAI)
Symposium on Principles of Programming Languages (POPL)
