LCM: Hochskalierende Capability-Systeme

• Antragsteller: Professor Dr. Hermann Härtig
• Fachliche Zuordnung: Sicherheit und Verlässlichkeit, Betriebs-, Kommunikations- und verteilte Systeme
• Förderung: Förderung von 2020 bis 2022
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 445973455

Im Kontext des Fachgebietes Betriebssysteme versteht man unter Capabilities einen Mechanismus für die feingranulare Steuerung der Interaktion zwischen ansonsten isolierten Einheiten. Nachdem capability-basierte Systeme für lange Zeit nur im Elfenbeinturm akademischer Forschung eine Rolle spielten, bilden sie inzwischen die technische Basis für viele sicherheitskritische Systeme insbesondere im Zusammenhang mit mikrokern-basierten Systemen. Beispiele sind Rechner in kritischen Regierungs- und Militäreinrichtungen sowie Steuerungen in Kraftfahrzeugen. Zu den capability-basierten Betriebssystemen gehören L4/Fiasco und M3, beides an der TU Dresden entworfene und weiterhin gepflegte Systeme.Das Ziel dieses Projekts ist die Klärung der Frage ob sich sehr große Systeme konstruieren lassen, welche direkt auf ein darunter liegendes Capability-System aufbauen. Dazu benötigt man hoch-skalierende Capability-Systeme, die als Basis für große Applikationen dienen können. Unseres Wissens nach und zu unserer Überraschung wurde diese Frage bisher nicht gestellt. Die größten Herausforderungen sind Entwurf und Implementierung der Datenstrukturen und Algorithmen mit deren Hilfe sich Capabilities im großen Maßstab schützen und durchsetzen lassen, insbesondere die Umsetzung der Schlüsseloperationen Delegation und Revokation und diese Algorithmen dabei robust gegen Fehler zu gestalten. Erste Anstrengungen diese Forschungsfrage zu beantworten wurden bereits Anfang 2017 von Asst. Prof. Dr. Pramod Bhatotia (Ko-Antragsteller) während seiner Zeit an der TU Dresden gestartet. Dies geschah in enger Kooperation mit Prof. Dr. Hermann Härtig, in dessen Gruppe L4/Fiasco und M3 entstanden.Ein erster pragmatischer und vielversprechender Ansatz zu diesem Thema bestand aus einer ad-hoc Analyse von SemperOS - einer verteilten Variante des M³ Capability-Systems welche bis zu 640 Knoten unterstützt. In dem hier beantragten Projekt wollen wir das Thema auf eine grundsätzlichere Art und Weise untersuchen. Dafür soll an einer kanonischen Systemstruktur für hoch-skalierende Capability-Systeme, formalen Modellierungen und Verifikation von Algorithmen, sowie einer sorgfältigen Evaluierung anhand von Simulationen und Implementierungen gearbeitet werden.

• DFG-Verfahren: Sachbeihilfen
• Internationaler Bezug: Großbritannien
• Kooperationspartner: Professor Dr.-Ing. Pramod Bhatotia