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
Sound transpilation from binary to machine-independent code
KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.ORCID iD: 0000-0001-5311-1781
KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
2017 (English)In: 20th Brazilian Symposium on Formal Methods, SBMF 2017, Springer, 2017, Vol. 10623, p. 197-214Conference paper (Refereed)
Abstract [en]

In order to handle the complexity and heterogeneity of modern instruction set architectures, analysis platforms share a common design, the adoption of hardware-independent intermediate representations. The usage of these platforms to verify systems down to binary-level is appealing due to the high degree of automation they provide. However, it introduces the need for trusting the correctness of the translation from binary code to intermediate language. Achieving a high degree of trust is challenging since this transpilation must handle (i) all the side effects of the instructions, (ii) multiple instruction encoding (e.g. ARM Thumb), and (iii) variable instruction length (e.g. Intel). We overcome these problems by formally modeling one of such intermediate languages in the interactive theorem prover HOL4 and by implementing a proof-producing transpiler. This tool translates ARMv8 programs to the intermediate language and generates a HOL4 proof that demonstrates the correctness of the translation in the form of a simulation theorem. We also show how the transpiler theorems can be used to transfer properties verified on the intermediate language to the binary code.

Place, publisher, year, edition, pages
Springer, 2017. Vol. 10623, p. 197-214
Series
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), ISSN 0302-9743 ; 10623
Keywords [en]
Binary analysis, Formal verification, Proof producing analysis, Theorem proving
National Category
Embedded Systems
Identifiers
URN: urn:nbn:se:kth:diva-219665DOI: 10.1007/978-3-319-70848-5_13Scopus ID: 2-s2.0-85035086144ISBN: 9783319708478 OAI: oai:DiVA.org:kth-219665DiVA, id: diva2:1165002
Conference
20th Brazilian Symposium on Formal Methods, SBMF 2017, Recife, Brazil, 29 November 2017 through 1 December 2017
Note

QC 20171212

Available from: 2017-12-12 Created: 2017-12-12 Last updated: 2017-12-12Bibliographically approved

Open Access in DiVA

No full text in DiVA

Other links

Publisher's full textScopus

Authority records BETA

Lindner, AndreasGuanciale, Roberto

Search in DiVA

By author/editor
Lindner, AndreasGuanciale, Roberto
By organisation
Theoretical Computer Science, TCS
Embedded Systems

Search outside of DiVA

GoogleGoogle Scholar

doi
isbn
urn-nbn

Altmetric score

doi
isbn
urn-nbn
Total: 26 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