ECOOP 2025
Mon 30 June - Fri 4 July 2025 Bergen, Norway
Tue 1 Jul 2025 12:09 - 12:30 at Auditorium M003 - Type Systems and Program Semantics Chair(s): Sukyoung Ryu

Many important security properties can be formulated in terms of flows of tainted data, and improved taint analysis tools to prevent such flows are of critical need. Most existing taint analyses use whole-program static analysis, leading to scalability challenges. Type-based checking is a promising alternative, as it enables modular and incremental checking for fast performance. However, type-based approaches have not been widely adopted in practice, due to challenges with false positives and annotating existing codebases. In this paper, we present a new approach to type-based checking of taint properties that addresses these challenges, based on two key techniques. First, we present a new type-based tainting checker with significantly reduced false positives, via more practical handling of third-party libraries and other language constructs. Second, we present a novel technique to automatically infer tainting type qualifiers for existing code. Our technique supports inference of generic type argument annotations, crucial for tainting properties. We implemented our techniques in a tool TaintTyper and evaluated it on real-world benchmarks. TaintTyper exceeds the recall of a state-of-the-art whole-program taint analyzer, with comparable precision, and 2.93X–22.9X faster checking time. Further, TaintTyper infers annotations comparable to those written by hand, suitable for insertion into source code. TaintTyper is a promising new approach to efficient and practical taint checking.

Tue 1 Jul

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

10:45 - 12:30
Type Systems and Program SemanticsTechnical Papers at Auditorium M003
Chair(s): Sukyoung Ryu KAIST
10:45
21m
Talk
Mono Types — First-Class Containers for Datalog
Technical Papers
Runqing Xu JGU Mainz, David Klopp JGU Mainz, Sebastian Erdweg JGU Mainz
11:06
21m
Talk
Monadic type-and-effect soundness
Technical Papers
Francesco Dagnino University of Genoa, Paola Giannini University of Eastern Piedmont, Elena Zucca University of Genoa
11:27
21m
Talk
An Effectful Object Calculus
Technical Papers
Francesco Dagnino University of Genoa, Paola Giannini University of Eastern Piedmont, Elena Zucca University of Genoa
11:48
21m
Talk
Compositional Bug Detection for Internally Unsafe Libraries: A Logical Approach to Type Unsoundness
Technical Papers
Pedro Carrott Imperial College London, Sacha-Élie Ayoun Imperial College London, Azalea Raad Imperial College London
DOI
12:09
21m
Talk
Practical Type-Based Taint Checking and InferenceRemote
Technical Papers
Nima Karimipour University of California, Riverside, Kanak Das University of California, Riverside, Manu Sridharan University of California at Riverside, Behnaz Hassanshahi Oracle Labs, Australia
:
:
:
: