English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Tools annual

Global: Zendy Free Plan

Global: Zendy Tools monthly

Global: Zendy Plus monthly

In order to handle the complexity and heterogeneity of mod- ern instructionset architectures, analysis platforms share a common design, the adoption ofhardware-independent intermediate representa- tions. The usage of theseplatforms to verify systems down to binary-level is appealing due to the highdegree of automation they provide. How- ever, it introduces the need fortrusting the correctness of the translation from binary code to intermediatelanguage. Achieving a high degree of trust is challenging since thistranspilation must handle (i) all the side effects of the instructions, (ii)multiple instruction encoding (e.g. ARM Thumb), and (iii) variable instructionlength (e.g. Intel). We overcome these problems by formally modeling one ofsuch intermediate languages in the interactive theorem prover HOL4 and byimplementing a proof- producing transpiler. This tool translates ARMv8 programsto the in- termediate language and generates a HOL4 proof that demonstrates thecorrectness of the translation in the form of a simulation theorem. We alsoshow how the transpiler theorems can be used to transfer properties verified onthe intermediate language to the binary code.

Sound Transpilation from Binary to Machine-Independent Code