Synthesis of Opacity-Enforcing Insertion Functions that can be Publicly Known
Yi-Chin Wu, Stephane Lafortune

Citation
Yi-Chin Wu, Stephane Lafortune. "Synthesis of Opacity-Enforcing Insertion Functions that can be Publicly Known". 54th Conference on Decision and Control, IEEE, 15, December, 2015.

Abstract
Our prior work has studied the enforcement of opacity, a security property, using insertion functions that insert fictitious events at the output of the system, thereby preventing an intruder from inferring the given system's secret. The insertion functions previously considered enforce opacity under the assumption that the intruder does not know about the implementation of the insertion function. In this paper, we relax that assumption and consider a stronger class of insertion functions that enforce opacity whether or not the intruder knows the insertion function. This property is formally characterized as public-and-private enforceability, or PP-enforceability for short. A PP-enforcing insertion function is guaranteed to output only behaviors consistent with the nonsecret behaviors of the system and thus it enforces opacity when the intruder has no knowledge of the insertion function (private case). Moreover, a PP-enforcing insertion function guarantees that the intruder can never infer the occurrence of the secret, even when the intruder knows the exact implementation of the insertion function (public case). We characterize the property of PP-enforceability and present an algorithm that provably synthesizes a PP-enforcing insertion function.

Electronic downloads

Internal. This publication has been marked by the author for TerraSwarm-only distribution, so electronic downloads are not available without logging in.

Citation formats

• HTML

  Yi-Chin Wu, Stephane Lafortune. <a
  href="http://www.terraswarm.org/pubs/521.html"
  >Synthesis of Opacity-Enforcing Insertion Functions that
  can be Publicly Known</a>, 54th Conference on Decision
  and Control, IEEE, 15, December, 2015.

• Plain text

  Yi-Chin Wu, Stephane Lafortune. "Synthesis of
  Opacity-Enforcing Insertion Functions that can be Publicly
  Known". 54th Conference on Decision and Control, IEEE,
  15, December, 2015.

• BibTeX

  @inproceedings{WuLafortune15_SynthesisOfOpacityEnforcingInsertionFunctionsThatCan,
      author = {Yi-Chin Wu and Stephane Lafortune},
      title = {Synthesis of Opacity-Enforcing Insertion Functions
                that can be Publicly Known},
      booktitle = {54th Conference on Decision and Control},
      organization = {IEEE},
      day = {15},
      month = {December},
      year = {2015},
      abstract = {Our prior work has studied the enforcement of
                opacity, a security property, using insertion
                functions that insert fictitious events at the
                output of the system, thereby preventing an
                intruder from inferring the given system's secret.
                The insertion functions previously considered
                enforce opacity under the assumption that the
                intruder does not know about the implementation of
                the insertion function. In this paper, we relax
                that assumption and consider a stronger class of
                insertion functions that enforce opacity whether
                or not the intruder knows the insertion function.
                This property is formally characterized as
                public-and-private enforceability, or
                PP-enforceability for short. A PP-enforcing
                insertion function is guaranteed to output only
                behaviors consistent with the nonsecret behaviors
                of the system and thus it enforces opacity when
                the intruder has no knowledge of the insertion
                function (private case). Moreover, a PP-enforcing
                insertion function guarantees that the intruder
                can never infer the occurrence of the secret, even
                when the intruder knows the exact implementation
                of the insertion function (public case). We
                characterize the property of PP-enforceability and
                present an algorithm that provably synthesizes a
                PP-enforcing insertion function. },
      URL = {http://terraswarm.org/pubs/521.html}
  }
  

Posted by Barb Hoversten on 24 Mar 2015.
Groups: services