Formal Methods in System Design

, Volume 40, Issue 1, pp 88–115 | Cite as

Synthesis of opaque systems with static and dynamic masks

  • Franck Cassez
  • Jérémy Dubreil
  • Hervé Marchand


Opacity is a security property formalizing the absence of secret information leakage and we address in this paper the problem of synthesizing opaque systems. A secret predicate S over the runs of a system G is opaque to an external user having partial observability over G, if s/he can never infer from the observation of a run of G that the run belongs to S. We choose to control the observability of events by adding a device, called a mask, between the system G and the users. We first investigate the case of static partial observability where the set of events the user can observe is fixed a priori by a static mask. In this context, we show that checking whether a system is opaque is PSPACE-complete, which implies that computing an optimal static mask ensuring opacity is also a PSPACE-complete problem. Next, we introduce dynamic partial observability where the set of events the user can observe changes over time and is chosen by a dynamic mask. We show how to check that a system is opaque w.r.t. to a dynamic mask and also address the corresponding synthesis problem: given a system G and secret states S, compute the set of dynamic masks under which S is opaque. Our main result is that the set of such masks can be finitely represented and can be computed in EXPTIME and this is a lower bound. Finally we also address the problem of computing an optimal mask.


Security Confidentiality property Opacity Synthesis Dynamic observation 


  1. 1.
    Alur R, Černý P, Zdancewic S (2006) Preserving secrecy under refinement. In: ICALP’06: proceedings (Part II) of the 33rd international colloquium on automata, languages and programming. Springer, Berlin, pp 107–118 Google Scholar
  2. 2.
    Badouel E, Bednarczyk M, Borzyszkowski A, Caillaud B, Darondeau P (2007) Concurrent secrets. Discret Event Dyn Syst 17:425–446 MathSciNetMATHCrossRefGoogle Scholar
  3. 3.
    Blanchet B, Abadi M, Fournet C (2005) Automated verification of selected equivalences for security protocols. In: 20th IEEE symposium on logic in computer science (LICS 2005), Chicago, IL, June 2005. IEEE Computer Society, Los Alamitos, pp 331–340 Google Scholar
  4. 4.
    Bryans J, Koutny M, Mazaré L, Ryan P (2008) Opacity generalised to transition systems. Int J Inf Secur 7(6):421–435 CrossRefGoogle Scholar
  5. 5.
    Cassez F, Tripakis S (2008) Fault diagnosis with static or dynamic diagnosers. Fundam Inform 88(4):497–540 MathSciNetMATHGoogle Scholar
  6. 6.
    Cassez F, Mullins J, Roux OH (2007) Synthesis of non-interferent systems. In: 4th int conf on mathematical methods, models and architectures for computer network security (MMM-ACNS’07). Communications in computer and inform science, vol 1. Springer, Berlin, pp 307–321 Google Scholar
  7. 7.
    Cassez F, Dubreil J, Marchand H (2009) Dynamic observers for the synthesis of opaque systems. In: Liu Z, Ravn AP (eds) 7th international symposium on automated technology for verification and analysis (ATVA’09), Macao SAR, China, October 2009. LNCS, vol 5799. Springer, Berlin, pp 352–367 CrossRefGoogle Scholar
  8. 8.
    Darmaillacq V, Fernandez J-C, Groz R, Mounier L, Richier J-L (2006) Test generation for network security rules. In: TestCom 2006. LNCS, vol 3964 Google Scholar
  9. 9.
    Dasdan A, Irani S, Gupta R (1999) Efficient algorithms for optimum cycle mean and optimum cost to time ratio problems. In: Annual ACM IEEE design automation conference, New Orleans, Louisiana, United States. ACM, New York, pp 37–42 Google Scholar
  10. 10.
    Dubreil J, Darondeau P, Marchand H (2008) Opacity enforcing control synthesis. In: Proceedings of the 9th international workshop on discrete event systems (WODES’08), Göteborg, Sweden, May 2008, pp 28–35 CrossRefGoogle Scholar
  11. 11.
    Dubreil J, Jéron T, Marchand H (2009) Monitoring confidentiality by diagnosis techniques. In: European control conference, Budapest, Hungary, August 2009, pp 2584–2590 Google Scholar
  12. 12.
    Dubreil J, Darondeau Ph, Marchand H (2010) Supervisory control for opacity. IEEE Trans Autom Control 55(5):1089–1100 MathSciNetCrossRefGoogle Scholar
  13. 13.
    Falcone Y, Fernandez J-C, Mounier L (2011) What can you verify and enforce at runtime? Int J Softw Tools Technol Transf (STTT) Google Scholar
  14. 14.
    Focardi R, Gorrieri R (2001) Classification of security properties (part I: Information flow). In: Focardi R, Gorrieri R (eds) Foundations of security analysis and design I: FOSAD 2000 tutorial lectures. Lecture notes in computer science, vol 2171. Springer, Heidelberg, pp 331–396 Google Scholar
  15. 15.
    Hadj-Alouane N, Lafrance S, Lin F, Mullins J, Yeddes M (2005) On the verification of intransitive noninterference in multilevel security. IEEE Trans Syst Man Cybern, Part B, Cybern 35(5):948–957 CrossRefGoogle Scholar
  16. 16.
    Karp R (1978) A characterization of the minimum mean cycle in a digraph. Discrete Math 23:309–311 MathSciNetMATHGoogle Scholar
  17. 17.
    Le Guernic G (2007) Information flow testing—the third path towards confidentiality guarantee. In: Advances in computer science, ASIAN 2007, Computer and network security. LNCS, vol 4846, pp 33–47 CrossRefGoogle Scholar
  18. 18.
    Ligatti J, Bauer L, Walker D (2005) Edit automata: enforcement mechanisms for run-time security policies. Int J Inf Secur 4(1–2):2–16 CrossRefGoogle Scholar
  19. 19.
    Lowe G (1999) Towards a completeness result for model checking of security protocols. J Comput Secur 7(2–3):89–146 Google Scholar
  20. 20.
    Martin D (1975) Borel determinacy. Ann Math 102(2):363–371 MATHCrossRefGoogle Scholar
  21. 21.
    Mazaré L (2004) Using unification for opacity properties. In: Proceedings of the 4th IFIP WG1.7 workshop on issues in the theory of security (WITS’04), Barcelona (Spain), pp 165–176 Google Scholar
  22. 22.
    Ricker SL (2006) A question of access: decentralized control and communication strategies for security policies. In: 8th international workshop on discrete event systems, June 2006, pp 58–63 CrossRefGoogle Scholar
  23. 23.
    Schneider F (2000) Enforceable security policies. ACM Trans Inf Syst Secur 3(1):30–50 CrossRefGoogle Scholar
  24. 24.
    Stockmeyer L, Meyer A (1973) Word problems requiring exponential time: Preliminary report. In: STOC. ACM, New York, pp 1–9 Google Scholar
  25. 25.
    Takai S, Oka Y (2008) A formula for the supremal controllable and opaque sublanguage arising in supervisory control. J Control Meas Syst Integr 1(4):307–312 Google Scholar
  26. 26.
    Thomas W (1995) On the synthesis of strategies in infinite games. In: Proc 12th annual symposium on theoretical aspects of computer science (STACS’95), vol 900. Springer, Berlin, pp 1–13. Invited talk Google Scholar
  27. 27.
    Zwick U, Paterson M (1996) The complexity of mean payoff games on graphs. Theor Comput Sci 158(1–2):343–359 MathSciNetMATHCrossRefGoogle Scholar

Copyright information

© Springer Science+Business Media, LLC 2012

Authors and Affiliations

  • Franck Cassez
    • 1
  • Jérémy Dubreil
    • 2
  • Hervé Marchand
    • 3
  1. 1.CNRSNational ICT AustraliaSydneyAustralia
  2. 2.ComèteINRIA and Ecole PolytechniquePalaiseauFrance
  3. 3.VerTeCs, INRIACentre Rennes–Bretagne AtlantiqueRennesFrance

Personalised recommendations