SPP 1496 - Teilprojekt: Informationsflusskontrolle für mobile Komponenten mittels präziser Analyse paralleler Programme (IFC for Mobile Components)

Grunddaten zu diesem Projekt

Beschreibung

Wir entwickeln eine hochpräzise Analyse zur Informationflusskontrolle (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 Nichtinterferenzbegriff 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". Das Projekt wird in Kooperation mit der Gruppe von Prof. Gregor Snelting from Karlsruhe Institute of Technology (KIT) durchgeführt und ist ein Teilprojekt des Schwerpunktprogramms 1496, "Reliably Secure Software Systems - RS3 (Zuverlässig sichere Softwaresysteme", das durch die DFG (Deutsche Forschungsgemeinschaft) gefördert wird.