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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Code & Models
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
