📝 SummarXiv

Abstract

The secret protection problem (SPP) seeks to synthesize a minimum-cost policy ensuring that every execution from an initial state to a secret state includes a sufficient number of protected events. Previous work showed that the problem is solvable in polynomial time under the assumptions that transitions are uniquely labeled and that the clearance level for every event is uniformly set to one. When these assumptions are relaxed, the problem was shown to be weakly NP-hard, leaving the complexity of the uniform variant open. In this paper, we close this gap by proving that the uniform secret protection problem is NP-hard, even if all parameters are restricted to binary values. Moreover, we strengthen the existing results by showing that the general problem becomes NP-hard as soon as the uniqueness constraint on event labels is removed. We further propose a formulation of SPP as an Integer Linear Programming (ILP) problem. Our empirical evaluation demonstrates the scalability and effectiveness of the ILP-based approach on relatively large systems. Finally, we examine a variant of SPP in which only distinct protected events contribute to clearance and show that its decision version is $\Sigma_{2}^{P}$-complete.