| Unmanned aerial vehicles(UAVs)are used more and more widely in areas related to people’s livelihood,and the consequent security issues cannot be ignored.With the development of the modern Internet,lots of embedded Io T devices are entering thousands of households,and the security of such devices also deserves attention.Such embedded devices usually use ARM or x86 architecture processor,often using the Linux kernel as its underlying operating system.Although such combinations are scalable,security is difficult to guarantee.How to build a software system that is compatible with multiple processor architectures to ensure scalability and security is a topic worth studying.In this dissertation,a lightweight hypervisor module compatible with both x86 and ARM processor architectures is implemented on the basis of the trustworthy OS kernel Certi KOS-multiarch using a hierarchical software design approach.In this way,the whole system architecture is composed of three parts: the kernel,user space,and virtual machine,with the user space running the flying control system and the virtual machine driving the Linux kernel to enhance the scalability of the software system and run customized third-party applications.This dissertation uses the construction of abstraction layers and function tables to mask the differences between the two processor architectures and provide a unified interface for the top-level implementation.The hypervisor implementation uses Virt IO technology to virtualize three devices(block device,network card and console),which not only facilitates cross-platform implementation but also reduces the additional cost of IO.To simplify the interaction between the virtualization module in the kernel and the virtual machine monitor processes in the user space,an instruction ring structure was designed that simplifies the interaction and reduces the effort required for formal verification.To ensure security,the formal verification of the Certi KOS-ARM-based hypervisor was done using a formal verification method based on Deep Spec.The dissertation also designed a series of Hypervisor performance test and security test.The hypervisor was analyzed using the microbenchmark tool LMBench3 and the results showed that the virtual machine kernel running on top of the hypervisor performs as well as the hardware.The security tests show that the hypervisor can effectively isolate trusted and untrusted modules to ensure the security of the kernel system.The proposed cross-platform trustworthy hypervisor module enhances the scalability of the overall software system,ensures the security of the OS kernel,and can be easily generalized to other embedded devices. |