Security types preserving compilation

Abstract

Initiating from the seminal work of Volpano and Smith, there has been ample evidence that type systems may be used to enforce confidentiality of programs through non-interference. However, most type systems operate on high-level languages and calculi, and “low-level languages have not received much attention in studies of secure information flow” (Sabelfeld and Myers, [16]). Further, security type systems for low-level languages should appropriately relate to their counterparts for high-level languages; however, we are not aware of any study of typepreserving compilers for type systems for information flow. In answer to these questions, we introduce a security type system for a low-level language featuring jumps and calls, and show that the type system enforces termination-insensitive non-interference. Then, we introduce a compiler from a high-level imperative programming language to our low-level language, and show that the compiler preserves security types.