Durchsetzung und Analyse von Programmierrichtlinien für sichere Web-Programmierung mit Typsystemen

• Antragsteller: Dr. Ulrich Schöpp
• Fachliche Zuordnung: Softwaretechnik und Programmiersprachen ; Theoretische Informatik
• Förderung: Förderung von 2014 bis 2023
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 250888164

• Erstellungsjahr: 2023

Zusammenfassung der Projektergebnisse

Security is becoming increasingly important for software development. Almost all software is exposed to security threats of some form. One measure for addressing this issue is to require that software development follows secure programming guidelines and security best practices. The GuideForce project developed an automatic static analysis method for the Java programming language for enforcing programming guidelines during development. The basis was a type-based approach to the static analysis of Java programs from the predecessor project. The project improved the expressive power of existing type systems, simplified and modularized the approach, and developed the meta-theory. The theoretical results were implemented in the form of Java bytecode analysis software. The main results of the project are: • a type-based static analysis method for Featherweight Java that can analyze properties of finite and infinite execution traces, with its associated meta-theory; • a generic type system for region and effect typing for Featherweight Java that allows us to establish the soundness of various region type regimes in a uniform way. Its instances include previous region type systems, as well as new instances that capture more precise analyses of trace-based properties; • a new approach to implementing region typing by abstracting Java program code into environment transformations, which avoids repeated analysis of the same code and allows more efficient type checking; • an implementation of the theoretical results for automatic static analysis of Java bytecode. The results were published in the proceedings of international conferences and workshops. The software, which is referenced in the publications, is available as open source.

Projektbezogene Publikationen (Auswahl)

• Type-based Enforcement of Infinitary Trace Properties for Java (CCC 2020). In Continuity, Computability, Constructivity – From Logic to Algorithms, Faro (Portugal), August 31 – September 4, 2020
  Erbatur, Serdar; Schöpp, Ulrich & Xu, Chuangjie
  
• A generic type system for featherweight Java. Proceedings of the 23rd ACM International Workshop on Formal Techniques for Java-like Programs (2021, 7, 11), 9-15. ACM.
  Schöpp, Ulrich & Xu, Chuangjie
  
• Type-based Enforcement of Infinitary Trace Properties for Java. 23rd International Symposium on Principles and Practice of Declarative Programming, 51(2021, 9, 6), 1-14. ACM.
  Erbatur, Serdar; Schöpp, Ulrich & Xu, Chuangjie
  
• Inferring Region Types via an Abstract Notion of Environment Transformation. Lecture Notes in Computer Science (2022), 45-64. Springer Nature Switzerland.
  Schöpp, Ulrich & Xu, Chuangjie
  
• Type Inference via Symbolic Environment Transformations. In 28th International Conference on Types for Proofs and Programs (TYPES 2022), Nantes, 2022
  Schöpp, Ulrich & Xu, Chuangjie