# Thread algebra for noninterference

RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications (2009)

- Volume: 43, Issue: 2, page 249-268
- ISSN: 0988-3754

## Access Full Article

top## Abstract

top## How to cite

topVu, Thuy Duong. "Thread algebra for noninterference." RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications 43.2 (2009): 249-268. <http://eudml.org/doc/245670>.

@article{Vu2009,

abstract = {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.},

author = {Vu, Thuy Duong},

journal = {RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications},

keywords = {noninterference; thread algebra; formal methods; security verification},

language = {eng},

number = {2},

pages = {249-268},

publisher = {EDP-Sciences},

title = {Thread algebra for noninterference},

url = {http://eudml.org/doc/245670},

volume = {43},

year = {2009},

}

TY - JOUR

AU - Vu, Thuy Duong

TI - Thread algebra for noninterference

JO - RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications

PY - 2009

PB - EDP-Sciences

VL - 43

IS - 2

SP - 249

EP - 268

AB - 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.

LA - eng

KW - noninterference; thread algebra; formal methods; security verification

UR - http://eudml.org/doc/245670

ER -

## References

top- [1] T. Basten, Branching bisimulation is an equivalence indeed. Inform. Process. Lett. 58 (1996) 333–337. Zbl0875.68624MR1409718
- [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. Zbl1008.68079MR1905619
- [4] J.A. Bergstra and J.W. Klop, Fixed point semantics in process algebra. Technical Report IW 208, Mathematical Center, Amsterdam (1982). Zbl0549.68012
- [5] J.A. Bergstra and M.E. Loots, Program algebra for sequential code. J. Logic Algebr. Program. 51 (2002) 125–156. Zbl1008.68079MR1905616
- [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. Zbl1131.68067
- [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. Zbl1113.68426MR2313398
- [8] J.A. Bergstra and C.A. Middelburg, Maurer computers for pipelined instruction processing. J. Math. Struct. Comput. Sci. 18 (2008) 373–409. Zbl1141.68010MR2462247
- [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. Zbl0991.68640
- [11] D.E. Denning, A lattice model of secure information flow. Commun. ACM 19 (1976) 236–243. Zbl0322.68034MR428801
- [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. Zbl0882.68085MR1408565
- [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. Zbl0765.68125
- [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). Zbl0683.68008
- [19] R. Paige and R. Tarjan, Three partition refinement algorithms. SIAM J. Comput. 16 (1987) 973–989. Zbl0654.68072MR917035
- [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. Zbl0457.68049
- [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. Zbl1015.68509MR2049487
- [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. Zbl1131.68069MR2378712
- [26] T.D. Vu, Semantics and applications of process and program algebra. Ph.D. thesis, University of Amsterdam (2007).

## NotesEmbed ?

topTo embed these notes on your page include the following JavaScript code on your page where you want the notes to appear.