Synthesis of Non-interferent Distributed Systems

  • Franck Cassez
  • John Mullins
  • Olivier H. Roux
Part of the Communications in Computer and Information Science book series (CCIS, volume 1)


In this paper, we focus on distributed systems subject to security issues. Such systems are usually composed of two entities: a high level user and a low level user that can both do some actions. The security properties we consider are non-interference properties. A system is non-interferent if the low level user cannot deduce any information by playing its low level actions. Various notions of non-interference have been defined in the literature, and in this paper we focus on two of them: one trace-based property (SNNI) and another bisimulation-based property (BSNNI).

For these properties we study the problems of synthesis of a high level user so that the system is non-interferent. We prove that a most permissive high level user can be computed when one exists.


Non-Interference Controller Synthesis 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    van der Meyden, R., Zhang, C.: Algorithmic verification of noninterference properties. In: Proceedings of the Second International Workshop on Views on Designing Complex Architectures (VODCA 2006). Electronic Notes in Theoretical Computer Science, vol. 168, pp. 61–75. Elsevier, Amsterdam (2006).Google Scholar
  2. 2.
    Agat, J.: Transforming out timing leaks. In: Proc. of the 27th ACM SIGPLAN-SIGACT symposium on Principles of programming languages (POPL′00), Boston, MA, USA, pp. 40–53. ACM Press, New York (2000)CrossRefGoogle Scholar
  3. 3.
    Sabelfeld, A., Myers, A.: Language-based information-flow security. IEEE Journal on Selected Areas in Communications 21(1) (2003)Google Scholar
  4. 4.
    Gardey, G., Mullins, J., Roux, O.H.: Non-interference control synthesis for security timed automata. In: 3rd International Workshop on Security Issues in Concurrency (SecCo′05), San Francisco, USA. Electronic Notes in Theoretical Computer Science, Elsevier, Amsterdam (2005)Google Scholar
  5. 5.
    Kozen, D.: Results on the propositional-calculus. In: Nielsen, M., Schmidt, E.M. (eds.) Automata, Languages, and Programming. LNCS, vol. 140, pp. 348–359. Springer, Heidelberg (1982)CrossRefGoogle Scholar
  6. 6.
    Arnold, A., Niwiński, D.: Rudiments of μ-calculus. In: Studies in Logic and the Foundations of Mathematics, vol. 146, North-Holland, Amsterdam, (2001)Google Scholar
  7. 7.
    Aceto, L., Ingólfsdóttir, A.: Characteristic formulæ: From automata to logic. Technical Report RS-07-2, BRICS, Aarhus, Denmark (2007)Google Scholar
  8. 8.
    Müller-Olm, M.: Derivation of characteristic formulæ. In: Workshop on Mathemantical Foundations of Computer Science, Brno, Slovakia. Electronic Notes in Theoretical Computer Science, vol. 18, Elsevier, Amsterdam (1998)Google Scholar
  9. 9.
    Ramadge, P., Wonham, W.: Supervisory control of a class of discrete event processes. SIAM J. Control Optim. 25(1) (1987)Google Scholar
  10. 10.
    Ramadge, P., Wonham, W.: The control of discrete event systems. In: Proceedings of the IEEE, IEEE Computer Society Press, Los Alamitos (1989).Google Scholar
  11. 11.
    Thomas, W.: On the synthesis of strategies in infinite games. In: Mayr, E.W., Puech, C. (eds.) STACS 95. LNCS, vol. 900, pp. 1–13. Springer, Heidelberg (1995)Google Scholar
  12. 12.
    Arnold, A., Vincent, A., Walukiewicz, I.: Games for synthesis of controllers with partial observation. Theor. Comput. Sci. 1(303), 7–34 (2003)CrossRefMathSciNetGoogle Scholar
  13. 13.
    Riedweg, S., Pinchinat, S.: Quantified mu-calculus for control synthesis. In: Rovan, B., Vojtáš, P. (eds.) MFCS 2003. LNCS, vol. 2747, pp. 642–651. Springer, Heidelberg (2003).Google Scholar
  14. 14.
    Focardi, R., Gorrieri, R.: Classification of security properties (part I: Information flow). In: Focardi, R., Gorrieri, R. (eds.) Foundations of Security Analysis and Design. LNCS, vol. 2171, pp. 331–396. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  15. 15.
    Hoffmann, G., Wong-Toi, H.: Symbolic synthesis of supervisory controllers. In: Proc. of the American Control Conference, Chicago, IL, pp. 2789–2793 (1992)Google Scholar
  16. 16.
    Point, G.: The synthesis toolbox-from modal automata to controller synthesis. Technical Report, 1342–05, LaBRI (2005) available at

Copyright information

© Springer-Verlag Berlin Heidelberg 2007

Authors and Affiliations

  • Franck Cassez
    • 1
  • John Mullins
    • 2
  • Olivier H. Roux
    • 1
  1. 1.IRCCyN/CNRSNantes Cedex 3France
  2. 2.École Polytechnique de MontréalMontrealCanada

Personalised recommendations