Certifying Machine Code Safe from Hardware Aliasing: RISC is not necessarily risky
This work addresses the need for certifying machine code safety in embedded systems, but it is incremental as it builds on existing programming memes and focuses on a specific architecture.
The paper tackled the problem of verifying machine code safety from hardware aliasing in embedded systems, and developed an inference system that can prove RISC machine code is provably safe, leveraging its limited memory access instructions.
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.