×

Specification and static enforcement of scheduler-independent noninterference in a middleweight Java. (English) Zbl 1387.68050

Summary: 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.

MSC:

68N15 Theory of programming languages
68N19 Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.)
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Volpano, D.; Irvine, C.; Smith, G., A sound type system for secure flow analysis, J Comput Secur, 4, 3, 167-187 (1996)
[5] Barthe, G.; Rezk, T.; Russo, A.; Sabelfeld, A., Security of multithreaded programs by compilation, ACM Trans Inf Syst Secur, 13, 3, 1-32 (2010)
[6] Sabelfeld, A.; Myers, A. C., Language-based information-flow security, IEEE J Sel Areas Commun, 21, 1, 5-19 (2003)
[9] Banerjee, A.; Naumann, D. A., Stack-based access control and secure information flow, J Funct Program, 15, 2, 131-177 (2005) · Zbl 1077.68569
[28] Jacob, B.; Mudge, T., Virtual memory in contemporary microprocessors, IEEE Micro, 18, 4, 60-75 (1998)
[33] Smith, G., Improved typings for probabilistic noninterference in a multi-threaded language, J Comput Secur, 14, 6, 591-623 (2006)
[38] Lux, A.; Starostin, A., A tool for static detection of timing channels in Java, J Cryptogr Eng, 1, 4, 303-313 (2011)
[39] Boudol, G.; Castellani, I., Noninterference for concurrent programs and thread systems, Theor Comput Sci, 281, 1-2, 109-130 (2002) · Zbl 0997.68022
[45] Giffhorn, D.; Snelting, G., A new algorithm for low-deterministic security, Int J Inf Secur, 14, 3, 263-287 (2015)
[47] Igarashi, A.; Pierce, B. C.; Wadler, P., Featherweight Javaa minimal core calculus for Java and GJ, ACM Trans Program Lang Syst, 23, 3, 396-450 (2001)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.