Security of Multithreaded Programs by Compilation

Information security is a pressing challenge for mobile code technologies. In order to claim end-to-end security of mobile code, it is necessary to establish that the code neither intentionally nor accidentally propagates sensitive information to an adversary. Although mobile code is commonly multithreaded low-level code, the literature is lacking enforcement mechanisms that ensure information security for such programs. This paper offers a modular solution to the security of multithreaded programs. The modularity is three-fold: the authors give modular extensions of sequential semantics, sequential security typing, and sequential security-type preserving compilation that allow them enforcing security for multithreaded programs.