高可信嵌入式操作系统：Hades架构及其安全信息流控制

"高可信嵌入式操作系统体系架构研究" 嵌入式操作系统是现代技术发展的重要组成部分，尤其在航空航天、核电能源、医疗卫生、国防电子等领域，它们对于安全关键系统的运行至关重要。由于这些系统的特殊性，一旦发生故障，可能导致重大的生命财产损失和环境破坏。在这些尖端领域，多级安全关键嵌入式系统的需求日益增加，它们需要同时满足不同级别的安全应用需求。 然而，随着互联网技术和软件技术的广泛应用，软件故障、失效以及安全威胁已经成为引发系统失效的主要因素。因此，提高多级安全关键嵌入式系统的可信性成为了当前亟待解决的问题。高可信嵌入式操作系统体系架构的构建旨在从软件平台层面提升系统的可信能力，它是解决这一问题的关键所在。 论文作者杨霞在其博士学位论文中对当前的高可信保障技术进行了详尽的分析，指出存在的主要挑战：一是难以同时满足安全性、防危性、实时性等多种可信属性；二是不能适应多级安全应用的复杂需求；三是系统开销过大，可能无法通过高级别的安全认证。为解决这些问题，论文提出了以下几点研究和贡献： 1. 对可信计算的概念和属性进行了深入探讨，明确了嵌入式操作系统高可信保障技术的局限性，并定义了嵌入式可信操作系统的概念，为后续研究开辟了新的方向。 2. 设计了一种名为Hades的高可信嵌入式操作系统体系架构。该架构创新性地克服了传统技术的不足，能够同时支持多个高可信属性，并通过时空隔离和分区机制限制故障和安全威胁的影响范围，同时为多级安全应用提供有效支持。 3. 针对敏感信息的保密性，分析了现有分区间数据通信机制的不足，提出了一种多级安全信息流控制模型。该模型建立了严格的信息流控制机制和策略，确保所有跨区间的通信都需经过可信分离内核的授权。实验验证表明，这种信息流控制机制是可行的，且其低系统开销不会妨碍可信分离内核的安全认证。 总体而言，这篇博士学位论文对高可信嵌入式操作系统体系架构的研究，不仅深化了我们对嵌入式系统可信性的理解，也为设计更安全、更可靠的嵌入式系统提供了理论基础和实践指导。通过Hades架构的创新设计，未来有望实现更加高效、多级安全的嵌入式系统，以满足日益严苛的安全需求。