License: 
Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.FSTTCS.2022.42
URN: urn:nbn:de:0030-drops-174342
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2022/17434/
Kupferman, Orna ;
Leshkowitz, Ofer
Synthesis of Privacy-Preserving Systems
Abstract
Synthesis is the automated construction of a system from its specification. In many cases, we want to maintain the privacy of the system and the environment, thus limit the information that they share with each other or with an observer of the interaction. We introduce a framework for synthesis that addresses privacy in a simple yet powerful way. Our method is based on specification formalisms that include an unknown truth value. When the system and the environment interact, they may keep the truth values of some input and output signals private, which may cause the satisfaction value of specifications to become unknown. The input to the synthesis problem contains, in addition to the specification φ, also secrets ψ_1,…,ψ_k. During the interaction, the system directs the environment which input signals should stay private. The system then realizes the specification if in all interactions, the satisfaction value of the specification φ is true, whereas the satisfaction value of the secrets ψ_1,…,ψ_k is unknown. Thus, the specification is satisfied without the secrets being revealed. We describe our framework for specifications and secrets in LTL, and extend the framework also to the multi-valued specification formalism LTL[F], which enables the specification of the quality of computations. When both the specification and secrets are in LTL[F], one can trade-off the satisfaction value of the specification with the extent to which the satisfaction values of the secrets are revealed. We show that the complexity of the problem in all settings is 2EXPTIME-complete, thus it is not harder than synthesis with no privacy requirements.
BibTeX - Entry
@InProceedings{kupferman_et_al:LIPIcs.FSTTCS.2022.42,
author = {Kupferman, Orna and Leshkowitz, Ofer},
title = {{Synthesis of Privacy-Preserving Systems}},
booktitle = {42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2022)},
pages = {42:1--42:23},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-261-7},
ISSN = {1868-8969},
year = {2022},
volume = {250},
editor = {Dawar, Anuj and Guruswami, Venkatesan},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2022/17434},
URN = {urn:nbn:de:0030-drops-174342},
doi = {10.4230/LIPIcs.FSTTCS.2022.42},
annote = {Keywords: Synthesis, Privacy, LTL, Games}
}
|
Keywords: |
|
Synthesis, Privacy, LTL, Games |
|
Collection: |
|
42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2022) |
|
Issue Date: |
|
2022 |
|
Date of publication: |
|
14.12.2022 |
