Main Page
(→Our research on opacity and its enforcement) |
(→Obfuscation Project of the DES Group at the University of Michigan) |
||
| Line 35: | Line 35: | ||
''Proceedings of the 14th International Workshop on Discrete Event Systems'', | ''Proceedings of the 14th International Workshop on Discrete Event Systems'', | ||
June 2018, pp. 157-163. | June 2018, pp. 157-163. | ||
| + | |||
| + | |||
| + | Video of App implementing real-time obfuscation for location privacy: | ||
| + | |||
===== Obfuscation Game: Can you keep a secret? ===== | ===== Obfuscation Game: Can you keep a secret? ===== | ||
Revision as of 14:58, June 17, 2021
Contents |
Obfuscation Project of the DES Group at the University of Michigan
We call this page the Obfuscation Project. A better but less catchy name should probably be: Opacity Enforcement and Its Application to Location Privacy.
What is Opacity?
Opacity is a general property that has been defined and studied in the context of computer security and privacy. Assuming that some information about a user is revealed to an eavesdropper with potentially malicious intentions, and assuming that a portion of that information needs to be kept secret, opacity roughly means that the user can always maintain plausible deniability about its secret information. Let's say that someone is tracking your movements and that your secret information is that you are at the bank, then the tracking should not reveal with certainty that you are at the bank; perhaps you could also be at the coffee shop next to the bank. For an overview of the study of opacity, please refer to [1]. For some historical remarks regarding the study of opacity in a branch of control engineering known as Discrete Event Systems (DES), see [2].
[1] Romain Jacob, Jean-Jacques Lesage, Jean-Marc Faure, "Overview of discrete event systems opacity: Models, validation, and quantification," Annual Reviews in Control, Volume 41, 2016, Pages 135-146.
[2] S. Lafortune, F. Lin, and C. Hadjicostis, "On the History of Diagnosability and Opacity in Discrete Event Systems," Annual Reviews in Control, Vol. 45, pp. 257-266, 2018.
Location Privacy: An Approach based on Opacity
Our group at Michigan has been doing work on opacity and its enforcement for many years. More on this in the section below. To illustrate our theoretical work on opacity enforcement by insertion and edit functions, we have used location privacy as an illustrative example. Let's imagine that you can send slightly altered (i.e., obfuscated) information about your location as you move around in a certain geographical area. Then how should your position information be slightly altered, as observed by the eavesdropper or other parties, so that your visits to secret locations are never revealed? This is more complicated than adding random noise to your location as you move. The obfuscated trajectory is required to be a valid trajectory where you are moving. Inside a building, the obfuscated trajectory should not go through walls. If you are moving around campus or town, then it should not go through buildings and follow sidewalks or streets. Moreover, to make the problem more challenging (and also more realistic), we require that the obfuscated position should never be more than a certain maximum distance from the true one. Our general algorithms for opacity enforcement by insertion functions can be used to solve this problem, if we model the trajectory of the user by discrete moves, such as from tile to tile in a grid.
The paper [3] gives an example on our methodology for location privacy for a user moving around the Central Campus of the University of Michigan. For the sake of simplicity, we consider only 8 possible locations for the user, with one of them being the secret.
[3] Y.-C. Wu, K.A. Sankararaman, and S. Lafortune, "Ensuring Privacy in Location-Based Services: An Approach Based on Opacity Enforcement," Proceedings of the 12th International Workshop on Discrete Event Systems, May 2014.
The paper [4] shows how to actually implement the same methodology in an indoor setting, using real-time data from an acoustic positioning system and a real-time obfuscator implemented in the cloud. The grid there is much larger, over 30 by 40.
[4] R. Meira Góes, B.C. Rawlings, N. Recker, G. Willett, and S. Lafortune, "Demonstration of Indoor Location Privacy Enforcement using Obfuscation," Proceedings of the 14th International Workshop on Discrete Event Systems, June 2018, pp. 157-163.
Video of App implementing real-time obfuscation for location privacy:
Obfuscation Game: Can you keep a secret?
As a way to illustrate the challenge of enforcing location privacy using obfuscation in an amusing way, we developed the Obfuscation Game. Here, the user is the obfuscator and it must try to obfuscate, in real-time, the moves of an agent in a grid. In the Obfuscation Game, our algorithms for opacity enforcement are relegated to the background and the user must do the obfuscation on their own. They play against the computer, which simply moves the agent randomly. The goal of this game is to show that due to obstacles and the maximum distance constraint, the obfuscator needs to plan several steps ahead (as in most board games), and this can often be quite difficult. Our algorithm does run in the background and it can provide a hint to the user, if need be.
The implementation of the background obfuscator in the Obfuscation Game is based on the symbolic implementation of edit functions in the paper [5].
[5] Y.-C. Wu, V. Raman, B.C. Rawlings, S. Lafortune, and S. Seshia, "Synthesis of Obfuscation Policies to Ensure Privacy and Utility," Journal of Automated Reasoning. Vol. 60, No. 1, pp. 107-131, January 2018.
Several people contributed to the development of the Obfuscation Game, principally Isaac Dubuque, Andrew Bourgeois, and Jack Weize, who worked under the mentorship of Blake Rawlings and Rômulo Meira-Góes.
Try the Obfuscation Game. We hope you enjoy it!
Our research on opacity and its enforcement
Our results to-date on opacity and its enforcement have been published in the papers listed below and organized chronologically. (Conference papers are omitted if they were followed by a journal paper that subsumed them.)
Opacity enforcement by insertion of fictitious events, or by deletion of events under some constraints, were the main results in the doctoral dissertations of Yi-Chin Wu and Yiding Ji. Xiang Yin contributed to opacity enforcement by supervisory control in his doctoral dissertation. Rômulo Meira-Góes participated in several papers on implementation of opacity enforcement during his graduate studies. Research fellows Blake Rawlings, Christoforos Keroglou, and Sahar Mohajerani were also important contributors to our efforts. Current student Andrew Wintenberg is considering opacity verification and enforcement in his doctoral research.
Several undergraduate students interned in our group and participated in our efforts; they are listed below as co-authors in the relevant papers. We also acknowledge our external collaborators.
Financial acknowledgement: We acknowledge in the papers below the sponsors that have made this work possible, principally the US National Science Foundation.
- Our first paper on the verification of different notions of opacity:
Y.C. Wu and S. Lafortune, "Comparative Analysis of Related Notions of Opacity in Centralized and Coordinated Architectures," Discrete Event Dynamic Systems: Theory and Applications. Vol. 23, No. 3, September 2013, pp. 307-339.
- Our papers where we first introduced opacity enforcement by insertion functions, applied this approach to location privacy, and considered a class of optimal insertion functions according to different cost criteria, first for a logical DES model and then for a stochastic DES model:
Y.-C. Wu and S. Lafortune, "Synthesis of Insertion Functions for Enforcement of Opacity Security Properties," Automatica. Vol. 50, No. 5, May 2014, pp. 1336-1348.
Y.-C. Wu, K.A. Sankararaman, and S. Lafortune, "Ensuring Privacy in Location-Based Services: An Approach Based on Opacity Enforcement," Proceedings of the 12th International Workshop on Discrete Event Systems, May 2014.
Y.C. Wu and S. Lafortune, "Synthesis of Optimal Insertion Functions for Opacity Enforcement," IEEE Transactions on Automatic Control. Vol. 61, No. 3, March 2016, pp. 571-584.
Y.-C. Wu, G. Lederman, and S. Lafortune, "Enhancing opacity of stochastic discrete event systems using insertion functions," Proceedings of the 2016 American Control Conference, July 2016, pp. 2053--2060.
- Our first paper on opacity enforcement by supervisory control:
X. Yin and S. Lafortune, "A Uniform Approach for Synthesizing Property-Enforcing Supervisors for Partially-Observed Discrete-Event Systems," IEEE Transactions on Automatic Control. Vol. 61, No. 8, August 2016, pp. 2140-2154.
- Our paper on a new method to verify K-step and infinite-step opacity:
X. Yin and S. Lafortune, "A New Approach for the Verification of Infinite-Step and K-Step Opacity using Two-Way Observers," Automatica. Vol. 80, pp. 162-171, June 2017. See also Vol. 124, Article 109273, February 2021, for Authors' Reply to Comment on above article.
- Our paper on obfuscation by edit functions, in a general set up of obfuscation where opacity itself is implicit and edit functions must satisfy a utility constraint:
Y.-C. Wu, V. Raman, B.C. Rawlings, S. Lafortune, and S. Seshia, "Synthesis of Obfuscation Policies to Ensure Privacy and Utility," Journal of Automated Reasoning. Vol. 60, No. 1, pp. 107-131, January 2018.
- Back to opacity enforcement by insertion functions, but this time allowing for deciding on insertion actions based on strings of length K, as opposed to one event at a time:
C. Keroglou, S. Lafortune, and L. Ricker, "Insertion Functions with Memory for Opacity Enforcement," Proceedings of the 14th International Workshop on Discrete Event Systems, June 2018, pp. 405-410.
- Application of opacity enforcement by edit functions with a utility constraint to location privacy in an indoor environment:
R. Meira Góes, B.C. Rawlings, N. Recker, G. Willett, and S. Lafortune, "Demonstration of Indoor Location Privacy Enforcement using Obfuscation," Proceedings of the 14th International Workshop on Discrete Event Systems, June 2018, pp. 157-163.
- More general set up of opacity enforcement by insertion or edit functions that may be known by the eavesdropper (public-private case):
Y. Ji, Y.-C. Wu, and S. Lafortune, "Enforcement of Opacity by Public and Private Insertion Functions," Automatica, Vol. 93, July 2018, pp. 369-378.
Y. Ji, X. Yin, and S. Lafortune, "Opacity Enforcement using Nondeterministic Publicly-Known Edit Functions," IEEE Transactions on Automatic Control. Vol. 64, No. 10, October 2019, pp. 4369-4376.
- Different approach to optimal insertion functions for opacity enforcement, under energy constraints:
Y. Ji, X. Yin, and S. Lafortune, "Enforcing Opacity by Insertion Functions under Multiple Energy Constraints, Automatica. Vol. 108, October 2019, pp. 108476 (1-14).
- Application of modular methods to opacity verification and enforcement (case of edit functions):
S. Mohajerani and S. Lafortune, "Transforming opacity verification to nonblocking verification in modular systems," IEEE Transactions on Automatic Control, Vol. 65, No. 4, April 2020, pp. 1739-1746.
S. Mohajerani, Y. Ji, and S. Lafortune, "Compositional and Abstraction-Based Approach for Synthesis of Edit Functions for Opacity Enforcement." IEEE Transactions on Automatic Control, Vol. 65, No. 8, August 2020, pp. 3349-3364.
- Opacity enforcement by insertion functions that can see the unobservable events generated by the systems (i.e., these insertion functions are embedded in the system as opposed to being an output interface):
C. Keroglou and S. Lafortune, "Embedded Insertion Functions for Opacity Enforcement," IEEE Transactions on Automatic Control. In print. [DOI: 10.1109/TAC.2020.3037891]
- Our most recent work on a general approach to opacity verification that covers not only current-state opacity but also K-step opacity in a unified framework, and application of that approach to enforcement of K-step opacity by edit functions:
A. Wintenberg, M. Blischke, S. Lafortune, and N. Ozay, "A General Language-Based Framework for Specifying and Verifying Notions of Opacity." Under review. Deposited in arxiv
A. Wintenberg, M. Blischke, S. Lafortune, and N. Ozay, "Enforcement of K-Step Opacity with Edit Functions," submitted to IEEE Conference on Decision and Control, December 2021.
