Security of multithreaded programs by compilation

Information security is a pressing challenge for mobile code technolo- gies. In order to claim end-to-end security of mobile code, it is necessary to es- tablish 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 in- formation security for such programs. This paper offers a modular solution to the security of multithreaded programs. The modularity is three-fold: we give modu- lar extensions of sequential semantics, sequential security typing, and sequential security-type preserving compilation that allow us enforcing security for multi- threaded programs. Thanks to the modularity, there are no more restrictions on multithreaded source programs than on sequential ones, and yet we guarantee that their compilations are provably secure for a wide class of schedulers.