Sprachbasierte Spezifikation und deduktive Verifikation von Sicherheitseigenschaften

• Antragsteller: Professor Dr. Bernhard Beckert, seit 10/2016
• Fachliche Zuordnung: Softwaretechnik und Programmiersprachen
• Förderung: Förderung von 2010 bis 2017
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 183818606

Thema des Projektes ist die sprachbasierte Spezifikation und deduktive Verifikation von Sicherheitseigenschaften.In den letzten Jahren wurden in der formalen Verifikation funktionaler Eigenschaften von Computerprogrammen ungeheure Fortschritte erreicht. Zudem wurden wegweisende Arbeiten publiziert, die zeigen, dass es grundsätzlich möglich ist, Informationsflusseigenschaften als Beweisverpflichtungen in Programmlogiken zu formulieren. Das übergeordnete Ziel dieses Projektes ist es, diese Fortschritte und unsere eigenen Erfahrungen mit formalen Methoden für funktionale Programmeigenschaften auch für die Spezifikation und Verifikation von Sicherheitseigenschaften nutzbar zu machen.Das Projekt leistet folgende Beiträge zu den drei Leitthemen des Schwerpunktprogramms 1496 "RS3", der Formalisierung und der Verifikation von Sicherheitseigenschaften, sowie der Zusicherung von Sicherheit "im Großen":* Wir definieren Syntax und Semantik einer Spezifikations- und Programmannotationssprache für Informationsflusseigenschaften von Computerprogrammen.* Wir entwickeln und implementieren ein System, das es erlaubt, formal zu beweisen, dass ein Programm seine Spezifikation erfüllt. Dieses System genügt den im Antrag des Schwerpunktprogramms formulierten Anforderungen an Korrektheit, Genauigkeit, Skalierbarkeit und Benutzbarkeit. Das KeY-System wird uns als technologische Basis dienen.In Phase 3 des Schwerpunktprogramms konzentriert sich die Arbeit auf Erweiterung der Leistungsfähigkeit und Reichweite der Methoden. Dies erfolgt mittels Modularisierung und Kopplung vonProgrammeingenschaften, Betonung quantitativer Sicherheitsmaße, Integration verschiedener Analysetypen und Schließen der Spezifikationslücken dazwischen.

• DFG-Verfahren: Schwerpunktprogramme
• Teilprojekt zu: SPP 1496: Reliably Secure Software Systems - Zuverlässig sichere Softwaresysteme
• Ehemaliger Antragsteller: Dr. Vladimir Klebanov, bis 10/2016