Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
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, Published 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
Identifiers
URN: urn:nbn:se:kth:diva-136351DOI: 10.1145/2517300.2517302Scopus ID: 2-s2.0-84889071512ISBN: 978-1-4503-2486-1 (print)OAI: oai:DiVA.org:kth-136351DiVA: diva2:675838
Conference
TrustED 13, November 4 2013, Berlin, Germany
Note

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)392 downloads
File information
File name FULLTEXT01.pdfFile size 432 kBChecksum SHA-512
57f1c4894c6bc53aea3765c5d04e66075227e275567252abd3842cc2d71b01b39ef07ab0041f574517486da3652fe8dc180987da902dce4eefdff729d7a6db28
Type fulltextMimetype application/pdf

Other links

Publisher's full textScopus

Authority records BETA

Dam, MadsNemati, Hamed

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: 392 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

doi
isbn
urn-nbn

Altmetric score

doi
isbn
urn-nbn
Total: 1080 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf