Opacity Enforcement via Greedy Privately-and-Publicly Known Insertion Functions

In this article, we investigate the enforcement of (current-state) opacity, an important information-flow security property, via insertion functions. An insertion function is an obfuscation mechanism that inserts fictitious events to the outputs in order to confuse the outside observer (intruder) such that the secret of the system is not revealed. In some situations, the secret may be revealed when the insertion mechanism is (or becomes) publicly known. This leads to the problem of synthesizing private-and-public enforcing (PP-enforcing) insertion functions in the sense that opacity is still enforced even when the mechanism is discovered or published by the designer. Existing works that have investigated this synthesis problem are either only sound or have limited applicability as we show in this work. For this reason, and more importantly, to better solve the synthesis problem, a new approach is proposed upon an improved greedy criterion. We show that the proposed algorithm is both sound and complete, and can be used to completely solve the synthesis problem for the PP-enforcing insertion function. With slight modifications of our algorithm, infinite-step opacity and
$ K$
-step opacity can also be enforced under publicly-known insertion mechanisms.