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.
@article{ITA_2009__43_2_249_0,
author = {Vu, Thuy Duong},
title = {Thread algebra for noninterference},
journal = {RAIRO - Theoretical Informatics and Applications - Informatique Th\'eorique et Applications},
volume = {43},
year = {2009},
pages = {249-268},
doi = {10.1051/ita:2008026},
mrnumber = {2512258},
zbl = {1166.68007},
language = {en},
url = {http://dml.mathdoc.fr/item/ITA_2009__43_2_249_0}
}
Vu, Thuy Duong. Thread algebra for noninterference. RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications, Tome 43 (2009) pp. 249-268. doi : 10.1051/ita:2008026. http://gdmltest.u-ga.fr/item/ITA_2009__43_2_249_0/
[1] , Branching bisimulation is an equivalence indeed. Inform. Process. Lett. 58 (1996) 333-337. | MR 1409718 | Zbl 0875.68624
[2] and , Secure computer systems: mathematical foundations and model. Tech. Rep. M74-244, MITRE Corporation, Bedford, Massachussets (1973).
[3] and , Molecular dynamics. J. Logic Algebr. Program. 51 (2002) 125-156. | MR 1905619 | Zbl 1008.68079
[4] and , Fixed point semantics in process algebra. Technical Report IW 208, Mathematical Center, Amsterdam (1982).
[5] and , Program algebra for sequential code. J. Logic Algebr. Program. 51 (2002) 125-156. | MR 1905616 | Zbl 1008.68079
[6] and , 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 1131.68067
[7] and , 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 2313398 | Zbl 1113.68426
[8] and , Maurer computers for pipelined instruction processing. J. Math. Struct. Comput. Sci. 18 (2008) 373-409. | MR 2462247 | Zbl 1141.68010
[9] and , 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] , , , , and , 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 0991.68640
[11] , A lattice model of secure information flow. Commun. ACM 19 (1976) 236-243. | MR 428801 | Zbl 0322.68034
[12] and , 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] and , The compositional security checker: A tool for the verification of information flow security properties. IEEE Transactions on Software Engineering 23 (1997) 550-571.
[14] and , Branching time and abstraction in bisimulation semantics. J. ACM 43 (1996) 555-600. | MR 1408565 | Zbl 0882.68085
[15] and , Secure policies and security models, in Proc. IEEE Symp. Security and Privacy (1982) 11-20.
[16] and , 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 0765.68125
[17] , Jflow: Practical mostly-static information flow control, in Proc. ACM Symp. on Principles of Programming Languages (1999) 228-241.
[18] , Communication and Concurrency. Prentice Hall (1989). | Zbl 0683.68008
[19] and , Three partition refinement algorithms. SIAM J. Comput. 16 (1987) 973-989. | MR 917035 | Zbl 0654.68072
[20] , Concurrency and automata on infinite sequences, in Proc. 5th GI Conference, edited by P. Deussen, Lect. Notes Comput. Sci. 104 (1982) 167-183. | Zbl 0457.68049
[21] and , Static confidentiality enforcement for distributed programs. in Proc. Symp. on Static Analysis. Lect. Notes Comput. Sci. 2477 (2002) 376-394. | MR 2049487 | Zbl 1015.68509
[22] and , Language-based information flow security. IEEE J. Sel. Areas Commun. 21 (2003) 5-19.
[23] and , Secure information flow in multi-threaded imperative languages, in Proc. POPL'98 29 (1998) 355-364.
[24] , and , A sound type system for secure flow analysis. J. Comput. Secur. 4 167-187 (1996).
[25] , Denotational semantics for thread algebra. J. Logic Algebr. Program. 74 (2007) 94-111. | MR 2378712 | Zbl 1131.68069
[26] , Semantics and applications of process and program algebra. Ph.D. thesis, University of Amsterdam (2007).