Privacy Assessment of Software Architectures based on Static Taint Analysis

TL;DR

This paper introduces a formal, static taint analysis-based method for assessing privacy properties in software architectures, aiding in privacy compliance verification and uncovering hidden violations.

Contribution

It formalizes privacy assessment using static taint analysis integrated into a verification framework, with proven soundness and real-world applicability.

Findings

Uncovered previously unknown privacy violations in case studies.

Demonstrated equivalence to traditional information flow security.

Validated the approach's effectiveness in real-world scenarios.

Abstract

Privacy analysis is critical but also a time-consuming and tedious task. We present a formalization which eases designing and auditing high-level privacy properties of software architectures. It is incorporated into a larger policy analysis and verification framework and enables the assessment of commonly accepted data protection goals of privacy. The formalization is based on static taint analysis and makes flow and processing of privacy-critical data explicit, globally as well as on the level of individual data subjects. Formally, we show equivalence to traditional label-based information flow security and prove overall soundness of our tool with Isabelle/HOL. We demonstrate applicability in two real-world case studies, thereby uncovering previously unknown violations of privacy constraints in the analyzed software architectures.