Evidential Tool Bus

Evidential Tool Bus

Ein Rahmenwerk für kontinuierliche und nachhaltige Softwarezertifizierung

Evidential Tool Bus

Die Komplexität eingebetteter Software und die steigenden Anforderungen an die Sicherheit übersteigen bereits die Möglichkeiten aktueller Verifikations- und Zertifizierungsmethoden. Das Framework Evidential Tool Bus (ETB2) bietet container-basierte Dienste, die Verifikations-Workflows automatisch und kontinuierlich dezentral ausführen, um formale Sicherheitsargumente zu generieren, die durch nachvollziehbare Beweise unterstützt werden und die Sicherheit der Software bestätigen.

Projektbeschreibung

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.

Forschungsbeitrag

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.

Förderung

Intern und über verschiedene Projekte

Projektdauer

fortlaufend

Dr. Tewodros Beyene

Ihr Kontakt

Dr. Tewodros Beyene

+49 89 3603522 24
beyene@fortiss.org

Weitere Informationen

Projektpartner

Publikationen