×

zbMATH — the first resource for mathematics

Noninterference for concurrent programs and thread systems. (English) Zbl 0997.68022
Summary: We propose a type system to ensure the property of noninterference in a system of concurrent programs, described in a standard imperative language enriched with parallelism. Our proposal is in the line of some recent work by Irvine, Volpano and Smith. Our type system seems more natural and less restrictive than that originally presented by these authors for the concurrent case. Moreover, we show how to extend the language in order to formalise scheduling policies for systems of sequential threads. The type system is extended to the new constructs, and we show that noninterference still holds, while remaining in a nonprobabilistic setting.

MSC:
68N19 Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.)
Software:
JFlow
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Abadi, M., Secrecy by typing in security protocols, Journal of the ACM, 46, 5, 749-786, (1999) · Zbl 1064.94542
[2] J. Agat, Transforming out timing leaks, in: 27th ACM Symposium on Principles of Programming Languages (POPL), 2000, pp. 40-53. · Zbl 1323.68399
[3] P. Bieber, J. Cazin, V. Wiels, G. Zanon, P. Girard, J.-L. Lanet, Electronic purse applet certification (extended abstract), in: Workshop on Secure Architectures and Information Flow, ENTCS, Vol. 32, 2000. · Zbl 0959.68506
[4] G. Boudol, I. Castellani, Noninterference for concurrent programs, in: ICALP’01, Lecture Notes in Computer Science, Vol. 2076, 2001, pp. 382-395. · Zbl 0986.68012
[5] R. Focardi, R. Gorrieri, F. Martinelli, Non interference for the analysis of cryptographic protocols, in: Proceedings ICALP’00, Lecture Notes in Computer Science, Vol. 1853, 2000. · Zbl 0973.94517
[6] J.A. Goguen, J. Meseguer, Security policies and security models, in: Proceedings 1982 IEEE Symposium on Security and Privacy, 1982, pp. 11-20.
[7] M. Hennessy, The security π-calculus and noninterference, Computer Science Technical Report 2000:05, University of Sussex, 2000.
[8] M. Hennessy, J. Riely, Information flow vs. resource access in the asynchronous pi-calculus (extended abstract), in: Proceedings ICALP’00, Lecture Notes in Computer Science, Vol. 1853, 2000. · Zbl 0973.68519
[9] K. Honda, V. Vasconcelos, N. Yoshida, Secure information flow as typed process behaviour, in: Proceedings ESOP’00, Lecture Notes in Computer Science, Vol. 1782, 2000, pp. 180-199. · Zbl 0960.68126
[10] J. Millen, 20 years of covert channel modeling and analysis, in: IEEE Symposium on Security and Privacy, 1999.
[11] Milner, R., A calculus of communicating systems, Lecture notes in computer science, Vol. 92, (1980), Springer Berlin
[12] A. Myers, Jflow: practical mostly-static information flow control, in: 26th ACM Symposium on Principles of Programming Languages (POPL), 1999.
[13] D. Park, Concurrency and automata on infinite sequences, in: Proceedings 5th GI-Conf. on Theoretical Computer Science, Lecture Notes in Computer Science, Vol. 104, 1981. · Zbl 0457.68049
[14] F. Pottier, S. Conchon, Information flow inference for free, in: Proceedings ICFP’00, 2000. · Zbl 1321.68158
[15] Ryan, P.Y.A.; Schneider, S.A., Process algebra and non-interference, Journal of computer security, 9, 1/2, (2001)
[16] A. Sabelfeld, D. Sands, Probabilistic noninterference for multi-threaded programs, in: IEEE, 13th Computer Security Foundations Workshop, 2000.
[17] G. Smith, A new type system for secure information flow, in: 14th IEEE Computer Security Foundations Workshop, 2001.
[18] G. Smith, D. Volpano, Secure information flow in a multi-threaded imperative language, in: ACM, Proceedings POPL ’98, ACM Press, 1998, pp. 355-364.
[19] D. Volpano, G. Smith, A type-based approach to program security, in: TAPSOFT’97, Lecture Notes in Computer Science, Vol. 1214, 1997, pp. 607-621.
[20] Volpano, D.; Smith, G., Probabilistic noninterference in a concurrent language, Journal of computer security, 7, 2-3, (1999)
[21] Volpano, D.; Smith, G.; Irvine, C., A sound type system for secure flow analysis, Journal of computer security, 4, 3, 167-187, (1996)
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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.