Safety checking of machine code
Abstract
We show how to determine statically whether it is safe for untrusted machine code to be loaded into a trusted host system.
Related papers
- A Semantic Model of Types and Machine Instructions for Proof-Carrying Code POPL 2000
- A Dependent Nominal Physical Type System for Static Analysis of Memory in Low Level Code OOPSLA 2024
- AUSPICE-R: Automatic Safety-Property Proofs for Realistic Features in Machine Code APLAS 2016
- The Embedded Machine: Predictable, Portable Real-Time Code PLDI 2002
- The embedded machine: Predictable, portable real-time code TOPLAS 2007
- Enhancing Symbolic Execution with Machine-Checked Safety Proofs CPP 2026
- Machine-checked semantic session typing CPP 2021
- VeriPhy: verified controller executables from verified cyber-physical system models PLDI 2018