Abstract
A major difficulty for tracking information flow in multithreaded programs is due to the internal timing covert channel. Information is leaked via this channel when secrets affect the timing behavior of a thread, which, via the scheduler, affects the interleaving of assignments to public variables. This channel is particularly dangerous because, in contrast to external timing, the attacker does not need to observe the actual execution time. This paper presents a compositional transformation that closes the internal timing channel for multithreaded programs (or rejects the program if there are symptoms of other flows). The transformation is based on spawning dedicated threads, whenever computation may affect secrets, and carefully synchronizing them. The target language features semaphores, which have not been previously considered in the context of termination-insensitive security.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Report on resource and information flow security requirements, Deliverable D1.1 of the EU IST FET GC2 MOBIUS project, (March 2006), http://mobius.inria.fr/
Agat, J.: Transforming out timing leaks. In: Proc. POPL 2002, pp. 40–53 (January 2000)
Boudol, G., Castellani, I.: Noninterference for concurrent programs. In: Orejas, F., Spirakis, P.G., van Leeuwen, J. (eds.) ICALP 2001. LNCS, vol. 2076, pp. 382–395. Springer, Heidelberg (2001)
Boudol, G., Castellani, I.: Non-interference for concurrent programs and thread systems. Theoretical Computer Science 281(1), 109–130 (2002)
Denning, D.E., Denning, P.J.: Certification of programs for secure information flow. Comm. of the ACM 20(7), 504–513 (1977)
Focardi, R., Gorrieri, R.: Classification of security properties (part I: Information flow). In: Focardi, R., Gorrieri, R. (eds.) Foundations of Security Analysis and Design. LNCS, vol. 2171, pp. 331–396. Springer, Heidelberg (2001)
Honda, K., Vasconcelos, V., Yoshida, N.: Secure information flow as typed process behaviour. In: Smolka, G. (ed.) ESOP 2000 and ETAPS 2000. LNCS, vol. 1782, Springer, Heidelberg (2000)
Honda, K., Yoshida, N.: A uniform type structure for secure information flow. In: Proc. ACM Symp. on Principles of Programming Languages, pp. 81–92. ACM Press, New York (2002)
Huisman, M., Worah, P., Sunesen, K.: A temporal logic characterisation of observational determinism. In: Proc. IEEE Computer Security Foundations Workshop (July 2006)
JSR 118 Expert Group. Mobile information device profile (MIDP), version 2.0. Java specification request, Java Community Process (November 2002)
JSR 179 Expert Group. Location API for J2ME. Java specification request, Java Community Process (September 2003)
Knudsen, J.: Networking, user experience, and threads. Sun Technical Articles and Tips, (2002), http://developers.sun.com/techtopics/mobility/midp/articles/threading/
Köpf, B., Mantel, H.: Eliminating implicit information leaks by transformational typing and unification. In: Dimitrakos, T., Martinelli, F., Ryan, P.Y.A., Schneider, S. (eds.) FAST 2005. LNCS, vol. 3866, Springer, Heidelberg (2006)
Mahmoud, Q.H.: Preventing screen lockups of blocking operations. Sun Technical Articles and Tips (2004), http://developers.sun.com/techtopics/mobility/midp/ttips/screenlock/
Pottier, F.: A simple view of type-secure information flow in the pi-calculus. In: Proc. IEEE Computer Security Foundations Workshop, pp. 320–330. IEEE Computer Society Press, Los Alamitos (2002)
Russo, A., Sabelfeld, A.: Securing interaction between threads and the scheduler. In: Proc. IEEE Computer Security Foundations Workshop, pp. 177–189. IEEE Computer Society Press, Los Alamitos (2006)
Russo, A., Sabelfeld, A.: Security for multithreaded programs under cooperative scheduling. In: Virbitskaite, I., Voronkov, A. (eds.) PSI 2006. LNCS, vol. 4378, Springer, Heidelberg (2007)
Ryan, P.: Mathematical models of computer security—tutorial lectures. In: Focardi, R., Gorrieri, R. (eds.) FOSAD 2001. LNCS, vol. 2946, Springer, Heidelberg (2004)
Sabelfeld, A.: The impact of synchronisation on secure information flow in concurrent programs. In: Bjørner, D., Broy, M., Zamulin, A.V. (eds.) PSI 2001. LNCS, vol. 2244, Springer, Heidelberg (2001)
Sabelfeld, A., Mantel, H.: Static confidentiality enforcement for distributed programs. In: Hermenegildo, M.V., Puebla, G. (eds.) SAS 2002. LNCS, vol. 2477, Springer, Heidelberg (2002)
Sabelfeld, A., Myers, A.C.: Language-based information-flow security. IEEE J. Selected Areas in Communications 21(1), 5–19 (2003)
Sabelfeld, A., Sands, D.: Probabilistic noninterference for multi-threaded programs. In: Proc. IEEE Computer Security Foundations Workshop, pp. 200–214. IEEE Computer Society Press, Los Alamitos (2000)
Smith, G.: A new type system for secure information flow. In: Proc. IEEE Computer Security Foundations Workshop, pp. 115–125. IEEE Computer Society Press, Los Alamitos (2001)
Smith, G.: Probabilistic noninterference through weak probabilistic bisimulation. In: Proc. IEEE Computer Security Foundations Workshop, pp. 3–13. IEEE Computer Society Press, Los Alamitos (2003)
Smith, G., Volpano, D.: Secure information flow in a multi-threaded imperative language. In: Proc. ACM Symp. on Principles of Programming Languages, pp. 355–364. ACM Press, New York (1998)
Smith, S.F., Thober, M.: Refactoring programs to secure information flows. In: PLAS 2006, pp. 75–84. ACM Press, New York (2006)
Volpano, D., Smith, G.: Probabilistic noninterference in a concurrent language. J. Computer Security 7(2–3), 231–253 (1999)
Volpano, D., Smith, G., Irvine, C.: A sound type system for secure flow analysis. J. Computer Security 4(3), 167–187 (1996)
Winskel, G.: The Formal Semantics of Programming Languages: An Introduction. MIT Press, Cambridge (1993)
Zdancewic, S., Myers, A.C.: Observational determinism for concurrent program security. In: Proc. IEEE Computer Security Foundations Workshop, pp. 29–43. IEEE Computer Society Press, Los Alamitos (2003)
Zheng, L., Chong, S., Myers, A.C., Zdancewic, S.: Using replication and partitioning to build secure distributed systems. In: Proc. IEEE Symp. on Security and Privacy, pp. 236–250. IEEE Computer Society Press, Los Alamitos (2003)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Russo, A., Hughes, J., Naumann, D., Sabelfeld, A. (2007). Closing Internal Timing Channels by Transformation. In: Okada, M., Satoh, I. (eds) Advances in Computer Science - ASIAN 2006. Secure Software and Related Issues. ASIAN 2006. Lecture Notes in Computer Science, vol 4435. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-77505-8_10
Download citation
DOI: https://doi.org/10.1007/978-3-540-77505-8_10
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-77504-1
Online ISBN: 978-3-540-77505-8
eBook Packages: Computer ScienceComputer Science (R0)