Association for Computing Machinery
The authors have designed and implemented ARMor, a system that uses Software Fault Isolation (SFI) to sandbox application code running on small embedded processors. Sandboxing can be used to protect components such as the RTOS and critical control loops from other, less-trusted components. ARMor guarantees memory safety and control flow integrity; it works by rewriting a binary to put a check in front of every potentially dangerous operation. They formally and automatically verify that an ARMored application respects the SFI safety properties using the HOL theorem prover.