Abstract
A well-established specification of noninterference in CSP is that, when high-level events are appropriately abstracted, the remaining low-level view is deterministic. This is not a workable definition in Timed CSP, where many processes cannot be refined to deterministic ones. We argue that in fact “deterministic” should be replaced by “maximally refined” in the definition above. We show how to automate the resulting timed noninterference check within the context of the recent extension of FDR to analyse a discrete version of Timed CSP, and how an extended theory of digitisation has the potential both to create more accurate specifications and to infer when processes are noninterfering in the more usual continuous-time semantics.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
Allen PG (1991) A comparison of non-interference and non-deducibility using CSP. Proc CSFW. IEEE
Alur R, Dill DL (1994) A theory of timed automata. Theor Comput Sci 126(2): 183–235
Armstrong P, Hopcroft PJ, Roscoe AW (2012) Fairness analysis through priority. Forthcoming
Armstrong PJ, Lowe G, Ouaknine J, Roscoe AW (2012) Model-checking Timed CSP. Forthcoming HOWARD (H. Barringer festschift), Easychair (pub)
Barbuti R, Francesco ND, Santone A, Tesei L (2002) A notion of non-interference for timed automata. Fundam Inform 51: 1–11
Barbuti R, Tesei L (2003) A decidable notion of timed non-interference. Fundam Inform 54: 137–150
Focardi R, Gorrieri R (1994) A classification of security properties for process algebras. J Comput Secur 3: 5–33
Focardi R, Gorrieri R, Martinelli F (2000) Information flow analysis in a discrete-time process algebra. CSFW-13, IEEE
Focardi R, Gorrieri R, Martinelli F (2003) Real-time information flow analysis. Sel Areas Commun 21: 20–34
Forster R (1999) Noninterference properties for nondeterministic processes. Oxford University DPhil thesis
Forster R, Reed GM, Roscoe AW (2000) The successes and failures of behavioural models. In: Millenial perspectives in computer science. Palgrave
Goguen JA, Meseguer J (1982) Security policies and security models. In: Proceedings of IEEE symposium on security and privacy
Graham-Cumming J (1992) The formal development of secure systems. Oxford University DPhil thesis
Henzinger TA, Manna Z, Pnueli A (1992) What good are digital clocks? In: Proceedings of the nineteenth international colloquium on automata, languages, and programming (ICALP 92), vol 623. Springer/LNCS, Berlin, pp 545–558
Huang J (2010) Extending non-interference properties to the timed world. Oxford University DPhil thesis
Huang J, Roscoe AW (2006) Extending non-interference properties to the timed world. In: Proc ACM SAC
Lazić RS (1999) A semantic study of data independence with applications to model checking. Oxford University DPhil thesis
Lowe G, Ouaknine J (2006) On timed models and full abstraction. ENTCS 155: 497–519
McIver AK, Morgan CC (2010) The thousand-and-one cryptographers. Reflections on the work of C.A.R. Hoare. Springer, Berlin
Morgan CC (2006) The shadow knows: refinement of ignorance in sequential programs. Proc MPC LNCS 4014
Ouaknine J (2001) Discrete analysis of continuous behaviour in real-time concurrent systems. Oxford University D.Phil thesis
Ouaknine J (2002) Digitisation and full abstraction for dense-time model checking. TACAS Springer LNCS
Ouaknine J, Worrell JB (2003) Timed CSP = closed timed epsilon-automata. Nord J Comput 10: 99–133
Reed GM (1988) A uniform mathematical theory for real-time distributed computing. Oxford University DPhil thesis
Reed GM, Roscoe AW (1988) A timed model for communicating sequential processes. Theor Comput Sci 58: 249–261
Reed GM, Roscoe AW (1999) The timed failures-stability model for CSP. Theor Comput Sci 211: 85–127
Roscoe AW (1994) Model checking CSP. In: A classical mind: essays in honour of C.A.R. Hoare. Prentice Hall
Roscoe AW (1995) CSP and determinism in security modelling. Proceedings of IEEE symposium on security and privacy
Roscoe AW (1997) The theory and practice of concurrency. Prentice Hall
Roscoe AW (2006) Confluence thanks to extensional determinism. ENTCS 162: 305–309
Roscoe AW (2010) Understanding concurrent systems. Springer, Berlin
Roscoe AW, Woodcock JCP, Wulf L (1996) Non-interference through determinism. J Comput Secur 4(1): 27–53
Ryan PYA (1991) A CSP formulation of non-interference and unwinding. Cipher Winter 1991. IEEE Press
Schneider SA (2000) Concurrent and real-time systems: the CSP approach. Wiley, New York
Author information
Authors and Affiliations
Corresponding author
Additional information
Peter Höfner, Robert van Glabbeek and Ian Hayes
Rights and permissions
About this article
Cite this article
Roscoe, A.W., Huang, J. Checking noninterference in Timed CSP. Form Asp Comp 25, 3–35 (2013). https://doi.org/10.1007/s00165-012-0251-6
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s00165-012-0251-6