Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • 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
TrABin: Trustworthy analyses of binaries
KTH, School of Electrical Engineering and Computer Science (EECS), Theoretical Computer Science, TCS.ORCID iD: 0000-0001-5311-1781
KTH, School of Electrical Engineering and Computer Science (EECS), Theoretical Computer Science, TCS.
2019 (English)In: Science of Computer Programming, ISSN 0167-6423, E-ISSN 1872-7964, Vol. 174, p. 72-89Article in journal (Refereed) Published
Abstract [en]

Verification of microkernels, device drivers, and crypto routines requires analyses at the binary level. In order to automate these analyses, in the last years several binary analysis platforms have been introduced. These platforms share a common design: the adoption of hardware-independent intermediate representations, a mechanism to translate architecture dependent code to this representation, and a set of architecture independent analyses that process the intermediate representation. The usage of these platforms to verify software introduces the need for trusting both the correctness of the translation from binary code to intermediate language (called transpilation) and the correctness of the analyses. Achieving a high degree of trust is challenging since the transpilation must handle (i) all the side effects of the instructions, (ii) multiple instruction encodings (e.g. ARM Thumb), and (iii) variable instruction length (e.g. Intel). Similarly, analyses can use complex transformations (e.g. loop unrolling) and simplifications (e.g. partial evaluation) of the artifacts, whose bugs can jeopardize correctness of the results. We overcome these problems by developing a binary analysis platform on top of the interactive theorem prover HOL4. First, we formally model a binary intermediate language and we prove correctness of several supporting tools (i.e. a type checker). Then, we implement two proof-producing transpilers, which respectively translate ARMv8 and CortexM0 programs to the intermediate language and generate a certificate. This certificate is a HOL4 proofdemonstrating correctness of the translation. As demonstrating analysis, we implement a proof-producing weakest precondition generator, which can be used to verify that a given loop-free program fragment satisfies a contract. Finally, we use an AES encryption implementation to benchmark our platform.

Place, publisher, year, edition, pages
Elsevier, 2019. Vol. 174, p. 72-89
Keywords [en]
Binary analysis, Formal verification, Proof producing analysis, Theorem proving
National Category
Computer Systems
Identifiers
URN: urn:nbn:se:kth:diva-246462DOI: 10.1016/j.scico.2019.01.001ISI: 000461533200003Scopus ID: 2-s2.0-85060511323OAI: oai:DiVA.org:kth-246462DiVA, id: diva2:1297984
Projects
Trustfull
Note

QC 20190321

Available from: 2019-03-21 Created: 2019-03-21 Last updated: 2019-10-04Bibliographically 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
In the same journal
Science of Computer Programming
Computer Systems

Search outside of DiVA

GoogleGoogle Scholar

doi
urn-nbn

Altmetric score

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

Direct link
Cite
Citation style
  • apa
  • 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