Type-based enforcement of secure programming guidelines


By following secure programming guidelines, programmers can avoid common mistakes that may lead to security problems in their software. This project develops automated tools that help programmers to apply such guidelines correctly and consequently during software development.

Project description

Security is becoming increasingly important for software development. With the increased connectivity of modern systems, today almost all software is exposed to security threats of some form. To address this issue, expert knowledge of secure software development has been captured in the form of programming guidelines and best practices. However, such guidelines are only if effective if they are applied correctly. This project develops automatic methods for checking adherence to programming guidelines during system development. This helps developers to identify potential security issues already during development.

Research contribution

The GuideForce project develops a lightweight static analysis method for the Java programming language. It combines ideas from type systems and abstract interpretation and improves the state of the art of scalable automatic program analysis methods.

The main goals of the project are:

  • Improve the expressiveness of type-based analysis methods in order to handle a wide range of programming guidelines and to cover a large set of features of the Java programming language, such as reflection, concurrency, generic types and higher-order features.
  • Develop practical applications of the method: Capture various kinds of guidelines from different application areas, in particular security, improve the implementation in a tool and assess the practicability and scalability of the approach under real-world conditions.

Project duration

01.11.2019 - 31.12.2022


  • 2022 Inferring Region Types via an Abstract Notion of Environment Transformation Ulrich Schöpp and Chuangjie Xu In Asian Symposium on Programming Languages and Systems (APLAS 2022), volume 13658 of LNCS, pages 45–64, Springer. Details DOI BIB
  • 2021 Type-based Enforcement of Infinitary Trace Properties for Java Serdar Erbatur, Ulrich Schöpp and Chuangjie Xu In PPDP 2021: 23rd International Symposium on Principles and Practice of Declarative Programming, ACM. Details DOI BIB
  • 2021 A generic type system for featherweight Java Ulrich Schöpp and Chuangjie Xu In FTfJP 2021: Proceedings of the 23rd ACM International Workshop on Formal Techniques for Java-like Programs, pages 9–15, ACM. Details DOI BIB