Heiko Mantel and Andrei Sabelfeld
The security of computation at the level of a specific programminglanguage and the security of complex systems ata more abstract level are two major areas of current securityresearch. With the objective to integrate the two, thisarticle proposes a translation of a timing-sensitive securityproperty for simple multi-threaded programs into a moregeneral security framework. Interestingly, our notion of securityfor programs is bisimulation-based while the securityframework is trace-based. Nevertheless, we show thatthe translation is sound and complete in the sense that thetrace-based specification which results from the translationof a multi-threaded program is secure if and only if the originalprogram is secure. The translation is presented as atwo-step process where the first step is independent fromthe concrete programming language.