Enforcing Programming Guidelines with Region Types and Effects

TL;DR

This paper introduces a new Java type and effect system that enforces secure web programming guidelines by leveraging region types, effects, and a flexible, automaton-based specification, with an advanced type inference and practical implementation.

Contribution

It extends existing region and effect systems with guideline parametrization, interprocedural type inference, and a Soot-based implementation tested on real benchmarks.

Findings

Successfully enforced security guidelines on large benchmarks

Achieved precise interprocedural type inference

Demonstrated practical applicability in Java security

Abstract

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.