时间自动机驱动的多级安全系统无干扰控制器设计

本文探讨了在多级安全环境下，密集时间离散事件系统（Dense Time Discrete Event Systems, DTDES）中，利用时间自动机（Time Automata）构建无干扰控制器的复杂问题。首先，作者对“非干扰”这一概念进行了深入讨论，强调在计算环境中，特别是涉及敏感数据处理的情况下，确保程序不泄露信息至未经授权的用户的重要性，这是信息安全领域的一个核心课题，被称为保密性。 在实时操作系统（Real-time Operating Systems,RTOS）背景下，传统的安全模型可能存在局限性。为了提升安全性，文中提出了一种扩展的时间自动机模型，它能够更好地捕捉高级信息与低级行为之间的复杂因果关系。这种模型的关键在于验证密集时间属性的可判定性问题，即确定是否可以通过时间自动机设计出满足特定安全约束的控制器。 作者证明了关于定时非干扰属性的定时控制器合成问题具有可判定性，这意味着存在一种符号化的算法方法，能够有效地合成出既能确保系统功能正常运行又能保障信息安全的控制器。这种方法的可判定性是基于理论计算机科学的坚实基础，包括形式逻辑、计算复杂性和自动机理论。 总结来说，这篇论文的贡献在于提供了一种创新的方法论，用于设计和验证在多级安全DTDES中的无干扰控制器，这对于保护敏感信息免受未经授权访问具有重要的实践意义。它不仅解决了实际问题，还对理论界关于可判定性问题的研究有所推进，推动了安全计算技术的发展。通过这种方法，研究人员和工程师可以更好地理解和实现复杂系统的安全控制策略。