关键词：形式化方法；虚拟化安全；模型；虚拟化软件；信息安全
摘 要：Virtualization software is increasingly a part of the infrastructure behind our online activities.In this work, we investigate the verification of isolation properties for virtualization software.We identify large data structures as one of the biggest challenges in applying traditional formal methods to the verification of isolation properties in virtualization software.