Certifying Machine Code Safe from Hardware Aliasing: RISC is not necessarily risky

TL;DR

This paper presents a verification system that certifies RISC machine code as safe from hardware aliasing, demonstrating that RISC architectures are not necessarily risky for embedded system safety.

Contribution

It introduces an inference system capable of proving machine code safety from hardware aliasing, challenging the assumption that RISC architectures are inherently risky.

Findings

The system can certify machine code safety against hardware aliasing.

RISC architecture's limited memory access instructions facilitate verification.

The approach provides provable guarantees of code safety in embedded systems.

Abstract

Sometimes machine code turns out to be a better target for verification than source code. RISC machine code is especially advantaged with respect to source code in this regard because it has only two instructions that access memory. That architecture forms the basis here for an inference system that can prove machine code safe against `hardware aliasing', an effect that occurs in embedded systems. There are programming memes that ensure code is safe from hardware aliasing, but we want to certify that a given machine code is provably safe.