Thread algebra for noninterference

Vu, Thuy Duong

RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications, Tome 43 (2009) no. 2, pp. 249-268.

Thread algebra is a semantics for recent object-oriented programming languages [J.A. Bergstra and M.E. Loots, J. Logic Algebr. Program. 51 (2002) 125-156; J.A. Bergstra and C.A. Middelburg, Formal Aspects Comput. (2007)] such as C# and Java. This paper shows that thread algebra provides a process-algebraic framework for reasoning about and classifying various standard notions of noninterference, an important property in secure information flow. We will take the noninterference property given by Volpano et al. [D. Volpano, G. Smith and C. Irvine, J. Comput. Secur. 4 (1996) 167-187] on type systems as an example of our approach. We define a comparable notion of noninterference in the setting of thread algebra. Our approach gives a similar result to the approach of [G. Smith and D. Volpano, in POPL'98 29 (1998) 355-364] and can be applied to unstructured and multithreaded programming languages.

Classification : 68Q60
Mots clés : noninterference, thread algebra, formal methods, security verification

[1] T. Basten, Branching bisimulation is an equivalence indeed. Inform. Process. Lett. 58 (1996) 333-337. | MR | Zbl

[2] D.E. Bell and L.J. La Padula, Secure computer systems: mathematical foundations and model. Tech. Rep. M74-244, MITRE Corporation, Bedford, Massachussets (1973).

[3] J.A. Bergstra and I. Bethke, Molecular dynamics. J. Logic Algebr. Program. 51 (2002) 125-156. | MR | Zbl

[4] J.A. Bergstra and J.W. Klop, Fixed point semantics in process algebra. Technical Report IW 208, Mathematical Center, Amsterdam (1982).

[5] J.A. Bergstra and M.E. Loots, Program algebra for sequential code. J. Logic Algebr. Program. 51 (2002) 125-156. | MR | Zbl

[6] J.A. Bergstra and C.A. Middelburg, Thread algebra for strategic interleaving. Formal Aspects Comput. 19 (2007) 445-474. Preliminary version: Computer Science Report PRG0404, Sectie Software Engineering, University of Amsterdam. | Zbl

[7] J.A. Bergstra and C.A. Middelburg, A thread algebra with multi-level strategic interleaving. Theor. Comput. Syst. 41 (2007). Preliminary versions: in CiE, edited by S.B. Cooper, B. Loewe and L. Torenvliet. Lect. Notes Comput. Sci. 3526 (2005) 35-48; Computer Science Report 06-28, Department of Mathematics and Computing Science, Eindhoven University of Technology. | MR | Zbl

[8] J.A. Bergstra and C.A. Middelburg, Maurer computers for pipelined instruction processing. J. Math. Struct. Comput. Sci. 18 (2008) 373-409. | MR | Zbl

[9] J.A. Bergstra and A. Ponse, A bypass of Cohen's impossibility result. in Advances in Grid Computing-EGC 2005, edited by P.M.A. Sloot, A.G. Hoekstra, T. Priol, A. Reinefeld and M. Bubak. Lect. Notes Comput. Sci. 3407 (2005) 1097-1106.

[10] S.C.C. Blom, W.J. Fokkink, J.F. Groote, I.A. Van Langevelde, B. Lisser and J.C. Van De Pol, $\mu$CRL: a toolset for analysing algebraic specifications. in Proc. 13th Conference on Computer Aided Verification-CAV'01, edited by G. Berry, H. Common and A. Finkel. Lect. Notes Comput. Sci. 2102 (2001) 250-254. | Zbl

[11] D.E. Denning, A lattice model of secure information flow. Commun. ACM 19 (1976) 236-243. | MR | Zbl

[12] R. Focardi and R. Gorrieri, Automatic compositional verification of some security properties for process algebras, in Proc. of TACA'96, edited by T. Margaria and B. Steffen. Lect. Notes Comput. Sci. 1055 (1996) 111-130.

[13] R. Focardi and R. Gorrieri, The compositional security checker: A tool for the verification of information flow security properties. IEEE Transactions on Software Engineering 23 (1997) 550-571.

[14] R.J. Van Glabbeek and W.P. Weijland, Branching time and abstraction in bisimulation semantics. J. ACM 43 (1996) 555-600. | MR | Zbl

[15] J. Goguen and J. Meseguer, Secure policies and security models, in Proc. IEEE Symp. Security and Privacy (1982) 11-20.

[16] J.F. Groote and F.W. Vaandrager, An efficient algorithm for branching bisimulation and stuttering equivalence, in Proc. ICALP 90, edited by M.S. Paterson. Lect. Notes Comput. Sci. 443 (1990) 626-638. | Zbl

[17] A.C. Meyers, Jflow: Practical mostly-static information flow control, in Proc. ACM Symp. on Principles of Programming Languages (1999) 228-241.

[18] R. Milner, Communication and Concurrency. Prentice Hall (1989). | Zbl

[19] R. Paige and R. Tarjan, Three partition refinement algorithms. SIAM J. Comput. 16 (1987) 973-989. | MR | Zbl

[20] D.M.R. Park, Concurrency and automata on infinite sequences, in Proc. 5th GI Conference, edited by P. Deussen, Lect. Notes Comput. Sci. 104 (1982) 167-183. | Zbl

[21] A. Sabelfeld and H. Mantel, Static confidentiality enforcement for distributed programs. in Proc. Symp. on Static Analysis. Lect. Notes Comput. Sci. 2477 (2002) 376-394. | MR | Zbl

[22] A. Sabelfeld and A. Myers, Language-based information flow security. IEEE J. Sel. Areas Commun. 21 (2003) 5-19.

[23] G. Smith and D. Volpano, Secure information flow in multi-threaded imperative languages, in Proc. POPL'98 29 (1998) 355-364.

[24] D. Volpano, G. Smith and C. Irvine, A sound type system for secure flow analysis. J. Comput. Secur. 4 167-187 (1996).

[25] T.D. Vu, Denotational semantics for thread algebra. J. Logic Algebr. Program. 74 (2007) 94-111. | MR | Zbl

[26] T.D. Vu, Semantics and applications of process and program algebra. Ph.D. thesis, University of Amsterdam (2007).