Evidential Tool Bus

Das Projekt ETB2 zielt darauf ab, Techniken zu entwickeln, um Sicherheitsaussagen für eine gegebene Software mithilfe von dezentralen Argumenten und unterstützenden Beweisen zu begründen. Einerseits entwickelt das Projekt formale und semiformale Sprachen zur Spezifikation von Sicherheitsargumentationsmustern, die in Zertifizierungsstandards und -richtlinien sowie in der bewährten industriellen Praxis zu finden sind. Die Sprachen sollen auch aussagekräftig genug sein, um daraus resultierende Sicherheitsaussagen und Argumente zu beschreiben.

Auf der anderen Seite entwickelt das Projekt Algorithmen für die dezentrale Ausführung von Sicherheitsargumenten, bei denen mehrere Entitäten zusammenarbeiten, um eine bestimmte Behauptung aufzustellen. Es ist wichtig, einen sicheren Weg für den Austausch von Behauptungen und unterstützenden Beweisen zwischen interagierenden Entitäten zu finden. Schließlich legt das Projekt einen besonderen Fokus auf neu entstehende Anwendungen von Künstlicher Intelligenz (KI) durch die Entwicklung von Sicherheitsargumentationsmustern und ausreichenden Beweisartefakten für Software mit lernfähigen Komponenten.

ETB2 ist auf den folgenden drei Eckpfeilern aufgebaut:

Formale Argumente: ETB2 formalisiert die in Sicherheitsargumenten verwendeten Richtlinien als logische Spezifikationen in Cyberlogic, einer Bescheinigungslogik erster Ordnung für beweiskräftige Transaktionen. Diese Richtlinien werden in Form von verteilten Logikprogrammen programmiert. Diese Spezifikationen kombinieren logische Inferenz mit Beweisen, die durch Verifikationsworkflows erzeugt werden. Das bedeutet, dass Sicherheitsargumente, die in Sicherheitsfällen verwendet werden, eine präzise Semantik haben und somit eine inkrementelle, kontinuierliche und automatisierte Bewertung der Zertifizierung ermöglichen.

Workflows als Dienste: Automatisierte Software-Verifikations-Workflows, die in Cyberlogic spezifiziert sind, ermöglichen die automatisierte Generierung von Beweisen durch die Ausführung bestehender, moderner Software-Verifikationswerkzeuge. Dienste sind dezentrale, container-basierte Komponenten, die solche Verifikations-Workflows bereitstellen und so die Skalierbarkeit in operativen Umgebungen unterstützen.

Intern und über verschiedene Projekte