Formal Verification Methods for Binary Translation in Embedded Instruction Set Architectures
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
|
|
