Specification and static enforcement of scheduler-independent noninterference in a middleweight Java. (November 2016)

• Record Type: Journal Article
• Authors: Iranmanesh, Zeinab; Fallah, Mehran S.
• Is Part Of: Computer languages, systems & structures. Volume 46(2016)
• Page Start: 20
• Page End: 43
• Publication Date: 2016-11
• Subjects: Covert channels -- Multithreaded object-oriented programming -- Scheduler-independent noninterference -- Security type systems; Programming languages (Electronic computers) -- Periodicals; Computer networks -- Periodicals; Computer architecture -- Periodicals; Computer systems -- Periodicals; Langage de programmation; Réseau d'ordinateurs; Architecture d'ordinateur; Périodique électronique (Descripteur de forme); Ressource Internet (Descripteur de forme); 005.13
• DOI: 10.1016/j.cl.2016.05.003
• Languages: English
• ISSNs: 1477-8424

Abstract

Abstract: 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. Abstract : Highlights: 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.