Fundierung und Sicherheitsanalyse verteilter, asynchroner Objektsysteme

点击翻译按钮获取中文摘要

Die enormen Chancen, die sich dem verteilten Rechnen durch das Internet als Kommunikationsmedium bieten, können nur genutzt werden, wenn den physikalischen und technischen Vorgaben eines weit-verteilten Computernetzes entsprochen werden kann. Global ablaufende Kommunikationsvorgänge zwischen asynchronen Aktivitäten führen zu nicht-vorhersagbaren Kommunikationszeiten; Codeverteilung auf getrennte Adressräume bedingt verborgene lokale Zustände paralleler Aktivitäten; die resultierenden Zugriffskonflikte und komplexen Aufrufstrukturen erfordern spezielle Auflösungskonzepte. Das Paradigma der Objektorientierung kommt solchen Konzepten entgegen. Objekte sind asynchron agierende Entitäten mit lokalem Zustand. Sie kommunizieren über Methodenaufrufe mit typisierbaren Schnittstellen. Dies bietet den Vorteil, dass Code-Verifikation und Prüfung des Kommunikationsvorgangs gemeinsam im Rahmen einer statischen Analyse ermöglicht werden. Ziel des Projektes ist es das Programmierparadigma der verteilten, aktiven Objekte auf Grundlage einer Isabelle/HOL-Formalisierung zu modellieren und die sicherheitsrelevanten Eigenschaften zu beweisen. Als Basiskalkül für verteilte, asynchrone, aktive Objekte verwenden wir ASP mit seiner Java-basierten Programmierumgebung ProActive. Sicherheitskritisch sind zum einen Kommunikationskonstrukte wie Futures, die zu nicht-terminierendem Verhalten führen können. Durch statische Analyse mit Hilfe eines Typecheckers können riskante Aufrufstrukturen entdeckt werden. Passende Typchecker können aus dem Isabelle/HOL-Modell gewonnen werden. Um weitere Sicherheitsrisiken zu vermeiden sollen die Eindeutigkeit der parallelen Evaluation (Konfluenz) und die Abwesenheit verdeckter Kanäle (Non-Interference) nachgewiesen werden.