Machine Code Verification of a Tiny ARM Hypervisor
2013 (English)Conference paper (Refereed)
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.
Place, publisher, year, edition, pages
ACM Press, 2013.
Binary Verification; Hypervisor
IdentifiersURN: urn:nbn:se:kth:diva-136351DOI: 10.1145/2517300.2517302ScopusID: 2-s2.0-84889071512ISBN: 978-1-4503-2486-1OAI: oai:DiVA.org:kth-136351DiVA: diva2:675838
TrustED 13, November 4 2013, Berlin, Germany
Qc 201312162013-12-042013-12-042013-12-16Bibliographically approved