Code injection and cross-site scripting belong to the most common security vulnerabilities in modern software, usually caused by incorrect string processing. These exploits are often addressed by formulating programming guidelines or “best practices”.
In this paper, we study the concrete example of a guideline used at SAP for the handling of untrusted, potentially executable strings that are embedded in the output of a Java servlet. To verify adherence to the guideline, we present a type system for a Java-like language that is extended with refined string types, output effects, and polymorphic method types.
The practical suitability of the system is demonstrated by an implementation of a corresponding string type verifier and context-sensitive inference for real Java programs.