用于增强不透明度的扩展插入函数
Extended Insertion Functions for Opacity Enforcement
摘要：
不透明性是一种机密性属性，当给定系统的某些秘密字符串在任何系统活动下都不能透露给外部观察者时，它就成立了。违反不透明激励不透明执法策略的研究。在其他方法中，不透明度已经使用插入机制来实施，即，输出混淆机制，允许在实际系统输出之前插入虚构的输出符号，以保持不透明性。本文研究和分析了更强大的扩展插入机制，它可以在实际系统输出之前和之后插入符号，从而为更广泛的系统提供不透明性。为了解决实际问题，本文还引入了事件插入约束（即，在实际系统输出之前和/或之后只能插入特定符号的情况）。对于每一种情况，我们构造了一个适当的验证器，可以用来获得必要和充分条件检查不透明度可验证性。
英文摘要：
Opacity is a confidentiality property that holds when certain secret strings of a given system cannot be revealed to an outside observer under any system activity. Opacity violations stimulate the study of opacity enforcement strategies. Among other methodologies, opacity has been enforced using insertion mechanisms, i.e., output obfuscation mechanisms that are allowed to insert fictitious output symbols before actual system outputs, in order to preserve opacity. This paper studies and analyzes more powerful extended insertion mechanisms, which can insert symbols before and after an actual system output, thus, providing opacity to a wider class of systems. In order to address practical considerations, the paper also introduces event insertion constraints (i.e., the case when only specific symbols can be inserted before and/or after an actual system output). For each case, we construct an appropriate verifier that can be used to obtain necessary and sufficient conditions for checking opacity enforceability.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
