嵌入式操作系统作为基础性软件系统,管理着嵌入式系统的软硬件资源,是嵌入式系统的核心与基石。近年来,随着智能技术和物联网的不断融合,嵌入式操作系统得到广泛应用,并呈现出智能化、网络化的发展趋势。但与此同时,嵌入式操作系统的自身安全性和用户敏感信息的安全性成为了嵌入式领域亟需解决的重点和难点问题。一旦嵌入式操作系统出现软件错误或泄露机密信息,则可能造成重大的安全事故或极大的经济损失。因此,针对嵌入式操作系统的应用场景,分析其实际特征需求,建立功能性、安全性的形式化模型,证明系统代码实现确实符合形式化的功能规范和安全属性规范,已成为重要的研究课题。针对上述问题,本文深入分析并总结了嵌入式操作系统的设计实现与验证需求,并针对内存管理模块的功能性验证、任务管理模块的功能性验证和可信执行环境的安全性验证等关键问题,分别提出了相应的解决方案,最终形成了一套可扩展的模块化验证框架与验证系统,以及实现并评估了一个经过验证的安全嵌入式操作系统可信执行环境。评估结果表明,可扩展的模块化验证框架结合硬件隔离保护机制,既能满足嵌入式操作系统在功能、性能和安全性方面的特殊需求,又能提高系统整体验证的可行性,为系统源码实现满足系统功能性、安全性需求提供可信证据。本文的主要贡献和创新点有:(1)为实现嵌入式操作系统的整体验证,提出了一种面向嵌入式操作系统的可扩展的模块化验证框架。对于每个单独模块,首先基于分离逻辑描述C程序的实现层规范,接着使用函数式编程方式构建C程序的抽象层规范,然后构建起两者之间的数据精化关系并进行一致性证明,最后形成一个源码实现与抽象层规范行为一致的验证模块。对于系统整体验证,使用框架的组合验证规则将各子模块的抽象层规范链接成一个完整的验证系统。(2)针对嵌入式操作系统的内存管理模块,提出了包含复杂指针数据结构的高性能C程序的建模验证方法。以内存碎片率低、内存分配粒度多样化、执行时间可预估的内存管理算法为研究案例,基于模块化验证框架,成功定义了底层数据结构操作接口和高层内存分配、回收操作的行为语义,完成了高性能内存管理模块的建模验证工作。(3)针对嵌入式操作系统的任务管理模块,构建了ARM汇编语义模型,扩充了模块化验证框架对汇编语言的验证支持,提出了支持C和ARM汇编程序的组合验证系统。基于组合验证系统,将任务管理模块分成任务调度(C实现)和任务上下文切换(ARM汇编实现)两个子模块,首先在不同的抽象层分别建模验证,然后基于各子模块的抽象层规范进行组合验证,从而解决了分离逻辑不支持汇编函数指针的问题,最终顺利完成任务管理模块的形式化验证。(4)为了满足嵌入式操作系统对执行环境的隔离性要求,基于ARM TrustZone硬件保护机制提出了一种窄通信接口的可信执行环境设计方法,并构建了可信执行环境的安全属性模型(如信息流无干扰性模型),最后形成了一套支持端到端安全属性验证、C和汇编功能正确性验证、程序抽象及数据精化证明的集成验证系统。实现了首个基于ARM TrustZone硬件保护机制的多任务嵌入式操作系统的形式化验证。(5)整个系统的形式化实现、规范、模型、属性定义和证明,均在辅助定理证明器Coq中完成,最大程度降低了不同规范接口间的语义鸿沟。最终经验证的软件系统可在真实硬件平台上执行,整套理论方案具备较高的实用性。目前,在嵌入式操作系统形式化验证领域仍然存在诸多挑战。本文旨在为研发与验证安全可靠的嵌入式操作系统提供新的理论依据和技术方法。