We present an approach based on inductive theorem proving for verifying invariants of dynamic systems specified in rewriting logic, a formal specification language implemented in the Maude system. An invariant is a property that holds on all the states that are reachable from a given class of initial states. Our approach consists in encoding the semantic aspects that are relevant for our task (namely, verifying invariance properties of the specified systems) in membership equational logic, a sublogic of rewriting logic. The invariance properties are then formalized over the encoded rewrite theories and are proved using an inductive theorem prover for membership equational logic also implemented in the Maude system using its reflective capabilities. We illustrate our approach by verifying mutual exclusion in an n-process Bakery algorithm }, OPTnote = {An english version is available here}, pdf = {http://www.irisa.fr/vertecs/Publis/Ps/rusu-clavel-francais.pdf}, x-international-audience ={no}, x-proceedings ={yes}, x-pays = {ES} } @Misc{Jeron-ETR09, Author = {J\'eron, T}, Title = {G\'enération de tests pour les syst\`emes r\'eactifs et temporis\'es}, Booktitle = {Ecole d'Et\'e Temps-R\'eel, T\'el\'ecom ParisTech, Paris}, Month = {September}, Year = 2009, note = {Invited talk}, pdf = {http://www.irisa.fr/vertecs/Publis/Ps/paper-ETR-2009.pdf} } @InProceedings{msr09, author = {Kalyon, G. and Le Gall, T. and Marchand, H. and Massart, T.}, title = {Contrôle décentralisé de systèmes symboliques infinis sous observation partielle}, booktitle = {7ème Colloque Francophone sur la Modélisation des Systèmes Réactifs}, confnat = true, year = 2009, pages = {805-820}, month = novembre, abstract = {Nous proposons des algorithmes permettant de synthétiser des contrôleurs décentralisés n'ayant qu'une observation partielle du système à contrôler. Ces systèmes, dont le nombre d'états peut être infini, sont modélisés par des Systèmes à Transitions Symboliques. Nous présentons des modèles de contrôleurs (non-bloquants) valides permettant d'assurer l'interdiction d'un ensemble d'états dans un cadre décentralisé. Pour obtenir des algorithmes pour ces problèmes, nous utilisons des techniques d'interprétation abstraite, qui induisent une sur-approximation de l'ensemble des transitions à interdire. Notre outil SMACS permet de valider empiriquement nos méthodes et de montrer leurs faisabilité et efficacité.}, x-international-audience ={no}, x-proceedings ={yes}, x-pays = {BE} } @InProceedings{icca, author = {Kalyon, G. and Le Gall, T. and Marchand, H. and Massart, T.}, title = {Computational Complexity for State-Feedback Controllers with Partial Observation}, booktitle = {7th International Conference on Control and Automation, ICCA'09}, year = 2009, pages = {435-441}, address = {Christchurch, New Zealand}, month = decembre, pdf = {http://www.irisa.fr/vertecs/Publis/Ps/icca2009.pdf}, doi = {http://dx.doi.org/10.1109/ICCA.2009.5410356 }, abstract = { We study the computational complexity of several decision and optimization control problems arising in partially observed discrete event systems. These problems are related to the state avoidance problem where one must compute a controller which prevents the system from accessing a set of bad states and which is maximal for a defined criterion, based on inclusion of the set of states remaining reachable after the control. We focus our study on memoryless controllers.}, x-international-audience ={yes}, x-proceedings ={yes}, x-pays = {BE} } @InProceedings{infinity09, author = {Morvan, C.}, title = {On external presentations of infinite graphs}, booktitle = {11th International Workshop on Verification of Infinite-State Systems, INFINITY'09}, year = 2009, address = {Bologna, Italy}, month = aout, series = {EPTCS}, volume = {10}, pages = {22-35} doi = {http://dx.doi.org/10.3233/10.4204/EPTCS.10.2}, pdf = {http://arxiv.org/pdf/0911.3283v1}, asbtract = {The vertices of a finite state system are usually a subset of the natural numbers. Most algorithms relative to these systems only use this fact to select vertices. For infinite state systems, however, the situation is different: in particular, for such systems having a finite description, each state of the system is a configuration of some machine. Then most algorithmic approaches rely on the structure of these configurations. Such characterisations are said internal. In order to apply algorithms detecting a structural property (like identifying connected components) one may have first to transform the system in order to fit the description needed for the algorithm. The problem of internal characterisation is that it hides structural properties, and each solution becomes ad hoc relatively to the form of the configurations. On the contrary, external characterisations avoid explicit naming of the vertices. Such characterisation are mostly defined via graph transformations. In this paper we present two kind of external characterisations: deterministic graph rewriting, which in turn characterise regular graphs, deterministic context-free languages, and rational graphs. Inverse substitution from a generator (like the complete binary tree) provides characterisation for prefix-recognizable graphs, the Caucal Hierarchy and rational graphs. We illustrate how these characterisation provide an efficient tool for the representation of infinite state systems.}, x-international-audience ={yes}, x-proceedings ={yes}, } @InProceedings{HVC2009, author = {Morvan, C. and Pinchinat, S.}, title = {Diagnosability of pushdown systems}, booktitle = {HVC2009, Haifa Verification Conference}, series = {LNCS}, volume = {6405}, pages = {21-33}, year = 2009, address = {Haifa, Israel}, month = {October}, abstract = {Diagnosis problems of discrete-event systems consist in detecting unobservable defects during system execution. For finite-state systems, the theory is well understood and a number of effective solutions have been developed. For infinite-state systems, however, there are only few results, mostly identifying classes where the problem is undecidable. We consider higher-order pushdown systems and investigate two basic variants of diagno- sis problems: the diagnosability, which consists in deciding whether defects can be detected within a finite delay, and the bounded-latency problem, which consists in determining a bound for the delay of detecting defects. }, pdf = {ftp://ftp.irisa.fr/techreports/2008/PI-1904.pdf}, doi = {http://dx.doi.org/10.1007/978-3-642-19237-1_6}, x-international-audience ={yes}, x-proceedings ={yes}, } @TechReport{delaval09, author = {Delaval, Gwenael. and Marchand, Hervé and Rutten, Eric}, title = {BZR Contracts for Modular Discrete Controller Synthesis}, institution = {INRIA}, year = {2009}, type = {Research Report}, number = {7111}, month = {November}, pdf={http://hal.inria.fr/docs/00/43/65/60/PDF/RR-7111.pdf} abstract = {We describe the extension of a reactive programming language with a behavioral contract construct. It is particularly dedicated to the programming of reactive control of applications in embedded systems, and involves principles of the supervisory control of discrete event systems. Our contribution is in a language approach where modular discrete controller synthesis (DCS) is integrated, and it is concretized in the encapsulation of DCS into a compilation process. From transition system specifications of possible behaviors, DCS automatically produces controllers that make the controlled system satisfy the property given as objective. Our language features and compiling technique hence provide correctness-by-construction in that sense, and enhance reliability and verifiability. An application domain particularly targeted at is that of adaptive and reconfigurable systems: closed-loop adaptation mechanisms enable flexible execution of functionalities w.r.t. changing resource and environment conditions. Our language can serve programming such adaption controllers. This paper particularly describes the compilation of the language. We present a method for the modular application of discrete controller synthesis on synchronous programs, and its integration in the BZR language. We consider structured programs, as a composition of nodes, and first apply DCS on particular nodes of the program, in order to reduce the complexity of the controller computation; then, we allow the abstraction of parts of the program for this computation; and finally, we show how to recompose the different controllers computed from different abstractions for their correct co-execution with the initial program. Our work is illustrated with examples, and we present quantitative results about its implementation.} } @Article{rutten09, author = {Rutten, Eric and Marchand, Hervé}, title = {Automatic generation of safe handlers for multi-task systems}, journal = {Journal of Embedded Computing}, year = {2009}, volume = {3}, number = {4}, pages = {255-276}, abstract = {We are interested in the programming of real-time embedded control systems, such as in robotic, automotive or avionic systems. They are designed with multiple tasks, each with multiple modes. It is complex to design task handlers that control the switching of activities in order to insure safety properties of the global system. We propose a model of tasks in terms of transition systems, designed especially with the purpose of applying existing discrete controller synthesis techniques. This provides us with a systematic methodology, for the automatic generation of safe task handlers, with the support of synchronous languages and associated tools.}, pdf = {http://www.irisa.fr/vertecs/Publis/Ps/jec-2009.pdf}, doi = {http://dx.doi.org/10.3233/JEC-2009-0097} } @inproceedings{RusuC09b, author = {Rusu, Vlad}, title = {Formal Executable Semantics for Conformance in the MDE Framework}, booktitle = {UML and FM workshop}, year = 2009, month = {December}, address = {Rio de Janeiro, Brazil}, abstract = {In the MDE framework, a metamodel is a language referring to some kind of metadata whose elements formalize concepts and relations providing a modeling language. An instance of this modeling language which adheres to its concepts and relations is called a valid model, i.e., a model satisfying structural conformance to its metamodel. However, a metamodel frequently imposes additional constraints to its valid instances. These conditions are usually written in OCL and are called well-formedness rules. In presence of these constraints, a valid model must adhere to the concepts and relations of its metamodel and fullfill its constraints, i.e., a valid model is a model satisfying semantical conformance to its metamodel. In this work, we provide a formal semantics to the notions of structural and semantical conformance between models and metamodels building on our previous work. Our definitions can be automatically checked using the ITP/OCL tool.}, x-international-audience ={yes}, x-proceedings ={yes} } @Misc{morvan:automatha09, author = {Morvan, C. and Pinchinat, S.}, title = {Diagnosability of pushdown systems}, booktitle = {AutomathA}, year = 2009, month = {June}, address = {Liège, Belgique}, abstract = {Diagnosis problems of discrete-event systems consist in detecting unobservable defects during system execution. For finite-state systems, the theory is well understood and a number of effective solutions have been developed. For infinite-state systems, however, there are only few results, mostly identifying classes where the problem is undecidable. We consider higher-order pushdown systems and investigate two basic variants of diagno- sis problems: the diagnosability, which consists in deciding whether defects can be detected within a finite delay, and the bounded-latency problem, which consists in determining a bound for the delay of detecting defects. }, x-international-audience ={yes} } @InProceedings{lics09, author = {Bertrand, N. and Genest, B. and Gimbert. H.}, title = {Qualitative Determinacy and Decidability of Stochastic Games with Signals}, booktitle = {24th Annual IEEE Symposium on Logic in Computer Science (LICS'09)}, pages = {319-328}, year = 2009, publisher = {IEEE Computer Society Press}, address = {Los Angeles, CA, USA}, month = {August}, pdf = {http://www.irisa.fr/vertecs/Publis/Ps/lics2009.pdf}, doi = {http://dx.doi.org/10.1109/LICS.2009.31}, abstract = {We consider the standard model of finite two-person zero-sum stochastic games with signals. We are interested in the existence of almost-surely winning or positively winning strategies, under reachability, safety, Büchi or co-Büchi winning objectives. We prove two qualitative determinacy results. First, in a reachability game either player 1 can achieve almost-surely the reachability objective, or player 2 can ensure surely the complementary safety objective, or both players have positively winning strategies. Second, in a Büchi game if player 1 cannot achieve almost-surely the Büchi objective, then player 2 can ensure positively the complementary co-Büchi objective. We prove that players only need strategies with finite-memory, whose sizes range from no memory at all to doubly-exponential number of states, with matching lower bounds. Together with the qualitative determinacy results, we also provide fix-point algorithms for deciding which player has an almost-surely winning or a positively winning strategy and for computing the finite memory strategy. Complexity ranges from EXPTIME to 2-EXPTIME with matching lower bounds, and better complexity can be achieved for some special cases where one of the players is better informed than her opponent.}, x-international-audience ={yes}, x-proceedings ={yes} } @InProceedings{icalp09, author = {Baier, C. and Bertrand, N. and Bouyer, P. and Brihaye, Th. }, title = {When are timed automata determinizable? }, booktitle = {36th International Colloquium on Automata, Languages and Programming (ICALP'09)}, Pages = {43-54}, doi = {http://dx.doi.org/10.1007/978-3-642-02930-1_4}, year = 2009, series = {LNCS}, volume = {5556}, address = {Rhodes, Greece}, month = {July}, pdf = {http://www.irisa.fr/vertecs/Publis/Ps/BBBB-icalp09.pdf}, abstract = {In this paper, we propose an abstract procedure which, given a timed automaton, produces a language-equivalent deterministic infinite timed tree. We prove that under a certain boundedness condition, the infinite timed tree can be reduced into a classical deterministic timed automaton. The boundedness condition is satisfied by several subclasses of timed automata, some of them were known to be determinizable (event-clock timed automata, automata with integer resets), but some others were not. We prove for instance that strongly non-Zeno timed automata can be determinized. As a corollary of those constructions, we get for those classes the decidability of the universality and of the inclusion problems, and compute their complexities (the inclusion problem is for instance EXPSPACE-complete for strongly non-Zeno timed automata). }, x-international-audience ={yes}, x-proceedings ={yes}, x-pays = {DE,BE} } @InProceedings{atva09, author = {Cassez, F. and Dubreil, J. and Marchand, H.}, title = {Dynamic Observers for the Synthesis of Opaque Systems}, booktitle = {7th International Symposium on Automated Technology for Verification and Analysis (ATVA'09)}, pages = {352-367}, year = 2009, editor = {Liu, Z. and Ravn, A.P. }, publisher = {Springer-Verlag}, volume = 5799, series = {LNCS}, address = {Macao SAR, China}, month = {October}, pdf = {http://www.irisa.fr/vertecs/Publis/Ps/atva09.pdf}, doi = {http://dx.doi.org/10.1007/978-3-642-04761-9_26}, abstract = {In this paper, we address 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 first investigate the case of static partial observability where the set of events the user can observe is fixed a priori. In this context, we show that checking whether a system is opaque is PSPACE-complete, which implies that computing an optimal static observer 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. We show how to check that a system is opaque w.r.t. to a dynamic observer and also address the corresponding synthesis problem: given a system G and secret states S, compute the set of dynamic observers under which S is opaque. Our main result is that the set of such observers can be finitely represented and can be computed in EXPTIME.}, x-international-audience ={yes}, x-proceedings ={yes} } @TechReport{PI-1930, Author = {Cassez, F. and Dubreil, J. and Marchand, H.}, Title = {Dynamic Observers for the Synthesis of Opaque Systems}, Number = 1930, Institution = {IRISA}, Month = {May}, Year = 2009, abstract = {In this paper, we address 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 first investigate the case of static partial observability where the set of events the user can observe is fixed a priori. In this context, we show that checking whether a system is opaque is PSPACE-complete, which implies that computing an optimal static observer 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. We show how to check that a system is opaque w.r.t. to a dynamic observer and also address the corresponding synthesis problem: given a system G and secret states S, compute the set of dynamic observers under which S is opaque. Our main result is that the set of such observers can be finitely represented and can be computed in EXPTIME.}, pdf = {http://hal.inria.fr/docs/00/39/64/42/PDF/PI-1930.pdf} } @misc{BBG-concur09, author = {Baier, Ch. and Bertrand, N. and Gr{\"o}sser , M.}, title = {The Effect of Tossing Coins in Omega-Automata}, booktitle = {Proceedings of the 20th International Conference on Concurrency Theory (CONCUR'09)}, series = {LNCS}, volume = {5710}, publisher = {Springer}, year = {2009}, pages = {15-29}, note = {Invited talk (C. Baier)}, x-international-audience ={yes}, x-proceedings ={yes}, } @InProceedings{apnoc09, Author = {Dubreil, J.}, Title = {Opacity and Abstraction}, BookTitle = {Proceedings of the First International Workshop on Abstractions for Petri Nets and Other Models of Concurrency (APNOC'09)}, Address = {Paris, France}, Month = {June}, Year = 2009, abstract = { The opacity property characterizes the absence of confidential information flow towards inquisitive attackers. Verifying opacity is well established for finite automata but is known to be not decidable for more expressive models like Turing machines or Petri nets. As a consequence, for a system dealing with confidential information, certifying its confidentiality may be impossible, but attackers can infer confidential information by approximating systems' behaviours. Taking such attackers into account, we investigate the verification of opacity using abstraction techniques to compute executable counterexamples (attack scenarios). Considering a system and a predicate over its executions, attackers are modeled as semi-conservative decision process determining from observed traces the truth of that predicate. Moreover, we will show that the most precise the abstraction is, the most accurate (and then dangerous) the corresponding class of attackers will be. Consequently, when no attack scenario is detected on an approximate analysis, we know that this system is safe against all ``less precise'' attackers. This can therefore be used to provide a level of certification relative to the precision of abstractions.}, pdf = {http://www.irisa.fr/vertecs/Publis/Ps/apnoc09.pdf}, x-international-audience ={yes}, x-proceedings ={yes} } @TechReport{morvan09, author = {Morvan, C.}, title = {Contextual graph grammars characterizing context-sensitive languages}, institution = {IRISA}, year = 2009, number = 1926, month = {March}, abstract = {Deterministic graph grammars generate a family of infinite graphs which characterize context-free (word) languages. In this paper we presents a context-sensitive extension of these grammars. We achieve a characterization of context-sensitive (word) languages. We show that this characterization is not straightforward and that unless having some rigorous restrictions, contextual graph grammars generate non-recursive graphs.}, pdf = {ftp://ftp.irisa.fr/techreports/2009/PI-1926.pdf} } @inproceedings{BLPR-icfem09, author = {Bertrand, N. and Legay, A. and Pinchinat, S. and Raclet, J-P.}, title = {A Compositional Approach on Modal Specifications for Timed Systems}, booktitle = {Proceedings of the 11th International Conference on Formal Engineering Methods (ICFEM'09)}, series = {LNCS}, volume = {5885}, month = {December}, address = {Rio de Janeiro, Brazil}, publisher = {Springer}, pages = {679-697}, year = {2009}, doi ={http://dx.doi.org/10.1007/978-3-642-10373-5_35}, abstract = {On the one hand, modal specifications are classic, convenient, and expressive mathematical objects to represent interfaces of component-based systems. On the other hand, time is a crucial aspect of systems for practical applications, e.g. in the area of embedded systems. And yet, only few results exist on the design of timed component-based systems. In this paper, we propose a timed extension of modal specifications, together with fundamental operations (conjunction, product, and quotient) that enable to reason in a compositional way about timed system. The specifications are given as modal event-clock automata, where clock resets are easy to handle. We develop an entire theory that promotes efficient incremental design techniques. }, pdf = {http://www.irisa.fr/vertecs/Publis/Ps/icfem09.pdf}, x-international-audience ={yes}, x-proceedings ={yes} } @InProceedings{testcom09, author = {Marchand, H. and Dubreil, J. and Jéron, T.}, title = {Automatic Testing of Access Control for Security Properties}, booktitle = {TestCom'09}, year = 2009, month = {November}, pages = {113-128}, publisher = {Springer-Verlag}, volume = 5826, series = {LNCS}, abstract = {In this work, we investigate the combination of controller synthesis and test generation techniques for the testing of open, partially observable systems with respect to security policies. We consider two kinds of properties: integrity properties and confidentiality properties. We assume that the behavior of the system is modeled by a labeled transition system and assume the existence of a black-box implementation. We first outline a method allowing to automatically compute an ideal access control ensuring these two kinds of properties. Then, we show how to derive testers that test the conformance of the implementation with respect to its specification, the correctness of the real access control that has been composed with the implementation in order to ensure a security property, and the security property itself.}, pdf = {http://www.irisa.fr/vertecs/Publis/Ps/testcom09.pdf}, doi ={http://dx.doi.org/10.1007/978-3-642-05031-2}, x-international-audience ={yes}, x-proceedings ={yes} } @InProceedings{sarssi09, author = {Marchand, H. and Dubreil, J. and Jéron, T.}, title = {Génération automatique de tests pour des propriétés de sécurité}, booktitle = {4ème Conférence sur la Sécurité des Architectures Réseaux et des Systèmes d'Information}, pages = {157-174}, year = 2009, month = {June}, confnat = true, Abstract = {Dans cet article, nous nous intéressons à l'utilisation conjointe de techniques de génération automatique de tests et de synthèse de contrôleurs pour tester des propriétés de sécurité. Nous suivons une approche orientée modèle, c'est-à-dire que nous supposons disposer d'une spécification du comportement du système. Sur celle-ci nous étudions la satisfaction de certaines classes de propriétés de confidentialité et d'inté\-grité. Nous proposons une méthode qui consiste à calculer automatiquement un modèle du contrôle d'accès idéal assurant ces deux types de propriétés de sécurité. Nous montrons ensuite comment en dériver des cas de tests qui, exécutés sur l'implémentation, permettent de détecter la non-conformité de l'implémentation et sous certaines hypothèses, la violation des propriétés de sécurité, et une éventuelle mauvaise implémentation du contrôle d'accès mis en place.}, pdf = {http://www.irisa.fr/vertecs/Publis/Ps/Sar-ssi-HM-JD-TJ.pdf}, x-international-audience ={no}, x-proceedings ={yes} } @InProceedings{kalyon09a, author = {Kalyon, G. and Le Gall T. and Marchand, H. and Massart, T.}, title = {Control of Infinite Symbolic Transition Systems under Partial Observation}, booktitle = {European Control Conference}, pages = {1456-1462}, year = 2009, address = {Budapest, Hungary}, month = aout, abstract = {We provide models of safe controllers both for potentially blocking and non blocking controlled systems. To obtain algorithms for these problems, we make the use of abstract interpretation techniques which provide over-approximations of the transitions set to be disabled. To our knowledge, with the hypotheses taken, the improved version of our algorithm provides a better solution than what was previously proposed in the literature. Our tool SMACS allowed us to make an empirical validation of our methods to show their feasibility and usability.}, pdf = {http://www.irisa.fr/vertecs/Publis/Ps/2009-ecc-control.pdf}, x-international-audience ={yes}, x-proceedings ={yes}, x-pays = {BE} } @InProceedings{dubreil09a, author = {Dubreil, J. and Jéron, T. and Marchand, H.}, title = {Monitoring Confidentiality by Diagnosis Techniques}, booktitle = {European Control Conference}, pages = {2584-2590}, year = 2009, address = {Budapest, Hungary}, month = aout, abstract = {We are interested in constructing monitors for the detection of confidential information flow in the context of partially observable discrete event systems. We focus on the case where the secret information is given as a regular language. We first characterize the set of observations allowing an attacker to infer the secret information. Further, based on the diagnosis of discrete event systems, we provide necessary and sufficient conditions under which detection and prediction of secret information flow can be ensured, and construct a monitor allowing an administrator to detect it.}, pdf = {http://www.irisa.fr/vertecs/Publis/Ps/2009-ecc-opacity.pdf}, x-international-audience ={yes}, x-proceedings ={yes}, } @inproceedings{BaierBG09, author = {Baier, C. and Bertrand, N. and Grosser, M.}, title = {Probabilistic Acceptors for Languages over Infinite Words}, booktitle = {35th Conference on Current Trends in Theory and Practice of Computer Science}, year = 2009, volume = 5404, series = {LNCS}, address = {Spindleruv Mlyn, Czech}, pages = {19-33}, abstract = {Probabilistic omega-automata are variants of nondeterministic automata for infinite words where all choices are resolved by probabilistic distributions. Acceptance of an infinite input word requires that the probability for the accepting runs is positive. In this paper, we provide a summary of the fundamental properties of probabilistic omega-automata concerning expressiveness, efficiency, compositionality and decision problems.}, pdf = {http://www.irisa.fr/vertecs/Publis/Ps/2009-sofsem.pdf}, doi = {http://dx.doi.org/10.1007/978-3-540-95891-8_3}, x-international-audience ={yes}, x-proceedings ={yes}, x-pays = {DE} } @InProceedings{lata09, author = {Bertrand, N. and Pinchinat, S. and Raclet, {J.B.}}, title = {Refinement and Consistency of Timed Modal Specifications}, booktitle = {Proceedings of the 3rd International Conference on Language and Automata Theory and Applications (LATA'09)}, series = {LNCS}, volume = 5457, pages = {152-163}, year = 2009, address = {Tarragona, Spain}, month = avril, abstract = {In the application domain of component-based system design, developing theories which support compositional reasoning is notoriously challenging. We define timed modal specifications, an automata-based formalism combining modal and timed aspects. As a stepping stone to compositional approaches of timed systems, we define the notions of refinement and consistency, and establish their decidability.}, pdf = {http://www.irisa.fr/vertecs/Publis/Ps/BPR-lata09.pdf}, doi = {http://dx.doi.org/10.1007/978-3-642-00982-2_13}, x-international-audience ={yes}, x-proceedings ={yes} } @PhdThesis{dubreil-phd, author = {Dubreil, Jérémy}, title = {Monitoring and Supervisory Control for Opacity Properties}, school = {Université de Rennes 1}, year = {2009}, month = {November}, abstract ={Les systèmes fonctionnant sur un réseau ouvert tels que les bases de données médicales ou les systèmes bancaires peuvent manipuler des informations dont la confidentialité doit être impérativement préservée. Dans ce contexte, la notion d'opacité formalise la capacité d'un système à garder secrètes certaines informations critiques. Dans cette thèse, nous nous intéressons à la fois à vérifier que la propriété d'opacité est satisfaite et à la synthèse de systèmes opaques. Vérifier l'opacité est un problème décidable pour des systèmes de transition finis. Pour les systèmes infinis, nous étudions l'application de techniques d'interprétation abstraite à la détection de vulnérabilité. Nous présentons aussi une méthode alternative qui s'appuie sur des abstractions régulières et sur des techniques de diagnostique pour détecter de telles vulnérabilité à l'exécution du système. Pour la synthèse de système opaque, nous appliquons dans un premier temps la théorie du contrôle à la Ramadge et Wonham pour calculer un contrôleur assurant l'opacité. Nous montrons que les techniques habituelles de synthèse de contrôleur ne peuvent être appliqué pour ce problème d'opacité et nous développons alors de nouveaux algorithmes pour calculer l'unique système opaque qui soit maximal au sens de l'inclusion des langages. Ces résultats sont à rapprocher des techniques de construction de système sécurisé par assemblage de composant. Finalement, nous présentons une autre approche pour la synthèse de système opaque qui consiste à synthétiser un filtre qui décide, dynamiquement, de masquer des événements observable afin d'éviter que de l'information secrète ne soit révélée. Ceci permet d'étudier dans un cadre formel la synthèse automatique de pare-feu assurant la confidentialité de certaines informations critiques.} pdf = {http://www.irisa.fr/vertecs/Publis/Ps/These_dubreil.pdf}, } @TECHREPORT{PI-1921, author = {Dubreil, J. and Darondeau, Ph. and Marchand, H.}, title = {Supervisory Control for Opacity}, institution = {IRISA}, year = 2009, number = 1921, month = fevrier, abstract = {In the field of computer security, a problem that received little attention so far is the enforcement of confidentiality properties by supervisory control. Given a critical system G that may leak confidential information, the problem consists in designing a controller C, possibly disabling occurrences of a fixed subset of events of G, so that the closed-loop system G/C does not leak confidential information. We consider this problem in the case where G is a finite transition system with set of events A and an inquisitive user, called the adversary, observes a subset Aa of A. The confidential information is the fact (when it is true) that the trace of the execution of G on A* belongs to a regular set S in A, called the secret. The secret S is said to be opaque w.r.t. G (resp. G/C) and Aa if the adversary cannot safely infer this fact from the trace of the execution of G (resp. G/C) on Aa*. In the converse case, the secret can be disclosed. We present an effective algorithm for computing the most permissive controller C such that S is opaque w.r.t. G/C and Aa. This algorithm subsumes two earlier algorithms working under the strong assumption that the alphabet Aa of the adversary and the set of events that the controller can disable are comparable.}, pdf = {http://www.irisa.fr/vertecs/Publis/Ps/PI-1921.pdf} }