Formal Verification Methods for Binary Translation in Embedded Instruction Set Architectures

July 17, 2023

Although memory corruption vulnerabilities have been extensively studied, effective mitigation strategies are still not universally available, particularly in deeply embedded systems with constrained hardware resources, heterogeneous development stacks, and various instruction set architectures. Additionally, in functional-safety relevant systems, changing the development stack (e.g., switching to a newer compiler) may not be feasible. Binary translation offers a practical solution, but the modified binary must maintain its intended functionality.

We present a binary translation approach to enable architecture-generic exploit mitigations and hardened code obfuscation transformations tailored to embedded systems. We incorporate formal verification methods into our development stack to ensure the translation correctness and effectiveness. We discuss the systems and tools required, such as on-device debugging and code-streaming operating systems, for successful translation and verification. Additionally, we address handling, unification, and comparison testing of various instruction semantics description sources, demonstrating the effectiveness of our approach through practical use cases.

Presentation summary:

  • Binary rewriting is a complex, multi-staged process
  • Requirement for large-scale validation and testing
  • Translation validation, fuzzing, formal verification

Download presentation slides

We send out regular updates on new releases, industry insights and technical case studies

Privacy policy

ยฉ 2023 emproof B.V. All rights reserved. Design by Kava. Privacy PolicyTerms and ConditionsISO 26262 (ASIL B) certification