Enforcing Programming Guidelines with Region Types and Effects
This work addresses security vulnerabilities in web programming for Java developers, but it is incremental as it builds upon an existing region and effect system.
The authors tackled the problem of ensuring secure web programming in Java by developing a new type and effect system that enforces arbitrary guidelines, achieving verification on benchmarks including large parts of the Stanford SecuriBench.
We present in this paper a new type and effect system for Java which can be used to ensure adherence to guidelines for secure web programming. The system is based on the region and effect system by Beringer, Grabowski, and Hofmann. It improves upon it by being parametrized over an arbitrary guideline supplied in the form of a finite monoid or automaton and a type annotation or mockup code for external methods. Furthermore, we add a powerful type inference based on precise interprocedural analysis and provide an implementation in the Soot framework which has been tested on a number of benchmarks including large parts of the Stanford SecuriBench.