Enforcing and analysing programming guidelines for secure web programming with type systems

• Applicant: Dr. Ulrich Schöpp
• Subject Area: Software Engineering and Programming Languages ; Theoretical Computer Science
• Term: from 2014 to 2023
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 250888164

• Final Report Year: 2023

Final Report Abstract

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.

Publications

• 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