当前的商用操作系统不断地被曝出各种各样的安全漏洞,攻击者能够通过攻击商用操作系统影响到安全代码的执行。为解决上述问题,研究人员提出了屏蔽系统,即一种可用来保护安全代码的软硬件系统。具体而言,屏蔽系统保护安全代码的两大属性-（1）机密性:安全代码的执行过程对于商用操作系统而言是不可见的。商用操作系统只能观察到此代码的输入和输出;（2）完整性:商用操作系统不能影响受保护代码的行为。一旦安全代码执行完成,代码的输出应与在其预期的参考输出相同。典型的屏蔽系统有基于hypervisor的TrustVisor,基于ARM TrustZone的TrustICE和基于硬件的Intel SGX技术等。屏蔽系统会使用在系统中比商用操作系统更高权限的核心管理模块来绕过操作系统保护安全代码。随着屏蔽系统的商业化,屏蔽系统的安全性越来越受重视。目前,尽管屏蔽系统的代码量远小于商用操作系统,屏蔽系统仍有存在漏洞的可能,这使得攻击者仍有机会危害到安全代码的执行。为此,一个重要的解决方案是对屏蔽系统进行形式化地安全分析。形式化分析方法通过建立理论模型和进行理论推导,能够在安全属性不完备时提供理论证据,或者证明安全属性的完备性。为软硬件系统提供形式化分析是目前安全性分析领域解决软硬件系统安全问题的一个重要手段。本文基于逐层精化的形式化分析方法围绕屏蔽系统安全性分析开展研究,取得以下成果:（1）提出了屏蔽系统数据机密性形式化分析方法。安全代码私密数据的安全性至关重要。例如,对于指纹解锁程序而言,其指纹数据一旦泄露,会给解锁程序的使用者带来极大的危害。因此,屏蔽系统需要确保安全代码私密数据不能够被攻击者获取。本方法支持分析多种屏蔽系统的数据机密性,如基于虚拟化扩展的屏蔽系统和基于ARM TrustZone的屏蔽系统。本方法构建了屏蔽系统在数据访问和数据加解密方面的普适形式化约束,并证明了这些约束能够抵抗住一个Dolev-Yao类型攻击者的攻击。本方法通过证明具体屏蔽系统是这些普适约束的精化,从而证明这些系统的数据私密性。本文用此方法分析了屏蔽系统TrustVisor和屏蔽系统OSP,并发现了这两个系统设计上的安全缺陷。（2）提出了屏蔽系统数据连续性形式化分析方法。针对特定的安全代码,其关键数据如果被攻击者用旧版本数据所替换,其使用效果可能受到极大的影响。例如,银行账目结算程序中的账目如果能够被攻击者回滚,就可能会导致银行用户产生损失。因此,屏蔽系统需要确保安全代码的关键数据始终处于最新的版本或者是一个可容忍的旧版本。本方法支持分析多种屏蔽系统状态连续性保护方案,如基于单调计数器的保护方案和基于历史记录的保护方案。本方法构建了屏蔽系统在数据存储和断电处理方面的普适形式化约束,并证明了这些约束能够应对一个恶意控制了电源和外部存储器的攻击者。本方法通过证明具体屏蔽系统是这些普适约束的精化,从而证明这些系统的数据连续性。本文用此方法证明了状态连续性保护方案Ariadne和状态连续性保护方案Menoir的状态连续性,展示了本方法的普适性。（3）提出了 ARM平台内存隔离性形式化分析方法。确保不同程序间的内存不可相互访问是很有必要的。因此,ARM平台提供了数据访问控制机制,使得ARM平台上的安全系统能够隔离关键程序之间的内存。本方法支持分析多种ARM平台的内存隔离性,如支持虚拟化扩展的ARM平台和不支持虚拟化扩展的ARM平台。本方法给出了 ARM平台上扩展分页机制和ARM TZASC机制的通用形式化表达,并基于这些表达构建了内存隔离性普适约束,然后证明了这些约束针对任意读写的被隔离程序始终有效。本方法通过证明具体的安全系统是这些普适约束的精化,从而证明这些系统的内存隔离性。本文用此方法从ARM平台的视角证明了屏蔽系统OSP和屏蔽系统TrustICE的内存隔离性,展示了本方法的普适性。