Zertifizierende Algorithmen für interaktive Komponenten und verteilte Systeme

• Antragsteller: Professor Dr. Wolfgang Reisig
• Fachliche Zuordnung: Theoretische Informatik
• Förderung: Förderung von 2014 bis 2019
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 261369405

Ein zertifizierender Algorithmus produziert bei jeder Berechnung zusätzlich zum Resultat noch einen Zeugen, der die Korrektheit des Resultats zeigt. Im besten Fall ist der Zeuge unmittelbar verständlich. Andernfalls überprüft ein (vergleichsweise einfacher) Checker-Algorithmus den Zeugen. Seit den 2000er Jahren werden für zahlreiche "klassische" Algorithmen zertifizierende Varianten entwickelt. Beispielsweise enthält die LEDA-Bibliothek des MPI Saarbrücken zahlreiche zertifizierende Algorithmen.Rechnerintegrierte Systeme und Infrastrukturen sind heutzutage oft aus interaktiven Komponenten aufgebaut, die als Knoten eines verteilten Systems lose gekoppelt miteinander interagieren. Algorithmen für interaktive Komponenten terminieren im Allgemeinen nicht. Weiterhin kennen die Komponenten eines verteilten Systems meist nicht die vollständige Struktur des Systems. Algorithmen für solche Komponenten und Systeme verhalten sich daher prinzipiell anders als klassische Algorithmen. In diesem Projekt wird untersucht, wie weit die Idee der Zertifizierung bei Algorithmen für interaktive Komponenten und verteilte Systeme trägt. Das ist deshalb besonders interessant, weil solche Systeme oft von Nicht-Informatikern genutzt werden, ihre inneren Abläufe der Geheimhaltung unterliegen und die Korrektheit ihrer Nutzung überzeugend dargestellt werden soll.Dieses Ziel wird von mehreren Seiten her zugleich angestrebt. Wir gehen zunächst von den bekannten zertifizierenden Algorithmen für Datenstrukturen aus und versuchen, die dabei verwendeten Konstruktionsverfahren für Zeugen und deren Checker auf allgemeine interaktive Komponenten zu übertragen. Dazu gehört insbesondere die Idee, dass der Algorithmus als Zeuge einen Datenstrom produziert, den der Checker zeitlich versetzt, aber nebenläufig prüft.Algorithmen für verteilte Systeme bestehen oft aus Algorithmen für interaktive Komponenten. Interessant ist deshalb die Frage nach der Komponierbarkeit zertifizierender Komponenten zu einem zertifizierenden System.Ein Netzwerk aus Rechnerknoten und Kommunikationskanälen ist ein spezielles verteiltes System. Für solche Netzwerke gibt es zahlreiche bekannte Algorithmen, beispielsweise Kommunikationsprotokolle, die ein mögliches Fehlverhalten der Kommunikationskanäle ausgleichen. Das wirft die interessante Frage auf, ob solche Protokolle auf spezielle Weise zertifizierend gestaltet werden können.In einem Netzwerk kann jeder Knoten nur mit seinen unmittelbaren Nachbarn kommunizieren. Das reicht, um globale Konstrukte des Netzwerks zu bilden und zu nutzen (beispielsweise einen virtuellen spannenden Baum). Dafür gibt es bereits geeignete Algorithmen; sie sollen nun zertifizierend ergänzt werden. Interessant ist es auch, bekannte zertifizierende Algorithmen auf Graphen zu Algorithmen auf den Knoten eines Netzwerks umzugestalten, zusammen mit den Zeugen und deren Checkern.

• DFG-Verfahren: Sachbeihilfen