Verification and Synthesis of Embedded Insertion Functions for Opacity Enforcement

  • Authors:
    Christoforos Keroglou (Univ. of Michigan), Stephane Lafortune (Univ. of Michigan)
    Publication ID:
    Publication Type:
    Received Date:
    Last Edit Date:
    2386.003 (California Institute of Technology)


We investigate the enforcement of opacity, an information-flow privacy property, using insertion decisions that modify the output of the system by event insertions. Previous work considered the problem of enforcing opacity under the assumption that the insertion functions were based on the observed system strings. Now, we investigate the more powerful method of insertion decisions based on the exact system states and events. In this case, the insertion function would be embedded into the system itself, rather than being an output interface. In this paper we develop methods that (i) verify if a valid insertion function exists in this setting; and (ii) if one exists, synthesize one using a computationally effective algorithm.

4819 Emperor Blvd, Suite 300 Durham, NC 27703 Voice: (919) 941-9400 Fax: (919) 941-9450

Important Information for the SRC website. This site uses cookies to store information on your computer. By continuing to use our site, you consent to our cookies. If you are not happy with the use of these cookies, please review our Cookie Policy to learn how they can be disabled. By disabling cookies, some features of the site will not work.