User-Controlled Privacy: Taint, Track, and Control
Authors: François Hublet (ETH Zürich), David Basin (ETH Zürich), Srđan Krstić (ETH Zürich)
Volume: 2024
Issue: 1
Pages: 597–616
DOI: https://doi.org/10.56553/popets-2024-0034
Abstract: We develop the first language-based, Privacy by Design approach that provides support for a rich class of privacy policies. The policies are user-defined, rather than programmer-defined, and support fine-grained information flow restrictions (considering individual application inputs and outputs) with temporal constraints. Our approach, called Taint, Track, and Control (TTC), combines dynamic information-flow control and runtime verification to enforce these policies in the presence of malicious users and developers.
We provide TTC's semantics and proofs of its correct enforcement, formalized in the Isabelle/HOL proof assistant. We also implement our approach in a web development framework and port three baseline applications from previous work into this framework for evaluation. Overall, our approach enforces expressive user-defined privacy policies with practical runtime performance.
Keywords: privacy by default, information-flow control, web development, temporal logic
Copyright in PoPETs articles are held by their authors. This article is published under a Creative Commons Attribution 4.0 license.
