Thread algebra for noninterference

Thuy Duong Vu

RAIRO - Theoretical Informatics and Applications (2008)

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

Abstract

top
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'9829 (1998) 355–364] and can be applied to unstructured and multithreaded programming languages.

How to cite

top

Vu, Thuy Duong. "Thread algebra for noninterference." RAIRO - Theoretical Informatics and Applications 43.2 (2008): 249-268. <http://eudml.org/doc/92915>.

@article{Vu2008,
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'9829 (1998) 355–364] and can be applied to unstructured and multithreaded programming languages. },
author = {Vu, Thuy Duong},
journal = {RAIRO - Theoretical Informatics and Applications},
keywords = {Noninterference; thread algebra; formal methods; security verification; noninterference},
language = {eng},
month = {10},
number = {2},
pages = {249-268},
publisher = {EDP Sciences},
title = {Thread algebra for noninterference},
url = {http://eudml.org/doc/92915},
volume = {43},
year = {2008},
}

TY - JOUR
AU - Vu, Thuy Duong
TI - Thread algebra for noninterference
JO - RAIRO - Theoretical Informatics and Applications
DA - 2008/10//
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'9829 (1998) 355–364] and can be applied to unstructured and multithreaded programming languages.
LA - eng
KW - Noninterference; thread algebra; formal methods; security verification; noninterference
UR - http://eudml.org/doc/92915
ER -

References

top
  1. T. Basten, Branching bisimulation is an equivalence indeed. Inform. Process. Lett.58 (1996) 333–337.  
  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.  
  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.  
  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.  
  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.  
  8. J.A. Bergstra and C.A. Middelburg, Maurer computers for pipelined instruction processing. J. Math. Struct. Comput. Sci.18 (2008) 373–409.  
  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, µ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.  
  11. D.E. Denning, A lattice model of secure information flow. Commun. ACM19 (1976) 236–243.  
  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 Engineering23 (1997) 550–571.  
  14. R.J. van Glabbeek and W.P. Weijland, Branching time and abstraction in bisimulation semantics. J. ACM43 (1996) 555–600.  
  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.  
  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).  
  19. R. Paige and R. Tarjan, Three partition refinement algorithms. SIAM J. Comput.16 (1987) 973–989.  
  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.  
  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.  
  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'9829 (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.  
  26. T.D. Vu, Semantics and applications of process and program algebra. Ph.D. thesis, University of Amsterdam (2007).  

NotesEmbed ?

top

You must be logged in to post comments.

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

Only the controls for the widget will be shown in your chosen language. Notes will be shown in their authored language.

Tells the widget how many notes to show per page. You can cycle through additional notes using the next and previous controls.

    
                

                
Note: Best practice suggests putting the JavaScript code just before the closing </body> tag.