# Communication-Obfuscation Project

##
**Communication-Obfuscation Project of the UMDES Group at the University of Michigan**

We call this page the *Communication-Obfuscation Project*. A better but
less catchy name should probably be: *Opacity Enforcement by Edit
Functions and Its Applications*. We write *Communication-Obfuscation* to
differentiate our work from related but different work on program
obfuscation or other forms of obfuscation in security and privacy. As
explained below, our aim is to use obfuscation when communicating in
order to hide secrets and at the same time deceive eavesdroppers.

#### 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 right now; perhaps you could also be
at the coffee shop next to the bank. Opacity is defined for a dynamical
model that captures how observations are emitted to the outside world.
This would be a mobility model in the above tracking example. Opacity
can also capture inferencing about the past; for instance, the secret
information could be that you visited the bank in some prior time
interval.

For an overview of the study of opacity, please refer to [A]. For some historical remarks regarding the study of opacity in a branch of control engineering known as Discrete Event Systems (DES), see [B].

[A] 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.

[B] 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.

#### Applications of Opacity

Opacity is defined in the context of a formal dynamical model, typically a nondeterministic transition system such as an NFA or a DFA with unobservable events; Petri net models have also been considered in the literature. Since it is a formal property related to information flow, it can be used to model many scenarios of privacy or security in cyber and cyber-physical systems. Our group has used location privacy to illustrate our theoretical contributions to opacity enforcement, but this is by no means the only application domain of opacity. In our current work, we have been looking at privacy issues in the context of contact tracing. Other groups have looked at other application domains, such as smart homes, mobile agents in sensor networks, encryption guarantees in pseudo-random generators, and so forth; see [A] above as well as Chapter 8 in the recent book:

[C] C.H. Hadjicostis, "Estimation and Inference in Discrete Event Systems.'' Springer, 2020.

#### Our Publications on Opacity and its Enforcement

The UMDES group at Michigan has been doing work on opacity and its enforcement for many years. 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. Opacity
enforcement by such edit functions produces a new output stream of
events from the stream of events produced by the system. Hence, it acts
as an output interface. We call this output interface an *obfuscator*
and we refer to the method of opacity enforcement by edit functions as
*communication-obfuscation*. Note that edit functions must satisfy
strict constraints on the altered (or obfuscated) output stream of
events. Namely, the obfuscated output should both (i) hide the secret
(i.e., it should enforce opacity) and (ii) be believable to the
eavesdropper (or unintended recipient) in terms of its knowledge of the
system dynamics (i.e., it should enforce deception). So this is not
quite the same as security by obscurity.

Xiang Yin contributed to opacity enforcement by *supervisory control* in
his doctoral dissertation. In this case, the output stream of events is
reduced so that secret-revealing strings never happen.

Rômulo Meira-Góes participated in several papers on implementation of opacity enforcement by obfuscation during his graduate studies. Research fellows Blake Rawlings, Christoforos Keroglou, and Sahar Mohajerani were also important contributors to our efforts on this topic.

With current student Andrew Wintenberg, and in collaboration with colleague Necmiye Ozay, we have been developing novel obfuscation schemes that are simultaneously secure to eavesdroppers (i.e., achieve a given privacy/secrecy specification), yet maintain utility to legitimate recipients with access to relevant information about this obfuscation strategy (in the form of a so-called inference function). These obfuscation schemes are realized by input/output transducers that map an unsecure input data stream to a secure output data stream that can then be inferred upon by the legitimate recipients. The key is to synthesize simultaneously a pair of input-output transducers, one for obfuscation and one for inferencing, that work together to ensure security and privacy.

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.

Location privacy is not the only application of interest for opacity enforcement by edit functions (or obfuscation). Also, the synthesis problems that we solve in our papers for different types of obfuscators are generic and therefore applicable to a wide range of domains. Recently, we have also developed case studies based on contact tracing (see [18] and [19]).

**Financial acknowledgement:** We acknowledge in the papers below the
sponsors that have made this work possible, principally the US National
Science Foundation, TerraSwarm (one of six centers of STARnet, a
Semiconductor Research Corporation program sponsored by MARCO and
DARPA), and more recently, Cisco Research.

- Our first paper on the verification of different notions of opacity:

[1] 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:

[2] 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.

[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.

[4] 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.

[5] 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*:

[6] 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:

[7] 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
*communication-obfuscation*by*edit functions*, in a general set up of obfuscation where opacity itself is implicit and edit functions must satisfy a utility constraint:

[8] 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:

[9] 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:

[10] 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):

[11] 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.

[12] 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:

[13] 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):

[14] 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.

[15] 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):

[16] C. Keroglou and S. Lafortune, "Embedded Insertion Functions for
Opacity Enforcement," *IEEE Transactions on Automatic Control*. In
print. [DOI: 10.1109/TAC.2020.3037891]

- 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:

[17] A. Wintenberg, M. Blischke, S. Lafortune, and N. Ozay, "A General
Language-Based Framework for Specifying and Verifying Notions of
Opacity," *Discrete Event Dynamic Systems: Theory and Applications*,
2022. [DOI: 10.1007/s10626-021-00357-x]. Also deposited in
arxiv

[18] A. Wintenberg, M. Blischke, S. Lafortune, and N. Ozay,
"Enforcement of *K*-Step Opacity with Edit Functions," *IEEE Conference
on Decision and Control*, December 2021. [DOI:
10.1109/CDC45484.2021.9682936]

- Our work on obfuscation for both security and utility, where intended recipients are provided an inference function that allows them to retrieve desired information from the obfuscated stream of data:

[19] A. Wintenberg, M. Blischke, S. Lafortune, and N. Ozay, "A Dynamic
Obfuscation Framework for Security and Utility," *13th ACM/IEEE
International Conference on Cyber-Physical Systems (ICCPS)*, May 2022

#### Location Privacy: An Approach based on Opacity

To illustrate our theoretical work on opacity enforcement by insertion
and edit functions, or *communication-obfuscation*, 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.

Paper [3] above 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.

Paper [10] above 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. The real-time obfuscator is based on the symbolic implementation of edit functions in the paper [8] and on the SynthSMV tool presented in the paper [D] below.

[D] B.C. Rawlings, S. Lafortune, and B.E. Ydstie, "Supervisory Control
of Labeled Transition Systems Subject to Multiple Reachability
Requirements via Symbolic Model Checking," *IEEE Transactions on Control
Systems Technology*. Vol. 8, No. 2, March 2020, pp. 644-652.

The following video shows a simulation of the implementation described in [10]. The grid shown in the video represents the first floor of the Clark Kerr building on the campus of the University of California at Berkeley. Media:Obfuscation-video.ogv

Papers [18] and [19] above consider a refined version of location
privacy in the context of *contact tracing* and develop a model for
capturing privacy in this setting.

#### 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 [8] and on the SynthSMV tool presented in the paper [D].

Several people contributed to the development of the Obfuscation Game; alphabetically: Andrew Bourgeois, Isaac Dubuque, Nicholas Recker, Jack Weitze, and Gregory Willett. They worked under the mentorship of Rômulo Meira-Góes and Blake Rawlings.

Try the Obfuscation Game. We hope you enjoy it!

Here is a video showing a user playing the Obfuscation Game: Media:Obfgame.mp4

#### Obfuscation App: Real-time Obfuscation for Location Privacy

The methodology from [8] used for the background obfuscator in the
Obfuscation Game was also deployed in an *Obfuscation app* running on an
ipad for real-time obfuscation when a user is moving in an area with
secret locations and obstacles. Given a bounded geographical area
modeled by a grid with obstacle cells and secret cells, an obfuscator is
constructed so that the reported (or obfuscated) location never visits
the secret grid cells. At the same time, the reported location should be
within some given bound from the actual one, and the resulting
obfuscated trajectory should be a valid one (i.e., avoid the obstacles).
The app monitors the location of the user in real-time using GPS and the
obfuscator synthesized by the methodology in [8] is used in real-time
to select a reported position each time the user enters a new cell.

We produced a video of the actual and obfuscated trajectories as a user holding an ipad running the app was moving in the Gerstacker Grove on the North Campus of the University of Michigan in Ann Arbor. In that video, the blue circle is the actual user location from GPS, the blue diamond is the actual cell location used as input to the obfuscator, the purple diamond is the reported position by the obfuscator, the black grid cells are obstacles, and the orange grid cell is the secret location. Here, the constraint was that the obfuscated position should never be more than 2 cells away from the actual one; moreover, the obfuscator is allowed to move at most 3 cells when the user moves one cell. It can be seen that the obfuscated trajectory is a valid one, which is provably guaranteed by construction of the obfuscator (if one exists).

Video of app implementing real-time obfuscation for location privacy: Media:Walk_grove.mp4

Several people contributed to the development of the Obfuscation app; alphabetically: Andrew Bourgeois, Isaac Dubuque, Dylan Lawton, Nicholas Recker, Jack Weitze, and Gregory Willett. They worked under the mentorship of Rômulo Meira-Góes and Blake Rawlings.