Abstract
We consider the problem of synthesizing an obfuscation policy that enforces privacy while preserving utility with formal guarantees. Specifically, we consider plants modeled as finite automata with pre-defined secret behaviors. A given plant generates event strings for some useful computation, but meanwhile wants to hide its secret behaviors from any outside observer. We formally capture the privacy and utility specifications using the automaton model of the plant. To enforce both specifications, we propose an obfuscation mechanism where an edit function “edits” the plant’s output in a reactive manner. We develop algorithmic procedures that synthesize a correct-by-construction edit function satisfying both privacy and utility specifications. To address the state explosion problem, we encode the synthesis algorithm symbolically using Binary Decision Diagrams. We present EdiSyn, an implementation of our algorithms, along with experimental results demonstrating its performance on illustrative examples. This is the first work, to our knowledge, to successfully synthesize controllers satisfying both privacy and utility requirements.
This work was supported in part by TerraSwarm, one of six centers of STARnet, a Semiconductor Research Corporation program sponsored by MARCO and DARPA, and in part by the National Science Foundation under grants CCF-1138860 and CCF-1139138 (NSF Expeditions in Computing project ExCAPE: Expeditions in Computer Augmented Program Engineering) and CNS-1421122.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
EdiSyn is available at https://bitbucket.org/yichinwu/edisyn.
References
Bryant, R.E.: Graph-based algorithms for Boolean function manipulation. IEEE Trans. Comput. C–35(8), 677–691 (1986)
Dwork, C.: Differential privacy. In: International Conference on Automata, Languages and Programming, pp. 1–12 (2006)
Emerson, E.A.: Model checking and the mu-calculus. DIMACS Ser. Discrete Math. 31, 185–214 (1997)
Falcone, Y., Marchand, H.: Runtime enforcement of K-step opacity. In: 52nd IEEE Conference on Decision and Control (2013)
Filippidis, I.: https://github.com/johnyf/dd
Kozen, D.: Results on the propositional \(\mu \)-calculus. Theor. Comput. Sci. 27(3), 333–354 (1983)
Kupferman, O., Tamir, T.: Coping with selfish on-going behaviors. In: Clarke, E.M., Voronkov, A. (eds.) LPAR-16 2010. LNCS, vol. 6355, pp. 501–516. Springer, Heidelberg (2010)
O’Kane, J.M., Shell, D.A.: Automatic design of discreet discrete filters. In: IEEE International Conference on Robotics and Automation (ICRA), pp. 353–360 (2015)
Ramadge, P.J., Wonham, W.M.: Supervisory control of a class of discrete event processes. SIAM J. Control Optim. 25(1), 206–230 (1987)
Saboori, A., Hadjicostis, C.N.: Opacity-enforcing supervisory strategies via state estimator constructions. IEEE Trans. Autom. Control 57(5), 1155–1165 (2012)
Somenzi, F.: CUDD: CU decision diagram package release 2.3.0. University of Colorado at Boulder (1998)
Wu, Y.-C., Lafortune, S.: Synthesis of insertion functions for enforcement of opacity security properties. Automatica 50(5), 1336–1348 (2014)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer International Publishing Switzerland
About this paper
Cite this paper
Wu, YC., Raman, V., Lafortune, S., Seshia, S.A. (2016). Obfuscator Synthesis for Privacy and Utility. In: Rayadurgam, S., Tkachuk, O. (eds) NASA Formal Methods. NFM 2016. Lecture Notes in Computer Science(), vol 9690. Springer, Cham. https://doi.org/10.1007/978-3-319-40648-0_11
Download citation
DOI: https://doi.org/10.1007/978-3-319-40648-0_11
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-40647-3
Online ISBN: 978-3-319-40648-0
eBook Packages: Computer ScienceComputer Science (R0)