Document Open Access Logo

Synthesis of Privacy-Preserving Systems

Authors Orna Kupferman , Ofer Leshkowitz

PDF
Thumbnail PDF

File

LIPIcs.FSTTCS.2022.42.pdf
  • Filesize: 0.81 MB
  • 23 pages

Document Identifiers

Author Details

Orna Kupferman
  • The Hebrew University of Jerusalem, Israel
Ofer Leshkowitz
  • The Hebrew University of Jerusalem, Israel

Cite As Get BibTex

Orna Kupferman and Ofer Leshkowitz. Synthesis of Privacy-Preserving Systems. In 42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 250, pp. 42:1-42:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022) https://doi.org/10.4230/LIPIcs.FSTTCS.2022.42

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.

Subject Classification

ACM Subject Classification
  • Theory of computation
  • Theory of computation → Automata over infinite objects
Keywords
  • Synthesis
  • Privacy
  • LTL
  • Games

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. S. Almagor, U. Boker, and O. Kupferman. Formalizing and reasoning about quality. Journal of the ACM, 63(3):24:1-24:56, 2016. Google Scholar
  2. S. Almagor and O. Kupferman. High-quality synthesis against stochastic environments. In Proc. 25th Annual Conf. of the European Association for Computer Science Logic, volume 62 of LIPIcs, pages 28:1-28:17, 2016. Google Scholar
  3. S. Almagor, O. Kupferman, and Y. Velner. Minimizing expected cost under hard boolean constraints, with applications to quantitative synthesis. In Proc. 27th Int. Conf. on Concurrency Theory, volume 59 of LIPIcs, pages 9:1-9:15, 2016. Google Scholar
  4. C. Baier, M. Größer, M. Leucker, B. Bollig, and F. Ciesinski. Controller synthesis for probabilistic systems. In Exploring New Frontiers of Theoretical Informatics, IFIP 18th World Computer Congress, 3rd International Conference on Theoretical Computer Science, volume 155 of IFIP, pages 493-506. Kluwer/Springer, 2004. Google Scholar
  5. B. Barak, O. Goldreich, R. Impagliazzo, S. Rudich, A. Sahai, S.P. Vadhan, and K. Yang. On the (im)possibility of obfuscating programs. J. ACM, 59(2):6:1-6:48, 2012. Google Scholar
  6. R. Berthon, S. Guha, and J-F Raskin. Mixing probabilistic and non-probabilistic objectives in markov decision processes. In Proc. 35th IEEE Symp. on Logic in Computer Science, pages 195-208. ACM, 2020. Google Scholar
  7. R. Berthon, M. Randour, and J-F. Raskin. Threshold constraints with guarantees for parity objectives in markov decision processes. In Proc. 44th Int. Colloq. on Automata, Languages, and Programming, volume 80 of LIPIcs, pages 121:1-121:15. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017. Google Scholar
  8. R. Bloem, K. Chatterjee, T. Henzinger, and B. Jobstmann. Better quality in synthesis through quantitative objectives. In Proc. 21st Int. Conf. on Computer Aided Verification, volume 5643 of Lecture Notes in Computer Science, pages 140-156. Springer, 2009. Google Scholar
  9. R. Bloem, K. Chatterjee, and B. Jobstmann. Graph games and reactive synthesis. In Handbook of Model Checking., pages 921-962. Springer, 2018. Google Scholar
  10. G. Bruns and P. Godefroid. Model checking partial state spaces with 3-valued temporal logics. In Proc. 11th Int. Conf. on Computer Aided Verification, pages 274-287, 1999. Google Scholar
  11. V. Bruyère, E. Filiot, M. Randour, and J-F. Raskin. Meet your expectations with guarantees: Beyond worst-case synthesis in quantitative games. In Proc. 31th Symp. on Theoretical Aspects of Computer Science, volume 25 of LIPIcs, pages 199-213, 2014. Google Scholar
  12. C.S. Calude, S. Jain, B. Khoussainov, W. Li, and F. Stephan. Deciding parity games in quasipolynomial time. In Proc. 49th ACM Symp. on Theory of Computing, pages 252-263, 2017. Google Scholar
  13. P. Cerný, K. Chatterjee, T.A. Henzinger, A. Radhakrishna, and R. Singh. Quantitative synthesis for concurrent programs. In Proc. 23rd Int. Conf. on Computer Aided Verification, pages 243-259, 2011. Google Scholar
  14. K. Chatterjee, L. Doyen, T. A. Henzinger, and J-F. Raskin. Algorithms for ω-regular games with imperfect information. In Proc. 15th Annual Conf. of the European Association for Computer Science Logic, volume 4207 of Lecture Notes in Computer Science, pages 287-302, 2006. Google Scholar
  15. K. Chatterjee, T. Henzinger, and B. Jobstmann. Environment assumptions for synthesis. In Proc. 19th Int. Conf. on Concurrency Theory, volume 5201 of Lecture Notes in Computer Science, pages 147-161. Springer, 2008. Google Scholar
  16. Y-F. Chen, O. Lengál, T. Tan, and Z. Wu. Register automata with linear arithmetic. In Proc. 32nd IEEE Symp. on Logic in Computer Science, pages 1-12, 2017. Google Scholar
  17. M.R. Clarkson, B. Finkbeiner, M. Koleini, K.K. Micinski, M.N. Rabe, and C. Sánchez. Temporal logics for hyperproperties. In 3rd International Conference on Principles of Security and Trust, volume 8414 of Lecture Notes in Computer Science, pages 265-284. Springer, 2014. Google Scholar
  18. L. de Alfaro and P. Roy. Solving games via three-valued abstraction refinement. Inf. Comput., 208(6):666-676, 2010. Google Scholar
  19. S. Demri. Linear-time temporal logics with presburger constraints: an overview. Journal of Applied Non-Classical Logics, 16(3-4):311-348, 2006. Google Scholar
  20. I. Dinur and K. Nissim. Revealing information while preserving privacy. In Proceedings of the 22nd ACM Symposium on Principles of Database Systems, pages 202-210. ACM, 2003. Google Scholar
  21. J. Dubreil, Ph. Darondeau, and H. Marchand. Supervisory control for opacity. IEEE Transactions on Automatic Control, 55(5):1089-1100, 2010. Google Scholar
  22. C. Dwork, F. McSherry, K. Nissim, and A.D. Smith. Calibrating noise to sensitivity in private data analysis. J. Priv. Confidentiality, 7(3):17-51, 2016. Google Scholar
  23. E.A. Emerson and C.-L. Lei. Efficient model checking in fragments of the propositional μ-calculus. In Proc. 1st IEEE Symp. on Logic in Computer Science, pages 267-278, 1986. Google Scholar
  24. B. Finkbeiner, C. Hahn, P. Lukert, M. Stenger, and L. Tentrup. Synthesis from hyperproperties. Acta Informatica, 57(1-2):137-163, 2020. Google Scholar
  25. D. Fisman, O. Kupferman, and Y. Lustig. Rational synthesis. In Proc. 16th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems, volume 6015 of Lecture Notes in Computer Science, pages 190-204. Springer, 2010. Google Scholar
  26. D. Fisman, O. Kupferman, S. Seinvald, and M.Y. Vardi. A framework for inherent vacuity. In 4th International Haifa Verification Conference, volume 5394 of Lecture Notes in Computer Science, pages 7-22. Springer, 2008. Google Scholar
  27. S. Garg, C. Gentry, S. Halevi, M. Raykova, A. Sahai, and B. Waters. Candidate indistinguishability obfuscation and functional encryption for all circuits. SIAM J. Comput., 45(3):882-929, 2016. Google Scholar
  28. A. Gurfinkel and M. Chechik. Multi-valued model-checking via classical model-checking. In Proc. 14th Int. Conf. on Concurrency Theory, pages 263-277. Springer-Verlag, 2003. Google Scholar
  29. O. Kupferman and Y. Lustig. Lattice automata. In Proc. 8th Int. Conf. on Verification, Model Checking, and Abstract Interpretation, volume 4349 of Lecture Notes in Computer Science, pages 199-213. Springer, 2007. Google Scholar
  30. O. Kupferman and M.Y. Vardi. Synthesis with incomplete information. In Advances in Temporal Logic, pages 109-127. Kluwer Academic Publishers, 2000. Google Scholar
  31. O. Kupferman and M.Y. Vardi. Safraless decision procedures. In Proc. 46th IEEE Symp. on Foundations of Computer Science, pages 531-540, 2005. Google Scholar
  32. M. Z. Kwiatkowska. Model checking and strategy synthesis for stochastic games: From theory to practice. In Proc. 43th Int. Colloq. on Automata, Languages, and Programming, volume 55 of LIPIcs, pages 4:1-4:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016. Google Scholar
  33. S. Maoz and R. Shalom. Inherent vacuity for GR(1) specifications. In Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, pages 99-110. ACM, 2020. Google Scholar
  34. N. Piterman. From nondeterministic Büchi and Streett automata to deterministic parity automata. In Proc. 21st IEEE Symp. on Logic in Computer Science, pages 255-264. IEEE press, 2006. Google Scholar
  35. J.H. Reif. The complexity of two-player games of incomplete information. Journal of Computer and Systems Science, 29:274-301, 1984. Google Scholar
  36. S. Safra. On the complexity of ω-automata. In Proc. 29th IEEE Symp. on Foundations of Computer Science, pages 319-327, 1988. Google Scholar
  37. S. Safra. Complexity of automata on infinite objects. PhD thesis, Weizmann Institute of Science, 1989. Google Scholar
  38. S. Schewe. Synthesis of distributed systems. PhD thesis, Saarland University, Saarbrücken, Germany, 2008. Google Scholar
  39. S. Shoham and O. Grumberg. A game-based framework for CTL counterexamples and 3-valued abstraction-refinement. In Proc. 15th Int. Conf. on Computer Aided Verification, volume 2725, pages 275-287, 2003. Google Scholar
  40. A.P. Sistla, M.Y. Vardi, and P. Wolper. The complementation problem for Büchi automata with applications to temporal logic. Theoretical Computer Science, 49:217-237, 1987. Google Scholar
  41. M.Y. Vardi. From verification to synthesis. In VSTTE, page 2, 2008. Google Scholar
  42. M.Y. Vardi and P. Wolper. Reasoning about infinite computations. Information and Computation, 115(1):1-37, 1994. Google Scholar
  43. Y. Wu, V. Raman, B.C. Rawlings, S. Lafortune, and S.A. Seshia. Synthesis of obfuscation policies to ensure privacy and utility. Journal of Automated Reasoning, 60(1):107-131, 2018. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact