A Refactoring for Data Minimisation Using Formal Verification

Reviewed Paper In Proceedings

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:
DOI:10.1007/978-3-031-19756-7_19
Links:

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.

BibTeX

@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}
}