Extensible Certified Software Architecture Of Drone System Based On Virtualization Technology

With the widespread use of drones in the military and civilian fields,the security issues of drones are increasingly being valued by researchers.The formally verified operating system kernel can guarantee the safety aspects of the drone system.However,it has poor extensibility,which means that the drone system cannot provide a rich software development environment for third-party applications.The key problem is improving the extensibility of the drone system while keeping the correctness of the kernel in the same time.A hierarchical software architecture is proposed in the thesis to improve the security and extensibility of the drone system.The software architecture is divided into three parts: operating system kernel,user space and virtual machine.The operating system kernel is called CertiKOS-ARM,which has been formally verified.The flight controller runs in the user space as several real-time processes.A Linux kernel is executed in the virtual machine to provide a powerful runtime environment for third-party applications.Two improvements of the CertiKOS-ARM were made in the thesis: interruptible kernel support and multicore support.Interruptible kernel support decreased the latency of time interrupts,and multicore support ensured the isolation among CPU cores.In order to create and manage the virtual machine,a system software called Hypervisor was designed in the thesis.The Hypervisor proposed in the thesis is called CertiKOS-ARM Hypervisor.CertiKOS-ARM Hypervisor adopted mixed-type architecture which reduced the overhead by using the hardware assisted virtualization technology.The code line of CertiKOS-ARM Hypervisor is much lower than other commercial Hypervisors,so the trusted computed base can keep small size.CertiKOS-ARM Hypervisor has hierarchical code structure which can be applied to both ARM and x86 architecture.Two experiments were designed in the thesis including: performance experiment and flight experiment.A performance analysis tool called LMbench was used to test the performance of CertiKOS-ARM Hypervisor.Three factors were tested including context switching time,IPC latency and file system latency.The results showed that the performance of the virtual machine is nearly the same as the real machine.Another experiment was carried out to demonstrate that the extensibility of the drone system was indeed improved by using this architecture.In addition to the drone system,the hierarchical software architecture proposed in this thesis can also be applied to other intelligent systems.