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 Informationsflusskontrolle (IFC) für nebenläufige Programme und mobile Komponenten. Die Analyse basiert auf Programmabhängigkeitsgraphen (PDGs), dynamischen Pushdown-Netzwerken, und fixpunktbasierter Invariantenerzeugung; sie ist flusssensitiv, kontextsensitiv, objektsensitiv, zeitsensitiv und locksensitiv. In der ersten Projektphase wurde eine PDG-basierte IFC-Analyse für Java-Softwarekomponenten entwickelt. Die Präzision der Analyse wurde durch dynamische Pushdown-Netzwerke erhöht. Ferner wurde ein neuer Algorithmus zur IFC-Analyse nebenläufiger Programme gefunden, der die erste PDG-basierte Analyse für Low-Security Observational Determinism (LSOD) für volles Java darstellt. In der zweiten Projektphase wird der Plug-In Mechanismus für mobile Komponenten fertiggestellt, Unterstützung für Sicherheit im Großen wird angeboten, die Skalierbarkeit und die Präzision der Analyse wird evaluiert und erhöht, Deklassifikation wird besser unterstützt und die vollständige Analyse integriert. Das Verfahren wird auf die RS3 Referenzszenarios ``Software for mobile devices'' und ``E-Voting'' angewendet, um Nichtinterferenz nebenläufiger Programme zu prüfen. 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.