Evidentia

Evidentia

Ein Rahmenwerk für kontinuierliche und nachhaltige Softwarezertifizierung

Evidentia

Die Komplexität eingebetteter Software und die steigenden Anforderungen an die Sicherheit übersteigen bereits die Möglichkeiten aktueller Verifikations- und Zertifizierungsmethoden. Das Evidentia-Framework bietet container-basierte Dienste, die Verifikationsworkflows 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 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 semi-formale 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

Evidentia ist auf den folgenden drei Eckpfeilern aufgebaut:

Formale Argumente: Evidentia 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.

Verteilte Rechenschaftspflicht: Die Distributed Ledger Technology gewährleistet die Nachvollziehbarkeit von Transaktionen durch die Protokollierung von beweiskräftigen Transaktionen. Dies bedeutet, dass es für Zertifizierungsauditoren möglich ist, aus dem Protokoll abzuleiten, welche Partei für Beweise und welche Teile von Sicherheitsargumenten verantwortlich ist.

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

SRI International

Publikationen

  • 2018Evidential and Continuous Integration of Software Verification ToolsTewodros Beyene und Harald Rueß In Formal Methods, pages 679-685, Cham, Springer International Publishing. DetailsBIB