Evidential Tool Bus

Das Projekt ETB2 verfolgt das Ziel, Techniken zur Begründung von Sicherheitsaussagen für Software auf Basis verteilter Argumente und unterstützender Nachweise zu entwickeln.

Hierzu entwickelt das Projekt einerseits formale und semi-formale Sprachen zur Spezifikation von Sicherheitsargumentationsmustern, wie sie in Zertifizierungsstandards, Richtlinien und etablierten industriellen Verfahren verwendet werden. Die entwickelten Sprachen sollen zugleich ausdrucksstark genug sein, um daraus abgeleitete Sicherheitsaussagen und Argumentationsketten präzise zu beschreiben.

Andererseits entwickelt ETB2 Algorithmen für die dezentrale Ausführung von Sicherheitsargumenten, bei denen mehrere Entitäten zusammenwirken, um eine bestimmte Behauptung zu begründen. Dabei ist insbesondere ein sicherer Austausch von Behauptungen und den dazugehörigen Nachweisen zwischen den beteiligten Entitäten erforderlich.

Darüber hinaus legt das Projekt einen besonderen Schwerpunkt auf neu entstehende Anwendungen der Künstlichen Intelligenz (KI). Hierzu werden Sicherheitsargumentationsmuster sowie geeignete Nachweisartefakte für Software mit lernfähigen Komponenten entwickelt.

ETB2 basiert auf den folgenden Eckpfeilern:

Formale Argumente

ETB2 formalisiert die in Sicherheitsargumenten verwendeten Richtlinien als logische Spezifikationen in Cyberlogic, einer Attestierungslogik erster Ordnung für beweiskräftige Transaktionen. Diese Richtlinien werden in Form verteilter Logikprogramme umgesetzt. Die Spezifikationen kombinieren logische Inferenz mit Nachweisen, die durch Verifikations-Workflows erzeugt werden. Dadurch erhalten die in Safety Cases verwendeten Sicherheitsargumente eine präzise Semantik und ermöglichen eine inkrementelle, kontinuierliche und automatisierte Zertifizierungsbewertung.

Workflows als Dienste

Automatisierte Software-Verifikations-Workflows, die in Cyberlogic spezifiziert sind, ermöglichen die automatisierte Generierung von Nachweisen durch die Ausführung bestehender moderner Software-Verifikationswerkzeuge. Die Dienste werden als dezentrale, containerbasierte Komponenten bereitgestellt und unterstützen dadurch die Skalierbarkeit in operativen Umgebungen.

Dezentrale Sicherheitsgewährleistung

ETB2 ermöglicht die dezentrale Zusammenarbeit mehrerer Werkzeuge und Entitäten zur Erzeugung, Verwaltung und Bewertung von Sicherheitsaussagen. Durch den sicheren Austausch von Behauptungen und Nachweisen sowie die kontinuierliche Ausführung von Verifikations-Workflows unterstützt das Framework eine durchgängige und nachvollziehbare Sicherheitsgewährleistung über den gesamten Lebenszyklus eines Systems hinweg.

Intern und über verschiedene Projekte