We study type systems for guaranteeing secure information flow in assembly languages. Earlier work has shown that type systems for high-level languages can guarantee confidentiality of local data accessed by untrusted software, but no such results have been established for realistic low-level languages. Low-level languages lack control-flow structures that guide static analysis, and they include operations for explicit management of the control stack that make it possible to leak confidential information. Our work addresses these issues and shows that the approach used for secure information flow in high-level languages can be adapted to low-level languages as well.

 

The key property we study is non-interference, that no public output of a program is affected by secret data it may have accessed. Non-interference can be shown sound for natural type systems of low-level programs, yielding efficient, static procedures that can be used by clients to verify non-interference of untrusted code.