【文献心得】Hypervisor 技术、安全

[1]肖伟民,邓浩江,孙鹏.嵌入式虚拟化技术研究综述[J].网络新媒体技术,2019,8(02):9-18.

​​https://www.jianshu.com/p/d808b8e6c917​​

计算机系统包括五个抽象层：硬件抽象层，指令集架构层，操作系统层，库函数层和应用程序层。虚拟化可以在每个抽象层来实现。

在系统虚拟化中，虚拟机（VM）是在一个硬件平台上模拟一个或者多个独立的和实际底层硬件相同的执行环境。

虚拟化技术是将计算机的各种实体资源，予以抽象、转换后创建某种特定虚拟对象的做法，包括虚拟的计算机硬件平台、存储设备和计算机网络资源等，该技术通过在软件和硬件中间引进一个新的虚拟化层，将宿主机的各种资源进行逻辑的抽象转换，实现了软硬件分离。用户无需关注硬件的具体实现即可在虚拟化的操作系统环境中运行应用程序，提高了资源的利用率和安全性。

虚拟化技术的发展阶段：

1. 硬件仿真技术。在宿主机操作系统上创建一个硬件VM来仿真所想要的硬件。采用该技术，甚至可以运行多个虚拟机，每个虚拟器仿真一个不同架构的处理器。WindRiver Simics、QEMU、Bochs。
2. 完全虚拟化技术。不对底层硬件资源进行划分分区，通过 Host 系统进行虚拟化，通过VMM来管控虚拟机。典型代表有 VirtualBox，Virtual Iron，IBM z/VM，Virtual PC，Hyper-V，VMware Workstation，VMware Server (formerly GSX Server)，Adeos，Mac-on-Linux以及Egenera vBlade technology等。为用户提供了完整的相互独立的虚拟化硬件资源，缺点是：VMM 需要消耗大量资源，物理主机开销大。
3. 半虚拟化技术。是指通过暴露给Guest OS一个修改过的硬件抽象，将硬件接口以软件的形式提供给客户机操作系统。这可以通过Hypercall（VMM提供给GuestOS的直接调用，与系统调用类似）的方式来提供。能够改善虚拟化的性能，通过定制的虚拟机操作系统使得其可以与 VMM 通信，协同工作，并对指令进行了优化，典型代表为早期的 XEN。并且半虚拟化技术修改了Guest OS与虚拟机监控器协同工作，使得虚拟机监控器可以得知Guest OS内部的一些状态，消除了黑盒调度带来的一些问题。优点是：提高了虚拟化的性能和系统效率，缺点是：由于其需要对虚拟机操作系统进行修改，增加了系统设计复杂性。
4. 硬件辅助虚拟化技术。硬件辅助虚拟化技术是指借助硬件（CPU、芯片组以及I/O设备等）的虚拟化支持来实现高效的全虚拟化。原有的硬件体系结构在虚拟化方面存在虚拟化漏洞等缺陷，导致单纯的软件虚拟化方法存在一些问题；还有就是由于硬件架构的限制，某些功能即使可以通过软件的方式来实现，但是实现过程却异常复杂，甚至带来性能的大幅下降，这主要体现在以软件方式实现的内存虚拟化和I/O设备虚拟化。通过在硬件中加入专门针对虚拟化的支持，系统虚拟化的实现变得更加容易和高效。例如，在Intel VT技术的支持下，Guest OS和VMM的执行环境可以自动地完全隔离开来，Guest OS有自己的“全套寄存器”，可以直接运行在最高级别。采用该技术的虚拟化平台有Linux KVM， VMware Workstation， VMware Fusion， Microsoft Virtual PC， Xen， Parallels Desktop for Mac，VirtualBox and Parallels Workstation。

5. 不在硬件平台，而是在操作系统层进行虚拟化 —— 操作系统虚拟化。所有虚拟机共享同一个操作系统实例，涉及轻量级虚拟化技术和容器化技术，OpenVZ、Sun Solaris Container 和 Linux 内核容器（LXC，通过控制组实现基于进程组的资源隔离，采用命名空间就为每个容器提供特定的命名空间，实现进程级别的隔离）等。

   1、所有容器共享同一操作系统内核，资源浪费和性能损耗较小；

   2、容器可根据需要获取资源，不会造成资源浪费；

   3、不需要操作系统和硬件资源间的指令集模拟和转换，提高系统性能；

   4、LXC 的特性由 Linux 内核提供，带来更小的虚拟化开销；

   5、LXC 提供管理工具，可以快速部署；

嵌入式虚拟化技术。是指通过在嵌入式系统部署虚拟机或容器监控程序，使得嵌入式系统硬件上能够支持多种类型的、相互隔离的客户操作系统。方案：开源社区 Open Kernel Lab 提出的 OKL4 Microvisor（半虚拟化）、NOVA（全面虚拟化）、Codezero、XEN on ARM（全虚拟化、半虚拟化）、KVM for ARM（全虚拟化、半虚拟化）、Xvisor（全虚拟化、半虚拟化）。

嵌入式Docker容器技术

Docker 扩展了 LXC 和应用层的接口，使进程隔离运行，隔离的进程资源包括 CPU、内存、I/O、网络等；通过采用命名空间实现底层操作环境的彻底隔离，包括进程树、网络、用户ID 和文件系统；具备镜像的自动化构建与便捷快速部署组件复用、容器共享、类似 git 的版本控制。

嵌入式 Docker 容器技术作为嵌入式虚拟化技术的典型代表，解决方案：RancherOS、HypriotOS、ResinOS。

以 Docker 容器技术为代表的轻量级虚拟化技术能够有效缓解嵌入式虚拟化给系统带来的性能下降、资源利用率低、额外开销大等问题。Docker 容器技术在应用的快速部署、容器数量及并发性方面更具有优势。通过镜像复用，Docker 容器可以共用操作系统和应用程序组件，极大的减轻系统负载，提高资源利用率。因此，基于 Docker 容器技术的轻量级虚拟化技术更适合嵌入式系统虚拟化。

Hypervisor types

Hypervisor types

• VMM 直接运行在没有操作系统的裸机上，具有最高特权级，管理底层所有的硬件资源。所有的Guest OS都运行在较低的特权级中，所有Guest OS对底层资源的访问都被虚拟机监控器拦截，由虚拟机监控器代为操作并返回操作结果，从而实现系统的隔离性，达到对系统资源绝对控制。
• 虚拟机监控器作为一个应用程序运行在宿主机操作系统（Host OS）上，而Guest OS运行于虚拟机监控器之上。Guest OS对底层硬件资源的访问要被虚拟机监控器拦截，虚拟机监控器再转交给Host OS进行处理。

• Type 1: Hyper-V，VMware ESX Server，Citrix XenServer，Oracle OVM for SPARC，KVM；
• Type 2: VMware Server，VMware Fusion，Microsoft Virtual Server，Oracle VM Virtual Box，Oracle VM for x86， Solaris Zones，Parallels，Microsoft Virtual PC。

[1]祝现威. Xen安全模型设计与形式化验证方法研究[D].解放军信息工程大学,2017.

Xen 虚拟化技术将关键性硬件的控制权，从原有运行在硬件上的操作系统转移到了虚拟机监视器层，Xen 中的安全机制大多是通过在 VMM 中添加安全模块来实现对平台和数据的安全保护。

Xen 的安全架构 XSM 参考了 Linux 操作系统中的安全架构 LSM，为实现 Xen 上虚拟机及其资源的调度和访问控制提供的一个安全架构，目前 XSM 支持的安全架构有 Dummy、ACM 和 Flask 三种。Dummy 是强隔离机制，使虚拟机间不产生信息流动，ACM 和 Flask 是通过安全策略限制具有冲突关系的虚拟机间的信息流动。

XSM 是通过在 Xen 中加入钩子实现的，XSM 在 Xen 中定义了几组函数指针，每组函数指针的集合称为 Hook，实现原理是 XSM 将所要执行的钩子函数放在其对应的敏感操作之前，实现 XSM 的安全策略。

1. ACM 安全架构

   又称为 sHype，是一个为解决 Xen 虚拟机多用户间的冲突而设计的一个冲突模型，其实现原理类似于容器，将相互冲突的虚拟机划分为同一集合。解决了不同虚拟机间的访问冲突问题，并且部分实现了虚拟机间的机密性，但是其安全策略的灵活性较低无法适应多种安全访问方式，并且访问方式限制的过为严格，甚至会影响系统的正常运行。

1. STE 模型（Simple Type Enforcement）

   主要对象为虚拟机及虚拟机所对应的资源。

2. CW 模型（Chinese Wall）

   制定了一组安全策略来定义和限制主体对客体的访问，要求主体不能访问同一冲突集中的客体。CW 通过定义的冲突集判断不同虚拟机是否能够在同一主机上运行。当创建一个新的虚拟机时，首先查找其所在的冲突集，在该冲突集中判断是否有虚拟机在运行，如果在同一冲突集中存在运行的虚拟机则该虚拟机不允许创建，否则

   允许创建。

1. Flask 安全架构

   Xen 将 Flask 体系结构从 SELinux 移植到了 XSM 中，它将策略执行和策略判断分开，具有很强的灵活性和扩展性。Flask 由客体管理器和安全服务器组成，客体管理器主要有安全策略执行和主客体标签分配两个功能，安全服务器对主体访问行为进行判断并给出访问策略。主体访问客体时客体管理器将主客体的安全标识发送给安全服务器，安全服务器查找到安全策略，并返回给客体管理器执行。

2. Xen 的增强安全架构 Xenon

   内核隔离实现虚拟机间隔离。MLS 安全模型。

3. 基于 Xen 的 BLP 模型

   当一个虚拟机访问另一个虚拟机时，通过在 VMM 的路径代码处插入钩子函数，钩子函数访问 Police Manager 判断该访问行为能否执行。

传统操作系统安全标准，使用经过形式化证明的可信的开发环境和流程，并提供可证明安全模型来达到其标准所声称的安全等级：

• 形式化评估标准：（TCSEC）《可信计算机系统评价标准》。提出安全功能和安全确信度两个概念。
• 面向标准开发的安全标准：计算机安全评价标准联邦标准。
• 面向工程实践的安全标准：信息安全评价国际通用标准。
• 操作系统安全评估标准 GB-17859、GB/T18336。

形式化验证：

形式化方法是指基于数理逻辑和逻辑语言来描述和验证软件和硬件的方法。利用形式化方法对目标系统及其模型进行验证，主要通过数学建模来描述目标系统的行为和语义，建立形式化模型，验证其实现特定的功能和满足安全要求。提供了一种数学评估的手段，是他们能够严格的刻画系统，被广泛的应用于系统安全评价标准中。

对于安全模型来说，主要的形式化验证手段是模型检测和演绎证明。

• 模型检测是利用系统问题建立数学模型，对系统的状态空间进行遍历，以判定规范的真假，其证明过程可以自动化证明。但是由于是对系统的状态空间进行遍历，要防止状态空间膨胀，模型检测只能应用于有限状态的并行系统中。
• 演绎证明一般采用交互式的定理辅助证明器对系统进行抽象描述，依赖系统的定理和公理来表达系统功能和安全性。

1. 提出系统建模框架，对目标模型进行描述；
2. 选择对验证安全模型的性质进行描述的规范语言；
3. 对系统性质的描述是否满足规范验证进行确认；

存在问题：

1. 传统操作系统的安全标准在结构和内容上与云计算安全标准有许多共通点，但由于云计算多用户、可迁移等特性使其与传统安全标准有许多不同，如何面对这种既有一致性又有区别的两种系统安全标准，也是开发人员要面对的重要问题。
2. 现阶段安全模型都是以虚拟机作为元单位，没有实现虚拟机的细粒度管理，违反最小特权原则。对安全模型的形式化是保证安全模型一致性的基础工作，安全模型形式化不仅要求开发人员具有深刻的模型设计理论，还要拥有坚实的数理逻辑功底。在形式化方面安全模型的形式化工作还是一个较为艰巨的工作。
3. 形式化方法可以最大程度的保证安全架构的正确性和一致性。由于模块化形式化建模方法的缺乏和开发效率的考虑，开发人员往往对安全模型和安全架构实行一体化证明，但是在实际应用中由于抽象层次、复杂性和规模上以及编程逻辑和应用逻辑的不同而导致安全模型和安全架构无法进行统一的建模。

[1]陈剑锋,王强,王剑锋.云计算虚拟环境的形式化安全验证[J].信息安全与通信保密,2012(04):64-66.

==目前针对云计算虚拟环境多采用传统的覆盖使验证方法，无法彻底解决正确性问题。==形式化方法的基本含义是借助数学的方法来研究计算机与数学科学问题，在系统构建、实现的全过程中，凡是采用严格的数学语音，具有精确的数学语义的方法，都可以称之为形式化方法。

模型检测技术：

• 1、配置采集。元素集合、谓词逻辑的实例化过程。
• 2、需求分析。得到形式化语言刻画的安全性质语句，一般也用逻辑命题的形式表述。
• 3、性质检测。检测器将算法选项参数初始化，并输入待检测的语句作为未知命题进行演算，穷举模型空间里的谓词和给定事实，寻找能够匹配的规则，将命题进一步分解，直到能够成功求值并返回演算结果，整个计算过程在遍历了整棵演算树后结束，根据获得的中间结果组合成最终返回值，给出是、否、系统异常三个结论。

[1]钱汉伟,王承毅.操作系统形式化验证综述[J/OL].河海大学学报(自然科学版):1-10[2021-07-28].http://kns.cnki.net/kcms/detail/32.1117.TV.20201218.1650.012.html.

支撑理论和框架：目前操作系统的形式化验证是用定理证明的方法对操作系统的性质规约进行验证。性质规约描述的逻辑基础是霍尔逻辑，并以此为基础进行扩展的分离逻辑、并发分离逻辑和并发精化程序逻辑。

• 霍尔逻辑。证明规约用形如​

  ​{Pre}P{Post}​

  ​ 的霍尔三元组表示，通过前置后置条件，比如某些不变量，放入程序要证明的性质，实现了用一组公理和一组规则描述程序代码应有的性质。
• 分离逻辑。对霍尔逻辑进行扩展，增加了分离合取和分离蕴含谓词及相应的推导规则，能够以自然的方式来描述计算过程中内存的属性和相关操作，验证指针程序也更加方便。
• 并发精化程序逻辑。将并发分离逻辑的断言语言扩展为关系型断言，更适合证明与多级中断有关的并发程序的上下文精化关系。操作系统验证问题也是精化验证问题，操作系统从底层模型到高层规约之间的一致性验证等问题都是以精化理论为基础。

形式化验证工具。 ==操作系统的验证问题都将转成定理证明问题，解决定理证明问题最终依赖于定理证明器。==目前广泛应用于操作系统验证的定理证明器有 Z3、Isabelle、Coq。可信编译器有 CompCert C，它严格保证了源代码和编译之后机器码之间的语义一致性，使得在源码层验证的定理很容易扩展到机器码层。如果验证用了 C 语言编写的操作系统源代码，通过可行编译器生成的相应机器码也可以被认为是通过验证了。选用微内核操作系统作为验证对象是减少验证规模的一个重要方法，目前操作系统验证工作取得一定成果的 seL4、mC2、PikeOS、uC/OS-Ⅱ。

现状。Verve 微软基于类型化汇编语言和霍尔逻辑，第一个证明了类型安全和内存安全操作系统。PikeOS、SeL4、CertiKOS、uC/OS-Ⅱ（仅证明了该系统互斥锁不会发生优先级反转，一共验证了1400行左右的C代码，证明器验证脚本量 225000 行）。

1. 操作系统过于复杂。
2. 验证成本高。验证 1 行 C 代码平均需要 25 行左右的证明代码，以μC/OS-II 系统内核的验证为例，1400 行 C 代码用了 22 万行 Coq 脚本代码，其中包括验证框架约 6 万行，证明库约 11 万行，代码证明约 4 万行，证明策略约 1.5 万行，共约 6 人年的工作量。
3. 专业人员少。形式化验证工作全部依赖于非常专业的人员，除了需要具有深厚的形式化理论功底，丰富的证明工具使用经验，还要对验证的软件有深刻的了解，过高的门槛使得这样的专业人员非常稀缺。