Tool Support of Formal Methods for Privacy by Design
Sibylle Schupp




Tool Support of Formal Methods for Privacy by Design
    Sibylle Schupp
    
====================================================


Formal methods are, in principle, suited for supporting  the recent
paradigm of privacy by design, but no overview is available 
that summarizes which particular approaches have been investigated, 
for which application domains they are suited, and whether they are 
implemented and available as tools. 
Using the techniques of search-based literature review and snowballing
this paper answers those questions for a selected set of research papers. 




§ INTRODUCTION

Whenever privacy regulations for software applications are formulated, they aim 
at making privacy an integral part of software development—a well-known 
slogan is “privacy by design”, coined by 
Ann Cavoukian <cit.>.
When private data is considered even critical, application developers might 
have to provide provable guarantees for respecting or implementing particular 
privacy concerns.  
Formal methods are, in principle, suited for supporting privacy by design, 
but no overview is available that summarizes which particular methods are 
“best practice”, or in use at all. 
The literature itself is spread and can be found not only in venues for 
applied formal methods, but also in conferences on software engineering, 
security, data management, or theory.

In this paper we provide a review of the current state of formal methods 
that may aid software development for privacy concerns. For each paper in a
selected list of papers we answer three questions:


  Q1. Which particular formal method is presented?

  Q2. In which application areas is this method applied and evaluated? 

  Q3. Which tool—existing or newly developed—implements the            presented approach? 


While the research area is certainly in flux, it is important to know for 
application developers as well as for judges or legal advisers whether obvious 
candidates of formal methods exist that either suggest some kind of “state of 
the art” or, conversely, render the use of particular other methods as 
negligent. 
This review can also be helpful for prospective researchers in the field, as 
there are only few conferences and journals dedicated to privacy, and 
formal-method papers are not necessarily published there. 

For selecting a set of primary studies, we employ the so-called hybrid 
approach, a method for systematic literature reviews 
that originates in software engineering. The hybrid approach consists of two stages, where 
stage 1 conducts a systematic search to obtain an initial list (<cit.>) and stage 2, called snowballing (<cit.>),
traces the forward and backward references to and from that initial list. 
We explain the paper selection process in Section <ref>; 
in this section we also detail how we pre-process the primary studies by
annotating them with sets of tags. 
The results themselves are presented in Section <ref>. 
Section <ref> discusses threats to their
validity and Section <ref> concludes. 



§ SELECTION AND TAGGING

In this section, we describe how the set of primary studies is 
constructed and how we pre-process those studies  by tagging them.




 §.§ Selection

Following the hybrid approach for paper selection, we perform first a
search, then a snowballing step; for an overview, see 
Figure <ref>. 



In the search stage, we feed the search term (see Table <ref>) 
to a search engine, Google scholar, and apply to the resulting hit list
a series of exclusion and inclusion criteria to filter out distractors. 
Those criteria correspond to common criteria for literature reviews (see
Table <ref> in the appendix). Applying the criteria
 reduces the list from originally 131 papers to 17 papers. 
Those papers form the initial list, which serves as input to stage 2. 







Stage 2 commences with backward snowballing, using the exclusion, inclusion, 
and white-listing criteria from before (see Table <ref>). 
For each paper in the initial set, we go through its references and apply 
all exclusion criteria; on the remaining references we apply the white-list 
criteria to obtain a temporary list. 
Each reference on the white list, next, is then manually checked for each 
inclusion criterion  and, in the positive case, added to our list of primary 
studies. 
Forward snowballing proceeds similarly.  Using Google Scholar again,
we determine for each paper in the initial set all papers it is cited by. 
For each citing paper we repeat the process employed for backward snowballing, 
i.e., apply the exclusion criteria and the white-list criteria, and check 
by hand the remaining papers for topicality and availability according 
to the inclusion criteria. 

Table <ref> provides the results. Altogether 57 additional papers can 
be obtained through backward snowballing and another 27 papers by forward 
snowballing.
For each paper in the initial set we list  the number of its
references (“refs”) for backward snowballing and citations (“cited”) for 
forward snowballing,  the number of potentially 
relevant papers (“inc?”) after white-listing, and the number of actually 
relevant (“inc!”) papers after the inclusion check.  
The last number refers to the papers that extend the initial set.

We note that the sum over those papers (row “Sum”) is significantly larger
than the number of actually added papers (row “Addit. papers”). This is no 
mistake but implies that some papers are cited multiple times. 
Multiple citations are a positive sign for the purpose of a review as they 
signify that a paper has a certain weight in the research discussion. 
We also note that the citation numbers (column “cited”) are comparatively low.
The reason is that  the papers in the initial set are all very recent: 
8 (of the 17) papers have been published 2016 or later, and the remaining
ones date back to not later than 2011.

Altogether, this review is based on a set of 101 primary studies. 





 §.§ Tagging

With each of the three questions Q1-Q3 we associate a number of tags that are
used to answer that question. In each case, we introduce three kinds of tags. 
The first kind of tags is formed by  all related terms that are highlighted by 
the authors themselves, because they use them in the title, abstract, or 
keyword list of their paper.
Apart from minor grammatical changes, those terms are taken verbatim from
the papers and directly serve as tags. As it turns out, however, very little 
of the information relevant for our review questions is directly exposed in the title, abstract, or keyword list. We therefore read cursory through each paper and extend the list of tags by the terms found thereby. Those terms also form tags directly. 
The third kind of tags are meta-tags, which we introduce to make 
the absence of information explicit, to further classify papers, and 
to group tags; those latter tags are prefixed with “meta-”. 
Table <ref> contains the complete set of tags, ordered by 
associated question; all meta-tags
are listed in the last row. 








§ RESULTS

We are now ready to present the findings. For each question Q1-Q3 we first 
explain how we aggregate the extracted tags, and then report the results in 
a bar chart, which tallies related papers and provides a numerical overview, 
and a table, which lists all related references explicitly. 



 §.§ Q1: Formal methods

Since the number of tags associated with question Q1 totals 101 
(Table <ref>), we need to group those tags as otherwise the 
presentation would become too fragmented. 
Table <ref> lists our partitioning into 13 groups where 
the group “Other” contains those tags that do not fit in any other cluster.
With the partitioning we intend to capture the view of the formal methods 
community, but our choice cannot be  free from subjectivity. 
Nor is the annotation process itself, which associates a paper with particular 
tags in the first place. 
We therefore decided to make our tagging transparent by publishing the 
bibliographic source file. Possible additional validity problems 
we discuss later, 
in Section <ref>.






Figure <ref> reports the numbers for each group of formal methods,
sorted alphabetically, while Table <ref> lists for each 
group, or approach, of formal methods the papers that follow that approach. 
Interpreting the results from a practitioner's point of view, 
no obviously preferred formal method exists. 
Even the high numbers in the group “Logic” do not change the picture, as, 
upon  closer look,  the particular logics in this group vary greatly in 
their syntax, semantics, and pragmatics. 
Our second observation concerns the group “Formal Model.” Papers on formal 
methods often present their method directly since they can assume appropriate 
underlying formal representations (“models”).
For the domain of privacy, however, it is apparently  a research effort of 
its own to provide a formal model, and more than 40% of the papers
is engaged in the some part of formalization. 









 §.§ Q2. Application domains

For presenting the targeted application domains we, again, we partition the 
corresponding tags. In this case, we partition 38 tags 
(see Table <ref>) 
in 9 groups, using the corresponding application domain as grouping criterion 
(see Table <ref>). 
Most group memberships are easy to decide syntactically and the application 
domains are largely as expected (see, e.g., the groups “E-Commerce”, 
“Health”, “Smart Grid”). 



The majority of the papers include examples mostly for the purpose of 
illustrating a theoretical point. Two important tags are therefore the 
meta-tags “example-extended” and “experimental”, which flag extended, 
(and ideally) realistic examples and empirical measurements, thus mark 
those papers that are of particular interest to application developers.



Again, we answer the question by providing a bar chart and a table: 
Figure <ref>  shows the distribution of papers
across application domains as well as the distribution of papers containing
extended examples or experimental data. Conversely, Table <ref> 
lists for each application domain the papers that relate to it. 

Comparing the numbers in Figure <ref>, one can see 
two application domains with higher numbers: “Health” and “Social Networks.” 
Looking closer at the numbers of  “extended examples” or 
“extended + empirical”, the domain “Health” clearly exhibits the largest
number of papers of practical relevance. 
Overall, however, the ratio of papers with extended examples is very low, 
amounting to less than a fifth. 
At the same time, the dominating number in the figure is the number 
of papers without examples beyond illustrative snippets (“No-app”), 
just a bit more than a fifth.
Altogether, it is fair to say that—with the possible exception of the health domain—current formal approaches cannot yet refer to many showcases. 
Accordingly, experimental evaluations—as they matter for practical
software development—are scarce: only 9 papers
contain experimental data and only two papers contain both an extended example
and its empirical evaluation.  The bar “No-app” includes additional two 
papers with experimental data: those papers measure
performance parameters of the presented tool rather than  an application.

For a legal advisor those numbers imply that there are no “best” formal
methods  one can application developers expect to follow; the only domain 
where it is sensible at all to ask for best practices is the health-care 
domain.  For application developers those numbers mean that, at present, there
is little software to reuse. 









 §.§ Q3. Tool support

The last question concerns the tool a paper either uses to implement its 
approach or newly develops for that purpose. 
Figure <ref> summarizes the current tool support
by breaking the set of tools down in three categories: unnamed tools, coming
from papers that devise a prototypical implementation; (named) tools that are
used either in one paper only or, if cited multiple times, by the same research
group; and, lastly, tools that are used by different research groups. 
As forth category, we include those papers that mention no tool. 
In Table <ref> we list which tool implements which approach.

The results are perhaps unexpected. For one, one might expect the
overall number of tools to be higher—after all the primary studies 
are authored by software engineers or computer scientists. Yet, almost half 
of the studies is purely theoretical in that sense (“No tool” in 
Figure <ref>). 
The spreading of tools, second, is very large: only four tools are used in 
more than one paper (see Table <ref>). 
Generally, such spreading of tools is quite common for formal methods and can 
be seen elsewhere as well. 
For the case at hand, high numbers follow already from the variety of formal 
methods used and the variety within those groups: the group “Logic”, for 
example comprises a wide range of logics, for which no single tool exists. 
Still, it is remarkable that there is only one tool in our primary studies,
Alloy, that is used by  more than one research group. 









§ THREATS TO VALIDITY


The results of
this review depend critically on the tags each paper is characterized by,
but the process of tagging is done manually, and this presents a threat
to the validity of the results. In this subsection we first explain how we
address this threat, then discuss additional potential validity problems. 
 
Unfortunately, tagging by hand is inevitable—the majority of
relevant information is not directly exposed to the readers but “hidden”
in the text. We double-checked so that we can ensure that the set of tags for terms that 
the authors themselves consider relevant (by including them in the title, 
abstract, or keyword list of their paper) is complete. 
Given the number of papers processed, however, we 
cannot dismiss the risk of having overlooked tags 
that emerge from cursory reading. Nor can we give a formal argument for
our specific partitioning of tags. 
The best we can do for mitigating validity problems is to make
our groupings transparent. We do so through the introduction
of appropriate meta-tags, and store with each paper its associated
meta-tags. 

The second source of threats to the overall validity concerns the selection 
process. A different search term as well as a different search engine would 
lead to a different initial list, while an additional 
iteration of the snowballing step would lead to
an extended list of primary studies. On the other hand, research for formal
methods on privacy has started only and we look at the references in this
review  as a starting point only, for a list that  needs to be extended as 
research moves on. We do not dispute that relevant papers might be missing
in the current review but we are confident that, using the technique of 
snowballing, one ultimately reaches all relevant papers. 


While it will not be possible to exclude all mistakes and subjective 
assessments, we can at least ensure the full reproducibility of the results
and therefore make the complete data set available: the bibtex information
 for the primary
studies can be downloaded as three separate files[<https://www.tuhh.de/sts/research/data-protection-machine -learning/initial17.bib> (<include-forward.bib>, <include-backward.bib>)]; all tags and meta-tags can be found
in the field “keywords.” 
The files were generated using the open-source software Zotero for reference 
management <cit.>, which allows for various filters and conversions 
to spreadsheet and bibtex formats, and which was of great help in automating 
the evaluation.  



§ SUMMARY AND CONCLUSION


Since personal data can be considered critical information,  
application developers may want to employ formals methods so that
they can argue in a rigorous manner that private data is protected properly. 
At present, however, no dedicated venues
exist where formal methods are discussed  that target specifically privacy 
concerns. Instead, the literature is scattered over conferences for
formal methods, software engineering, security, data management, or theoretical computer
science. In this paper we provide a systematic review of the use of
formal methods for privacy protection in practice.


 A wide variety of methods is available already today, and there
is no evidence for more, or less, suitable methods. Notably, a large 
portion of papers falls in the categories “Formal Model” and “Language”: 
since privacy regulations are provided in natural language, extra modeling 
efforts are needed. 
On the other hand, comparatively few examples are available that application 
developers could take as a blueprint. Also, about half of the papers do not 
present an implementation of their approach and, generally, dedicated tool 
support is in its infancy. 

Concluding, privacy protection is an important topic where formal methods
can contribute in significant ways. As the publication years of the primary 
studies show, research in this field has gained momentum. 
As the review also shows, tooling support is a worthwhile subject for 
further research. 



  
Acknowledgment
My sincere thanks are to Wolfgang Schulz, Max von Grafenstein,
 Jörg Pohle, and the Humboldt Institute for Internet 
and Society (HIIG) for feedback and discussions on the legal issues of privacy. 
I also owe to the participants of the Dagstuhl seminar 18471, "Next Generation Domain Specific Conceptual Modeling: Principles and Methods",
and to the Dagstuhl library for granting access to all literature
needed for this review. 

The paper is part of the project “Information Governance Technologies: Ethics, Policies, Architectures, Engineering” funded by the “Landesforschungsförderung Hamburg.”







plain

