Orna Kupferman ; Ofer Leshkowitz ; Namma Shamash Halevy - Synthesis with Privacy Against an Observer

lmcs:14744 - Logical Methods in Computer Science, July 29, 2025, Volume 21, Issue 3 - https://doi.org/10.46298/lmcs-21(3:12)2025
Synthesis with Privacy Against an ObserverArticle

Authors: Orna Kupferman ; Ofer Leshkowitz ; Namma Shamash Halevy

    We study automatic synthesis of systems that interact with their environment and maintain privacy against an observer to the interaction. The system and the environment interact via sets $I$ and $O$ of input and output signals. The input to the synthesis problem contains, in addition to a specification, also a list of secrets, a function $cost: I\cup O\rightarrow\mathbb{N}$, which maps each signal to the cost of hiding it, and a bound $b\in\mathbb{N}$ on the budget that the system may use for hiding of signals. The desired output is an $(I/O)$-transducer $T$ and a set $H\subseteq I\cup O$ of signals that respects the bound on the budget, thus $\sum_{s\in H} cost(s)\leq b$, such that for every possible interaction of $T$, the generated computation satisfies the specification, yet an observer, from whom the signals in $H$ are hidden, cannot evaluate the secrets.

    We first show that the problem's complexity is 2EXPTIME-complete for specifications and secrets in LTL, making it no harder than synthesis without privacy requirements. We then analyze the complexity further, isolating the two aspects that do not exist in traditional synthesis: the need to hide secret values and the need to choose the set $H$. We do this by studying settings in which traditional synthesis is solvable in polynomial time -- when the specification formalism is deterministic automata and when the system is closed -- and show that each of these aspects adds an exponential blow-up in complexity. We continue and study bounded synthesis with privacy, where the input includes a bound on the synthesized transducer size, as well as a variant of the problem in which the observer has knowledge, either about the specification or about the system, which can be helpful in evaluating the secrets. Additionally, we study certified privacy, where the synthesis algorithm provides certification that the secrets remain hidden.


    Volume: Volume 21, Issue 3
    Published on: July 29, 2025
    Accepted on: May 8, 2025
    Submitted on: November 14, 2024
    Keywords: Logic in Computer Science

    Consultation statistics

    This page has been seen 1052 times.
    This article's PDF has been downloaded 521 times.