Verifikation polymorpher Nichtinterferenz für mobile Software - PolyNi

• Antragsteller: Professor Dr. Martin Hofmann, seit 9/2010 (†)
• Fachliche Zuordnung: Softwaretechnik und Programmiersprachen
• Förderung: Förderung von 2010 bis 2015
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 157355546

• Erstellungsjahr: 2013

Zusammenfassung der Projektergebnisse

Im Projekt PolyNI wurden typtheoretische Analysen zur Erhöhung der Sicherheit webbasierter und mobiler Software entwickelt und die Grundlagen solcher typbasierten Analysen weiterentwickelt. Im einzelnen entstanden: • ein System zur Durchsetzung dynamisch konfigurierbarer Informationsflusspolitiken in mobilen Anwendungen, • eine typbasierte Analyse zur korrekten Verwendung eines Frameworks für die sichere Verarbeitung von Benutzereingaben, • ein generisches Typsystem für Java-artige Sprachen, welches mehrere moderne Analysetechniken vereinigt. Im Rahmen der Projektarbeit entstanden Kooperationen mit SAP und der Universität Edinburgh, die zu entsprechenden Folgearbeiten führen werden.

Projektbezogene Publikationen (Auswahl)

• Noninterference with dynamic security domains and policies. In Anupam Datta, editor, ASIAN, volume 5913 of Lecture Notes in Computer Science, pages 54–68. Springer, 2009
  Robert Grabowski and Lennart Beringer
  
• Verifying pointer and string analyses with region type systems. In Edmund M. Clarke and Andrei Voronkov, editors, LPAR (Dakar), volume 6355 of Lecture Notes in Computer Science, pages 82–102. Springer, 2010
  Lennart Beringer, Robert Grabowski, and Martin Hofmann
  
• Type-based enforcement of secure programming guidelines - code injection prevention at SAP. In Gilles Barthe, Anupam Datta, and Sandro Etalle, editors, Formal Aspects in Security and Trust, volume 7140 of Lecture Notes in Computer Science, pages 182–197. Springer, 2011
  Robert Grabowski, Martin Hofmann, and Keqin Li
  
• Information Flow Analysis for Mobile Code in Dynamic Security Environments. PhD thesis, Ludwig-Maximilians-Universität München, 2012
  Robert Grabowski
  
• Verifying pointer and string analyses with region type systems. Computer Languages, Systems & Structures, 39(2):49–65, 2013
  Lennart Beringer, Robert Grabowski, and Martin Hofmann