Sichern des Informationsflusses in parallelen Systemen

Den Schutz vertraulicher Informationen zu gewährleisten, ist ein entscheidender Aspekt heutiger Anwendungen. Das Hauptziel ist, ungewollte Leaks an Leute zu verhindern, die zuschauen, vor allem wenn sie böse Absichten haben. Um dieses Problem anzugehen, können Systeme zur Kontrolle des Informationsflusses (IFC) helfen, sicherzustellen, dass sensible Daten nicht unangemessen entweichen.

In diesem Artikel diskutieren wir ein IFC-System, das für Programme entwickelt wurde, die über Nachrichten kommunizieren, was eine gängige Methode in modernen Rechenumgebungen wie Cloud-Diensten und dem Internet der Dinge (IoT) ist. Diese Systeme haben normalerweise Regeln, die bestimmen, wie Nachrichten ausgetauscht werden. Um die Sicherheit in diesen Austäuschen aufrechtzuerhalten, können wir verhaltensorientierte Systeme nutzen, wie etwa Sitzungstypen.

Dieser Artikel stellt eine Methode vor, die IFC mit Sitzungstypen kombiniert und Fortschritte gegenüber früheren Forschungen in den folgenden Bereichen hervorhebt:

1. Unterstützung realistischer zyklischer Prozessnetzwerke anstelle von nur baumähnlichen Strukturen.
2. Ermöglichen flexiblerer, aber sicherer IFC-Operationen, die diese zyklischen Netzwerke ausnutzen.
3. Behandlung von Deadlocks als mögliche Leckstellen und Etablierung eines Konzepts namens deadlock-sensitive noninterference (DSNI) für korrekt typisierte Programme.

Um die Wirksamkeit dieses Systems zu zeigen, erstellen wir eine neue logische Beziehung, die es uns ermöglicht, zyklische Prozessnetzwerke zu analysieren. Diese Beziehung basiert auf linearer Logik und verbessert frühere Modelle, die auf Baumstrukturen beschränkt waren.

#Hintergrund

Viele moderne Anwendungen sind von Natur aus gleichzeitig, was bedeutet, dass sie mehrere Aufgaben gleichzeitig erledigen können, und sie verlassen sich oft auf nachrichtenbasierte Systeme. Dazu gehören beliebte Programmiersprachen wie Erlang, Go und Rust. Das theoretische Modell für diese nachrichtenbasierten Sprachen ist als Prozesskalculus bekannt.

Im Wesentlichen kann ein Programm als mehrere Prozesse gesehen werden, die durch Kanäle verbunden sind und Nachrichten austauschen, anstatt gemeinsamen Speicher zu verwenden oder Standardberechnungen durchzuführen. Nachrichten können sogar Kanäle selbst enthalten, was als höhergradiger Nachrichtenversand bekannt ist.

Ursprünglich verwendete das Prozesskalculus keine Typen. Im Laufe der Zeit wurde es jedoch verbessert, indem Typen hinzugefügt wurden, um festzulegen, welche Nachrichten über welche Kanäle gesendet werden können, während gleichzeitig bestimmte Eigenschaften wie die Verhinderung von Deadlocks und Datenrennen sichergestellt werden.

#Sitzungstypen

Sitzungstypen wurden geschaffen, um die Protokolle zu beschreiben, die diese Austausche regeln. Sie verwenden einen linearen Ansatz, um zu modellieren, wie sich der Zustand während eines Protokolls ändern kann. Diese Verbindung zwischen Sitzungstypen und linearer Logik hilft, nicht nur die Freiheit von Deadlocks und Rennen zu gewährleisten, sondern auch die Treue zum ursprünglichen Protokoll.

#Bedeutung der Sicherheit

Sicherheit ist ein weiterer wichtiger Aspekt moderner Anwendungen. Insbesondere der Schutz vertraulicher Informationen ist entscheidend, um Leaks an bösartige Beobachter zu verhindern, die sensible Informationen ableiten könnten.

Um dies zu erreichen, nutzen IFC-Systeme Typen, um die Möglichkeit von Leaks zu beseitigen. Sie verwenden eine Sicherheits-Hierarchie, bei der Informationen und Aktionen mit unterschiedlichen Sicherheitsstufen gekennzeichnet sind. Wenn ein Programm diesen Typen folgt, wird jeder Datenfluss von einer höheren Sicherheitsstufe zu einer niedrigeren verhindert, sodass Beobachter keine sensiblen Informationen erhalten können.

Fortgeschrittene Beweis-Techniken, wie logische Beziehungen, werden eingesetzt, um diese Nicht-Interferenz zu garantieren. Dabei wird zwischen zwei Arten von Nicht-Interferenz unterschieden: fortschrittssensitiv (wo das System berücksichtigt, wie ein Programm stecken bleiben könnte) und fortschrittsunempfindlich (was Abweichungen lässiger behandelt).

#Zyklische Prozessnetzwerke

Die Entwicklung von IFC-Systemen war in imperativen und sequentiellen Sprachkontexten häufiger. Im Gegensatz dazu war die Anwendung von IFC-Systemen in parallelen nachrichtenbasierten Umgebungen begrenzt.

Neuere Bemühungen haben begonnen, IFC für Sitzungstypen basierend auf linearer Logik zu untersuchen, obwohl die meisten dieser Systeme immer noch davon ausgehen, dass Prozessnetzwerke als Bäume geformt sind. Die realen Szenarien stellen oft ein breiteres Spektrum an Strukturen dar, wie zyklische Prozessnetzwerke, in denen es Rückkopplungsschleifen und Wiederverbindungen geben kann.

#Beitrag dieses Papiers

Dieser Artikel präsentiert drei Hauptbeiträge:

1. Ein IFC-Sitzungstyp-System, das für asynchronen Prozesskalculus geeignet ist und in der Lage ist, zyklische Prozessnetzwerke zu handhaben, um die Sicherheit und Treue der Kommunikation zu gewährleisten.
2. Eine logische Beziehung, die das Konzept von DSNI unterstützt und eine Äquivalenz zwischen Prozessen herstellt, die korrekt typisiert werden können.
3. Ein zentrales Ergebnis, das bestätigt, dass korrektes Typisieren DSNI garantiert, basierend auf einem grundlegenden Theorem, das aus unserer logischen Beziehung abgeleitet ist.

#Schlüssige Ideen hinter den Beiträgen

#Zyklische Prozessnetzwerke

Um zu veranschaulichen, wie zyklische Verbindungen IFC verbessern, können wir eine Situation betrachten, in der zwei Regierungen an wissenschaftlichen und geheimdienstlichen Bemühungen zusammenarbeiten.

In diesem Szenario sind die Austausche zwischen einer Regierungsbehörde und einer Geheimdienstagentur vertrauliche Informationen. Im Gegensatz dazu sollten die Austausche zwischen einer Regierung und der wissenschaftlichen Gemeinschaft keine Geheimdienstdaten beinhalten, um das Risiko von Spionage zu vermeiden.

Wir können zwischen Informationen mit hoher und niedriger Vertraulichkeit unterscheiden und verstehen, dass Kommunikationskanäle unterschiedliche Sicherheitsstufen haben können. Die beiden Regierungen können sich als verschiedene Abteilungen (Prozesse) vorstellen.

Im ersten Setup, ohne zyklische Verbindungen, sind die Regierungen auf einen Kommunikationskanal beschränkt. Dieser Kanal muss hohe Vertraulichkeit gewährleisten, was das Teilen wissenschaftlicher Informationen behindern kann.

Im zweiten Setup, mit doppelten Verbindungen, könnten die Regierungen wissenschaftliche Erkenntnisse teilen und gleichzeitig Geheimdienstinformationen kommunizieren. Dieses Setup könnte jedoch zu Situationen führen, in denen Geheimdienstinformationen aus den geteilten wissenschaftlichen Daten abgeleitet werden können.

Das ideale dritte Setup würde darin bestehen, die Regierungen in verschiedene Abteilungen zu unterteilen, wo Geheimdienste Informationen untereinander austauschen können, während nur die wissenschaftlichen Abteilungen Ergebnisse miteinander kommunizieren. Diese Trennung hilft, das Risiko des Verschleuderns sensibler Geheimdienstinformationen innerhalb der wissenschaftlichen Gemeinschaft zu minimieren.

#Deadlocks als Informationslecks

Zyklische Netzwerke bringen auch das Risiko von Deadlocks mit sich, bei denen Prozesse endlos aufeinander warten können. In den vorherigen Beispielen könnte beispielsweise eine Regierung auf Geheimdienstinformationen von der anderen warten und gleichzeitig auf eine Antwort auf ihre Anfrage hoffen, was das System zum Stillstand bringen kann.

Deadlocks können als ein Nebenschauplatz für das Lecken von Informationen wirken, weil der Zustand des Systems einem Beobachter indirekt Informationen über seine inneren Abläufe vermitteln kann. Wenn zwei Prozesse beispielsweise darauf warten, dass der andere etwas tut, kann der Beobachter folgern, dass sensible Informationen im Fluss sind.

Um diesem Problem zu begegnen, führen wir DSNI ein, eine Bedingung, bei der ein blockierter Prozess nur mit einem anderen gleichgesetzt wird, der ebenfalls blockiert ist. Dieses Design verhindert, dass Informationen durch Deadlocks entweichen.

#Überblick über das Informationsflusskontrolltyp-System

Unser IFC-System baut auf früheren Arbeiten auf, indem es ein Sitzungstyp-System mit IFC-Anforderungen anreichert. Wir konzentrieren uns auf die Sitzungstypgetypte asynchrone Variante des Prozesskalculus.

Kanäle erhalten maximale Geheimhaltungsstufen, die das höchste Niveau von Vertraulichkeit repräsentieren, das Nachrichten beim Übertragen über diese Kanäle haben können. Das Geheimhaltungsniveau des Prozesses kann steigen, wenn er neue Informationen erhält, darf jedoch die Geheimhaltungsstufen der Kanäle, mit denen er interagiert, nicht überschreiten.

Daher stellen wir sicher, dass keine Informationen über einen Kanal gesendet werden, es sei denn, das aktuelle Geheimhaltungsniveau des Prozesses erlaubt dies. Die Annotationen in unseren Typisierungsregeln sind darauf ausgelegt, diese Sicherheit effektiv zu verwalten.

#Umgang mit Deadlock-Sensitivität

Um die Sensitivität gegenüber Deadlocks zu implementieren, verfolgt unser Typsystem, wie Geheimhaltungsstufen über Prozessinteraktionen verwaltet werden. Wenn ein Prozess ein laufendes Geheimhaltungsniveau hat, wird dieses Niveau basierend auf den erhaltenen Informationen aktualisiert. Wenn ein Prozess versucht, Informationen auf einem höheren Geheimhaltungsniveau auszugeben, als erlaubt ist, wird er als falsch getypt betrachtet.

Der Schlüssel zur Aufrechterhaltung dieses deadlock-sensitiven Verhaltens liegt in der Dynamik der laufenden Geheimhaltung. Die Logik hinter DSNI ist darauf ausgelegt, übereinstimmendes beobachtbares Verhalten in Kontexten zu gewährleisten, in denen die Prozesse laufen.

#Logische Beziehung für deadlock-sensitive Noninterference

Die logische Beziehung, die wir für DSNI entwickeln, umfasst Evaluierungskontexte, die es uns ermöglichen, zu analysieren, wie Prozesse in verschiedenen Setups interagieren. Diese Untersuchung ist entscheidend, da sie sich auf die beobachtbaren Nachrichten konzentriert, die über Schnittstellen ausgetauscht werden, und diejenigen herausfiltert, die nicht beobachtbar sind.

Die Terminterpretation der Beziehung definiert Paare von Prozessen, die eng miteinander verwandt sind, basierend auf den Nachrichten, die sie senden und empfangen. Die Werteinterpretation konzentriert sich darauf, wie diese Prozesse Nachrichten über ihre beobachtbaren Schnittstellen behandeln, was es uns ermöglicht, ihr Verhalten effektiv zu überprüfen.

#Definition der beobachtbaren Äquivalenz

Beobachtbare Äquivalenz bestimmt, wie zwei Prozesse in Bezug auf die Nachrichten, die von einem Angreifer beobachtet werden können, agieren. Dieser Angreifer kann Kommunikationen beobachten und diese Informationen nutzen, um Rückschlüsse auf die im Netzwerk laufenden Prozesse zu ziehen.

Um als äquivalent betrachtet zu werden, müssen zwei Prozesse die gleichen beobachtbaren Verhaltensweisen aufweisen – das bedeutet, ein Angreifer, der die relevanten Kanäle überwacht, könnte sie nicht anhand der Informationen, die ihm zugänglich sind, unterscheiden.

#Nachweis des Hauptergebnisses: Gut getypte Prozesse implizieren DSNI

Um zu zeigen, dass gut getypte Prozesse DSNI implizieren, definieren wir zunächst die beobachtbare Äquivalenz und verbinden sie dann mit unserem grundlegenden Theorem. Das Theorem besagt, dass so lange zwei Prozesse beobachtbar äquivalent sind, sie hinsichtlich der Sicherheitsmerkmale der Informationen, die durch ihre Kanäle fliessen, identisch agieren werden.

#Technische Herausforderungen

Bei der Etablierung der Beziehung und dem Nachweis unserer Ergebnisse treten mehrere Herausforderungen auf. Dazu gehört, dass die ordnungsgemässe Handhabung asynchroner Kommunikationen sichergestellt wird, bei denen Ausgaben keine Fortsetzungen haben, dass gewährleistet wird, dass Deadlocks keine Informationen leaken, und dass die strukturelle Kongruenz aufrechterhalten wird, die notwendig ist, um unsere Theoreme zu beweisen.

Die logische Beziehung muss auch mit Fällen umgehen, in denen Nachrichten mit beobachtbaren und nicht beobachtbaren Kanälen verbunden sind. Die Fähigkeit, zu verfolgen, wie Informationen durch diese Kanäle fliessen, ist entscheidend für die Aufrechterhaltung der Integrität des logischen Rahmens, den wir etabliert haben.

#Fazit

Zusammenfassend legt dieser Artikel die Grundlage für eine neue Methode zur Gewährleistung der Kontrolle des Informationsflusses in nachrichtenbasierten Systemen, die realistischere Strukturen wie zyklische Prozessnetzwerke zulassen. Durch die Kombination von Sitzungstypen mit IFC und den Nachweis von Nichtinterferenz durch logische Beziehungen können wir die Sicherheit und den Schutz der Informationen, die in parallelen Programmen ausgetauscht werden, erhöhen.

Zukünftige Arbeiten werden untersuchen, wie komplexere Merkmale wie Rekursion und Nichtdeterminismus integriert werden können, während die Sicherheitsgarantien, die wir hier etabliert haben, aufrechterhalten werden. Die Interaktionen zwischen diesen Merkmalen und unseren bestehenden Rahmenwerken werden entscheidend sein, um ein umfassenderes Verständnis des sicheren Informationsflusses in modernen Rechensystemen zu entwickeln.