Machine Code Verification of a Tiny ARM Hypervisor

Hypervisors are low level execution platforms that provideisolated partitions on shared resources, allowing to design se-cure systems without using dedicated hardware devices. Akey requirement of this kind of solution is the formal verifi-cation of the software trusted computing base, preferably atthe binary level. We accomplish a detailed verification of anARMv7 tiny hypervisor, proving its correctness at the ma-chine code level. We present our verification strategy, whichmixes the usage of the theorem prover HOL4, the computa-tion of weakest preconditions, and the use of SMT solvers tolargely automate the verification process. The automationrelies on an integration of HOL4 with BAP, the Binary Anal-ysis Platform developed at CMU. To enable the adoption ofthe BAP back-ends to compute weakest preconditions andcontrol flow graphs, a HOL4-based tool was implementedthat transforms ARMv7 assembly programs to the BAP In-termediate Language. Since verifying contracts by comput-ing the weakest precondition depends on resolving indirectjumps, we implemented a procedure that integrates SMTsolvers and BAP to discover all the possible assignments tothe indirect jumps under the contract precondition.Qc 20131216