Information Flow Control for Mobile Components Based on Precise Analysis for Parallel Programs

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

Wir entwickeln eine hochpräzise Analyse zur Informationsflusskontrolle (IFC) für verteilte, nebenläufige Programme und mobile Komponenten. Die Analyse basiert auf Programmabhängigkeitsgraphen (PDGs), dynamischen Pushdown-Netzwerken, und Inferenz von Invarianten; sie ist flusssensitiv, kontextsensitiv, objektsensitiv, zeitsensitiv und locksensitiv. In Phase 1 und 2 wurde eine kompositionale, PDG-basierte IFC-Analyse für nebenläufige Java-Softwarekomponenten und Android Apps entwickelt. Die Präzision der Analyse wurde durch Analysen basierend auf dynamischen Pushdown-Netzwerken erhöht und wir sind auf gutem Wege, sie durch Invarianten-Inferenz weiter zu verbessern. Es wurde ein neuer ``RLSOD'' Algorithmus gefunden, der probabilistische Nichtinterferenz für volles Java garantiert und Probleme früherer LSOD Ansätze vermeidet. RLSOD ist in das am Lehrstuhl Snelting entwickelte JOANA System integriert, das in vielen RS3 Projekten verwendet wird. In Phase 3 wird RLSOD für verteilte Systeme mit Message Passing erweitert. Message Passing stellt ganz neue Probleme, die in der Literatur nur ansatzweise gelöst sind. Ein adäquater Nichtinterferenzbegriffs für verteilte Systeme wird entwickelt; ein entsprechender Algorithmus wird in JOANA integriert. Zur Erhöhung der Präzision wird das neue Verfahren des ``Data Flow Slicing'' entwickelt, das PDGs mit Invarianteninferenz in neuartiger Weise koppelt. Ferner wird JOANA in diverse RS3-Szenarien integriert, z.B. den ``Secure App Store''.