@InProceedings{LanzingerUlbrichWeigl2022,
author = {Florian Lanzinger and
Mattias Ulbrich and
Alexander Weigl},
editor = {Tiziana Margaria and
Bernhard Steffen},
title = {A Refactoring for Data Minimisation Using Formal
Verification},
booktitle = {11th International Symposium on Leveraging Applications of
Formal Methods, Verification and Validation. Software
Engineering ({ISoLA} 2022)},
month = oct,
year = {2022},
publisher = {Springer Nature Switzerland},
address = {Cham},
pages = {345--364},
abstract = {Concerns about protecting private user data grow as
automated data processing by software becomes more
ubiquitous in our society. One important principle
is data minimisation, which requires that all collected
personal data must be limited to what is necessary for the
respective declared purpose. For existing software systems,
it can be difficult to determine which input data are
indeed necessary to compute the result and which data can
(in certain cases) be left out. We present a new approach
that can be used to adapt an existing program to data
minimisation requirements. In this framework a user
transmits a set of facts about their data instead of the
full data. We formally define the approach and introduce a
variety of minimisation notions for it. We have implemented
the approach and demonstrate its feasibility on a few
selected examples.},
isbn = {978-3-031-19756-7},
doi = {10.1007/978-3-031-19756-7_19},
url = {https://doi.org/10.1007/978-3-031-19756-7_19}
}
A Refactoring for Data Minimisation Using Formal Verification
| Author(s): | Florian Lanzinger, Mattias Ulbrich, and Alexander Weigl |
|---|---|
| In: | 11th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation. Software Engineering (ISoLA 2022) |
| Publisher: | Springer Nature Switzerland |
| Year: | 2022 |
| Pages: | 345-364 |
| PDF: | |
| URL: | https://doi.org/10.1007/978-3-031-19756-7_19 |
| DOI: | 10.1007/978-3-031-19756-7_19 |
| Links: | The final publication is available at Springer. |
Abstract
Concerns about protecting private user data grow as automated data processing by software becomes more ubiquitous in our society. One important principle is data minimisation, which requires that all collected personal data must be limited to what is necessary for the respective declared purpose. For existing software systems, it can be difficult to determine which input data are indeed necessary to compute the result and which data can (in certain cases) be left out. We present a new approach that can be used to adapt an existing program to data minimisation requirements. In this framework a user transmits a set of facts about their data instead of the full data. We formally define the approach and introduce a variety of minimisation notions for it. We have implemented the approach and demonstrate its feasibility on a few selected examples.