Hypervisor

[Google Scholar]

  • Automated verification of a small hypervisor [alkassar:vstte:2010]
  • A high assurance virtualization platform for ARMv8 [baumann:eucnc:2016]
  • Combining mechanized proofs and model-based testing in the formal analysis of a hypervisor [becker:fm:2016]
  • A case study on formal verification of the Anaxagoros hypervisor paging system with Frama-C [blanchard:fmics:2015]
  • Local verification of global invariants in concurrent programs [cohen:cav:2010]
  • Machine code verification of a tiny ARM hypervisor [dam:ted:2013]
  • Machine code verification of a tiny ARM hypervisor [dam:trusted:2013]
  • Attacking, repairing, and verifying SecVisor: A retrospective on the security of a hypervisor [franklin:cmu:2008]
  • CertiKOS: An extensible architecture for building certified concurrent OS Kernels [gu:osdi:2016]
  • Verifying the Microsoft Hyper-V hypervisor with VCC [leinenbach:fm:2009]
  • A secure and formally verified Linux KVM hypervisor [li:sandp:2021]
  • Formally verified memory protection for a commodity multiprocessor hypervisor [li:usenix:2021]
  • VMSL: A separation logic for mechanised robust safety of virtual machines communicating above FF-A [liu:pldi:2023]
  • Vx86: x86 assembler simulated in C powered by automated theorem proving [maus:amast:2008]
  • Design of a symbolically executable embedded hypervisor [nordholz:eurosys:2020]
  • Toward confidential cloud computing: Extending hardware-enforced cryptographic protection to data while in use [russinovich:acmq:2021]
  • Integrated semantics of intermediate-language C and macro-assembler for pervasive formal verification of operating systems and hypervisors from VerisoftXT [schmaltz:vstte:2012]
  • SecVisor: A tiny hypervisor to provide lifetime kernel code integrity for commodity OSes [seshadri:sosp:2007]
  • Formal verification of a multiprocessor hypervisor on Arm relaxed memory hardware [tao:sosp:2021]
  • Design, implementation and verification of an extensible and modular hypervisor framework [vasudevan:secpriv:2013]
  • überSpark: Enforcing verifiable object abstractions for automated compositional security analysis of a hypervisor [vasudevan:usenix:2016]