Specification and static enforcement of scheduler-independent noninterference in a middleweight Java

• We present a multithreaded model language for Java.
• We introduce a timing channel that arises from dynamic dispatch in the presence of multithreading.
• We propose a more permissive scheduler-independent noninterference property.
• We present a security type system to enforce the proposed noninterference property.

We introduce a new timing covert channel that arises from the interplay between multithreading and object orientation. This example motivates us to explore the root of the problem and to devise a mechanism for preventing such errors. In doing so, we first add multithreading constructs to Middleweight Java, a subset of the Java programming language with a fairly rich set of features. A noninterference property is then presented which basically demands program executions be equivalent in the view of whom observing final public values in environments using the so-called high-independent schedulers. It is scheduler-independent in the sense that no matter which scheduler is employed, the executions of the program satisfying the property do not lead to illegal information flows in the form of explicit, implicit, or timing channels. We also give a provably sound type-based static mechanism to enforce the proposed property.