Hostname: page-component-cd9895bd7-q99xh Total loading time: 0 Render date: 2024-12-29T05:51:39.715Z Has data issue: false hasContentIssue false
  • English
  • Français

Thread algebra for noninterference

Published online by Cambridge University Press:  02 October 2008

Thuy Duong Vu
Thuy Duong Vu*
Affiliation:
Sectie Software Engineering, University of Amsterdam, Kruislaan 403, 1098 SJ Amsterdam, The Netherlands; [email protected]
Get access

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.

Keywords

Noninterferencethread algebraformal methodssecurity verification
Type
Research Article
Information
RAIRO - Theoretical Informatics and Applications , Volume 43 , Issue 2 , April 2009 , pp. 249 - 268
Copyright
© EDP Sciences, 2008

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

Basten, T., Branching bisimulation is an equivalence indeed. Inform. Process. Lett. 58 (1996) 333–337. CrossRef
D.E. Bell and L.J. La Padula, Secure computer systems: mathematical foundations and model. Tech. Rep. M74-244, MITRE Corporation, Bedford, Massachussets (1973).
Bergstra, J.A. and Bethke, I., Molecular dynamics. J. Logic Algebr. Program. 51 (2002) 125–156. CrossRef
J.A. Bergstra and J.W. Klop, Fixed point semantics in process algebra. Technical Report IW 208, Mathematical Center, Amsterdam (1982).
Bergstra, J.A. and Loots, M.E., Program algebra for sequential code. J. Logic Algebr. Program. 51 (2002) 125–156. CrossRef
Bergstra, J.A. and Middelburg, C.A., Thread algebra for strategic interleaving. Formal Aspects Comput. 19 (2007) 445–474. Preliminary version: Computer Science Report PRG0404, Sectie Software Engineering, University of Amsterdam. CrossRef
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.
Bergstra, J.A. and Middelburg, C.A., Maurer computers for pipelined instruction processing. J. Math. Struct. Comput. Sci. 18 (2008) 373–409.
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.
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.
Denning, D.E., A lattice model of secure information flow. Commun. ACM 19 (1976) 236–243. CrossRef
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.
Focardi, R. and Gorrieri, R., The compositional security checker: A tool for the verification of information flow security properties. IEEE Transactions on Software Engineering 23 (1997) 550–571. CrossRef
van Glabbeek, R.J. and Weijland, W.P., Branching time and abstraction in bisimulation semantics. J. ACM 43 (1996) 555–600. CrossRef
J. Goguen and J. Meseguer, Secure policies and security models, in Proc. IEEE Symp. Security and Privacy (1982) 11–20.
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.
A.C. Meyers, Jflow: Practical mostly-static information flow control, in Proc. ACM Symp. on Principles of Programming Languages (1999) 228–241.
R. Milner, Communication and Concurrency. Prentice Hall (1989).
Paige, R. and Tarjan, R., Three partition refinement algorithms. SIAM J. Comput. 16 (1987) 973–989. CrossRef
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.
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.
Sabelfeld, A. and Myers, A., Language-based information flow security. IEEE J. Sel. Areas Commun. 21 (2003) 5–19. CrossRef
G. Smith and D. Volpano, Secure information flow in multi-threaded imperative languages, in Proc. POPL'98 29 (1998) 355–364.
D. Volpano, G. Smith and C. Irvine, A sound type system for secure flow analysis. J. Comput. Secur. 4 167–187 (1996).
Denotational, T.D. Vu semantics for thread algebra. J. Logic Algebr. Program. 74 (2007) 94–111.
T.D. Vu, Semantics and applications of process and program algebra. Ph.D. thesis, University of Amsterdam (2007).