为了满足先进工业制造和装备控制智能化的需求,嵌入式系统已成为关键基础设施的核心控制组件,并在工业制造、船舶、交通、国防安全、信息通信等领域起着影响全局系统安全的重要作用。近年来,随着嵌入式应用的广泛普及,以及网络化、智能化的发展趋势,系统运行的可靠性和敏感数据的安全性成为了嵌入式领域亟待解决的关键问题。倘若嵌入式软件系统失效或遭受安全入侵,则可能产生危及到国家政治、经济以及军事安全的重大事故。因此,如何针对此类安全关键的应用场景,设计和开发一种功能正确、满足所需安全(Security)和防危(Safety)属性,并能对所宣称的正确性提供确凿可信证据的嵌入式系统,成为了一个重要的研究课题。针对上述问题,本文全面分析并总结了高可信嵌入式应用对于系统软件的安全要求,提出满足安全隔离和形式化验证的软件体系架构。并针对系统软件中,硬件机制建模、可中断代码验证、不可信组件的安全访问控制以及基于虚拟化的隔离保护等关键问题,分别提出了相应的解决方法。最终,形成了一套可组合、可伸缩的高可信嵌入式系统基础软件开发和形式化验证框架与工具链,并实现了原型系统的开发和实验评估。结果表明,通过采用隔离、硬件保护机制和形式化方法相结合方式,在功能和性能方面可实现满足高可信嵌入式应用安全和可靠性需求的系统软件。并能提供可信的证据,证明软件实现满足系统的功能规约和相关安全属性。为高可信嵌入式系统的开发打下坚实的基础。本学位论文的主要贡献和创新之处有:(1)针对嵌入式系统中安全关键的设备驱动,提出了一种基于分层精化的、可组合、可伸缩的硬件建模及驱动程序验证框架。在证明驱动组件端到端的功能正确性同时,系统性地确保其与其它功能模块相互隔离。(2)为了支持内核中可中断代码的验证,提出了一种基于抽象层的中断建模方法。首先分别刻画与真实硬件行为一致的“硬件中断模型”,和用于验证可中断代码的“抽象中断模型”,然后在二者之间,使用多个抽象层建立起上下文相关的精化(Contextual Refinement)关系,最终证明可中断代码在抽象模型上的正确性,可传递到真实的硬件模型之上。从而解决内核代码与中断向量并发执行,所导致的语义不确定性问题。(3)在驱动验证框架与抽象中断建模方法之上,对高可信操作系统中包括中断控制器在内的多个驱动组件进行了形式验证。找到系统先前开发过程中,存在的多个错误。实现了首个包含驱动程序的可中断内核的形式化验证。(4)针对高可信嵌入式系统中非安全关键驱动的执行,提出了一种基于命令解释器与安全策略检查相结合的高性能安全运行时框架。通过在用户态驱动进程与内核之间建立的命令通道,将所有设备操作转换为对驱动命令解释器的请求。从而实现对驱动行为的安全策略检查和硬件资源的访问控制,完成对不可信系统组件的故障隔离和安全防御。(5)综合运用基于抽象层的形式化验证方法和安全运行时框架的设计理念,针对高可信嵌入式系统中虚拟机监视器(VMM),提出了一种采用硬件辅助虚拟化、安全隔离与形式验证相结合的设计与验证框架。对于VMM中与虚拟机隔离和访问控制直接相关的组件,利用分层精化的验证方法确保其功能正确性。而对于与安全无关的组件,将其置于用户空间,通过安全内核的保护机制,满足客户系统行为的安全属性。(6)整个系统的模型、规约、实现和证明,均统一在交互式定理证明器Coq中完成。正确性可通过机器检查。最终,通过验证框架抽取的代码,所构建的原型系统可在真实硬件上运行,具备了较高的可行性。目前,国内外对高可信嵌入式系统的研究仍然存在许多挑战。本文所提出的技术和方法,对广大研究者提供了一种新的思路,为增强我国自主知识产权的高可信嵌入式系统的研发,提供了理论和技术支持。