%0 Conference Proceedings
%T Privacy Assessment Using Static Taint Analysis (Tool Paper)
%+ Technische Universität Munchen - Technical University Munich - Université Technique de Munich (TUM)
%A Maltitz, Marcel, Von
%A Diekmann, Cornelius
%A Carle, Georg
%< avec comité de lecture
%( Lecture Notes in Computer Science
%B 37th International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE)
%C Neuchâtel, Switzerland
%Y Ahmed Bouajjani
%Y Alexandra Silva
%I Springer International Publishing
%3 Formal Techniques for Distributed Objects, Components, and Systems
%V LNCS-10321
%P 225-235
%8 2017-06-19
%D 2017
%R 10.1007/978-3-319-60225-7_16
%Z Computer Science [cs]
%Z Computer Science [cs]/Networking and Internet Architecture [cs.NI]Conference papers
%X When developing and maintaining distributed systems, auditing privacy properties gains more and more relevance. Nevertheless, this task is lacking support of automated tools and, hence, is mostly carried out manually. We present a formal approach which enables auditors to model the flow of critical data in order to shed new light on a system and to automatically verify given privacy constraints. The formalization is incorporated into a larger policy analysis and verification framework and overall soundness is proven with Isabelle/HOL. Using this solution, it becomes possible to automatically compute architectures which follow specified privacy conditions or to input an existing architecture for verification. Our tool is evaluated in two real-world case studies, where we uncover and fix previously unknown violations of privacy.
%G English
%Z TC 6
%Z WG 6.1
%2 https://inria.hal.science/hal-01658424/document
%2 https://inria.hal.science/hal-01658424/file/446833_1_En_16_Chapter.pdf
%L hal-01658424
%U https://inria.hal.science/hal-01658424
%~ IFIP-LNCS
%~ IFIP
%~ IFIP-TC
%~ IFIP-WG
%~ IFIP-TC6
%~ IFIP-WG6-1
%~ IFIP-FORTE
%~ IFIP-LNCS-10321