Change search
ReferencesLink to record
Permanent link

Direct link
Machine Code Verification of a Tiny ARM Hypervisor
KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.ORCID iD: 0000-0001-5432-6442
KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.ORCID iD: 0000-0001-9251-3679
2013 (English)Conference paper (Refereed)
Abstract [en]

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.
Keyword [en]
Binary Verification; Hypervisor
National Category
Computer Science
URN: urn:nbn:se:kth:diva-136351DOI: 10.1145/2517300.2517302ScopusID: 2-s2.0-84889071512ISBN: 978-1-4503-2486-1OAI: diva2:675838
TrustED 13, November 4 2013, Berlin, Germany

Qc 20131216

Available from: 2013-12-04 Created: 2013-12-04 Last updated: 2013-12-16Bibliographically approved

Open Access in DiVA

trusted13_dam_prosper_machine_code_verification.pdf(432 kB)312 downloads
File information
File name FULLTEXT01.pdfFile size 432 kBChecksum SHA-512
Type fulltextMimetype application/pdf

Other links

Publisher's full textScopus

Search in DiVA

By author/editor
Dam, MadsGuanciale, RobertoNemati, Hamed
By organisation
Theoretical Computer Science, TCS
Computer Science

Search outside of DiVA

GoogleGoogle Scholar
Total: 312 downloads
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

Altmetric score

Total: 362 hits
ReferencesLink to record
Permanent link

Direct link