Search

Restarts are used in many computer systems to improve performance. Examples include reloading a webpage, reissuing a request, or restarting a randomized search. The design of restart strategies has been extensively studied by the performance evaluation community. In this paper, we address the problem of designing universal restart strategies, valid for arbitrary finite-state Markov chains, that enforce a given ω-regular property while not knowing the chain. A strategy enforces a property φ if, with probability 1, the number of restarts is finite, and the run of the Markov chain after the last restart satisfies φ. We design a simple "cautious" strategy that solves the problem, and a more sophisticated "bold" strategy with an almost optimal number of restarts., LIPIcs, Vol. 203, 32nd International Conference on Concurrency Theory (CONCUR 2021), pages 5:1-5:22

In the new generation of message-based systems such as network-based smart systems, distributed components collaborate via asynchronous message passing. In some cases, particular ordering among the messages may lead to violation of the desired properties such as data confidentiality. Due to the absence of a global clock and usage of off-the-shelf components, there is no control over the order of messages at design time. To make such systems safe, we propose a choreography-based runtime enforcement algorithm that given an automata-based specification of unwanted message sequences, prevents certain messages to be sent, and assures that the unwanted sequences are not formed. Our algorithm is fully decentralized in the sense that each component is equipped with a monitor, as opposed to having a centralized monitor. As there is no global clock in message-based systems, the order of messages cannot be determined exactly. In this way, the monitors behave conservatively in the sense that they prevent a message from being sent, even when the sequence may not be formed. We aim to minimize conservative prevention in our algorithm when the message sequence has not been formed. The efficiency and scalability of our algorithm are evaluated in terms of the communication overhead and the blocking duration through simulation., LIPIcs, Vol. 184, 24th International Conference on Principles of Distributed Systems (OPODIS 2020), pages 21:1-21:18

With the explosion of Industry 4.0, industrial facilities and critical infrastructures are transforming into “smart” systems that dynamically adapt to external events. The result is an ecosystem of heterogeneous physical and cyber components, such as programmable logic controllers, which are more and more exposed to cyber-physical attacks, i.e., security breaches in cyberspace that adversely affect the physical processes at the core of industrial control systems. We apply runtime enforcement techniques, based on an ad-hoc sub-class of Ligatti et al.’s edit automata, to enforce specification compliance in networks of potentially compromised controllers, formalised in Hennessy and Regan’s Timed Process Language. We define a synthesis algorithm that, given an alphabet $\mathcal{P}$ of observable actions and an enforceable regular expression e capturing a timed property for controllers, returns a monitor that enforces the property e during the execution of any (potentially corrupted) controller with alphabet $\mathcal{P}$ and complying with the property e. Our monitors correct and suppress incorrect actions coming from corrupted controllers and emit actions in full autonomy when the controller under scrutiny is not able to do so in a correct manner. Besides classical properties, such as transparency and soundness, the proposed enforcement ensures non-obvious properties, such as polynomial complexity of the synthesis, deadlock-and diverge-freedom of monitored controllers, together with scalability when dealing with networks of controllers.

Many implantable medical devices, such as pacemakers, have been recalled due to failure of their embedded software. This motivates rethinking their design and certification processes. We propose, for the first time, an additional layer of safety by formalising the problem of run-time enforcement of implantable pacemakers. While recent work has formalised run-time enforcement of reactive systems, the proposed framework generalises existing work along the following directions: (1) we develop bi-directional enforcement, where the enforced policies depend not only on the status of the pacemaker (the controller) but also of the heart (the plant), thus formalising the run-time enforcement problem for cyber-physical systems (2) we express policies using a variant of discrete timed automata (DTA), which can cover all regular properties unlike earlier frameworks limited to safety properties, (3) we are able to ensure the timing safety of implantable devices through the proposed enforcement, and (4) we show that the DTA-based approach is efficient relative to its dense time variant while ensuring that the discretisation error is relatively small and bounded. The developed approach is validated through a prototype system implemented using the open source KIELER framework. The experiments show that the framework incurs minimal runtime overhead.

Android applications are executed on smartphones equipped with a variety of resources that must be properly accessed and controlled, otherwise the correctness of the executions and the stability of the entire environment might be negatively affected. For example, apps must properly acquire, use, and release microphones, cameras, and other multimedia devices otherwise the behavior of the apps that use the same resources might be compromised. Unfortunately, several apps do not use resources correctly, for instance due to faults and inaccurate design decisions. By interacting with these apps users may experience unexpected behaviors, which in turn may cause instability and sporadic failures, especially when resources are accessed. In this paper, we present an approach that lets users protect their environment from the apps that use resources improperly by enforcing the correct usage protocol. This is achieved by using software enforcers that can observe executions and change them when necessary. For instance, enforcers can detect that a resource has been acquired but not released, and automatically perform the release operation, thus giving the possibility to use that same resource to the other apps. The main idea is that software libraries, in particular the ones controlling access to resources, can be augmented with enforcers that can be activated and deactivated on demand by users to protect their environment from unwanted app behaviors. We call the software libraries augmented with one or more enforcers proactive libraries because the activation of the enforcer decorates the library with proactive behaviors that can guarantee the correctness of the execution despite the invocation of the operations implemented by the library., accepted for publication in ACM Transactions on Autonomous and Adaptive Systems (TAAS). Special Section on Best Papers from SEAMS 2017 (The conference paper is arXiv:1703.08005)

The complex architecture of browser technologies and dynamic characteristics of JavaScript make it difficult to ensure security in client-side web applications. Browser-level security policies alone are not sufficient because it is difficult to apply them correctly and they can be bypassed. As a result, they need to be completed by application-level security policies. In this paper, we survey existing solutions for specifying and enforcing application-level security policies for client-side web applications, and distill a number of desirable features. Based on these features we developed Guardia, a framework for declaratively specifying and dynamically enforcing application-level security policies for JavaScript web applications without requiring VM modifications. We describe Guardia enforcement mechanism by means of JavaScript reflection with respect to three important security properties (transparency, tamper-proofness, and completeness). We also use Guardia to specify and deploy 12 access control policies discussed in related work in three experimental applications that are representative of real-world applications. Our experiments indicate that Guardia is correct, transparent, and tamper-proof, while only incurring a reasonable runtime overhead.

This thesis studies the runtime enforcement of timed properties when some events are uncontrollable. This work falls in the domain of runtime verification, which includes all the techniques and tools based on or related to the monitoring of system executions with respect to requirement properties. These properties can be specified using different models such as logic formulae or automata. We consider timed regular properties, that can be represented by timed automata. As for runtime verification, a runtime enforcement mechanism watches the executions of a system, but instead of just outputting a verdict, it modifies the execution so that it satisfies the property. We are interested in runtime enforcement with uncontrollable events. An uncontrollable event is an event that an enforcement mechanism can not modify. We describe the synthesis of enforcement mechanisms, in both a functional and an operational way, that enforce some desired timed regular property. We define two equivalent enforcement mechanisms, the first one being simple, without considering complexity aspects, whereas the second one has a better time complexity thanks to the use of game theory; the latter being better suited for implementation. We also detail a tool that implements the second enforcement mechanism, as well as some performance considerations. The overhead introduced by the use of our tool seems low enough to be used in some real-time application scenarios., Cette thèse étudie l’enforcement de propriétés temporisées à l’exécution en présence d’évènements incontrôlables. Les travaux se placent dans le cadre plus général de la vérification à l’exécution qui vise à surveiller l’exécution d’un système afin de s’assurer qu’elle respecte certaines propriétés. Ces propriétés peuvent être spécifiées à l’aide de formules logiques, ou au moyen d’autres modèles formels, parfois équivalents, comme des automates. Nous nous intéressons à l’enforcement à l’exécution de propriétés spécifiées par des automates temporisés. Tout comme la vérification à l’exécution, l’enforcement à l’exécution surveille l’exécution d’un système, la différence étant qu’un mécanisme d’enforcement réalise certaines modifications sur l’exécution afin de la contraindre à satisfaire la propriété souhaitée. Nous étudions plus particulièrement l’enforcement à l’exécution lorsque certains évènements de l’exécution sont incontrôlables, c’est-à-dire qu’ils ne peuvent pas être modifiés par un mécanisme d’enforcement. Nous définissons des algorithmes de synthèse de mécanismes d’enforcement décrits de manières fonctionnelle puis opérationnelle, à partir de propriétés temporisées régulières (pouvant être représentées par des automates temporisés). Ainsi, deux mécanismes d’enforcement équivalents sont définis, le premier présentant une approche correcte sans considération d’implémentation, alors que le second utilise une approche basée sur la théorie des jeux permettant de précalculer certains comportements, ce qui permet de meilleures performances. Une implémentation utilisant ce précalcul est également présentée et évaluée. Les résultats sont encourageant quant à la faisabilité de l’enforcement à l’exécution en temps réel, avec des temps supplémentaires suffisamment courts sur de petites propriétés pour permettre une utilisation de tels systèmes.

Policy enforcers are sophisticated runtime components that can prevent failures by enforcing the correct behavior of the software. While a single enforcer can be easily designed focusing only on the behavior of the application that must be monitored, the effect of multiple enforcers that enforce different policies might be hard to predict. So far, mechanisms to resolve interferences between enforcers have been based on priority mechanisms and heuristics. Although these methods provide a mechanism to take decisions when multiple enforcers try to affect the execution at a same time, they do not guarantee the lack of interference on the global behavior of the system. In this paper we present a verification strategy that can be exploited to discover interferences between sets of enforcers and thus safely identify a-priori the enforcers that can co-exist at run-time. In our evaluation, we experimented our verification method with several policy enforcers for Android and discovered some incompatibilities., Comment: Oliviero Riganelli, Daniela Micucci, Leonardo Mariani, and Yli\`es Falcone. Verifying Policy Enforcers. Proceedings of 17th International Conference on Runtime Verification (RV), 2017. (to appear)

International audience; Runtime enforcement (RE) is a technique to ensure that the (untrustworthy) output of a black-box system satisfies some desired properties. In RE, the output of the running system, modeled as a sequence of events, is fed into an enforcer. The enforcer ensures that the sequence complies with a certain property, by delaying or modifying events if necessary. This paper deals with predictive runtime enforcement, where the system is not entirely black-box, but we know something about its behavior. This a priori knowledge about the system allows to output some events immediately, instead of delaying them until more events are observed, or even blocking them permanently. This in turn results in better enforcement policies. We also show that if we have no knowledge about the system, then the proposed enforcement mechanism reduces to standard (non-predictive) runtime enforcement. All our results related to predictive RE of untimed properties are also formalized and proved in the Isabelle theorem prover. We also discuss how our predictive runtime enforcement framework can be extended to enforce timed properties.

International audience; Runtime enforcement is a verification/validation technique aiming at correcting possibly incorrect executions of a system of interest. In this paper, we consider enforcement monitoring for systems where the physical time elapsing between actions matters. Executions are thus modelled as timed words (i.e., sequences of actions with dates). We consider runtime enforcement for timed specifications modelled as timed automata. Our enforcement mechanisms have the power of both delaying events to match timing constraints, and suppressing events when no delaying is appropriate, thus possibly allowing for longer executions. To ease their design and their correctness-proof, enforcement mechanisms are described at several levels: enforcement functions that specify the input-output behaviour in terms of transformations of timed words, constraints that should be satisfied by such functions, enforcement monitors that describe the operational behaviour of enforcement functions, and enforcement algorithms that describe the implementation of enforcement monitors. The feasibility of enforcement monitoring for timed properties is validated by prototyping the synthesis of enforcement monitors from timed automata.

Copyright © 2015 by the Association for Computing Machinery, Inc. (ACM). Security enforcement mechanisms like execution monitors are used to make sure that some untrusted program complies with a policy. Different enforcement mechanisms have different strengths and weaknesses and hence it is important to understand the qualities of various enforcement mechanisms. This paper studies runtime enforcement mechanisms for reactive programs. We study the impact of two important constraints that many practical enforcement mechanisms satisfy: (1) the enforcement mechanism must handle each input/output event in finite time and on occurrence of the event (as opposed to for instance Ligatti's edit automata that have the power to buffer events for an arbitrary amount of time), and (2) the enforcement mechanism treats the untrusted program as a black box: it can monitor and/or edit the input/output events that the program exhibits on execution and it can explore alternative executions of the program by running additional copies of the program and providing these different inputs. It can not inspect the source or machine code of the untrusted program. Such enforcement mechanisms are important in practice: They include for instance many execution monitors, virtual machine monitors, and secure multi-execution or shadow executions. We establish upper and lower bounds for the class of policies that are enforceable by such black box mechanisms, and we propose a generic enforcement mechanism that works for a wide range of policies.We also show how our generic enforcement mechanism can be instantiated to enforce specific classes of policies, at the same time showing that many existing enforcement mechanisms are optimized instances of our construction. ispartof: Proceedings of the 42nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2015) vol:50 issue:1 pages:43-54 ispartof: location:Mumbai, India status: published

Runtime enforcement techniques are introduced in the literature to cope with the failures that occur while software is being executed in its target environment. These techniques may also offer diagnosis and recovery actions to respectively identify the causes of the failures and to heal them. Since the development of runtime enforcement techniques can be complex, error-prone and costly, runtime enforcement frameworks are proposed to ease the development process. To this aim, these frameworks support various languages to specify the desired properties of software, to express the necessary diagnosis rules for detecting the causes of failures, and to define the recovery strategies. Based on the specifications, runtime enforcement frameworks generate code and integrate it with the software to be verified and/or healed. The code is usually generated in the same language that is used to implement the software, or in an intermediate language that abstracts the software. Unfortunately, the specification languages employ the elements of the programming languages of the generated code, and therefore, they fall short in representing the runtime enforcement concepts naturally. By the term concept we mean a fundamental abstraction or definition that exists in most runtime enforcement techniques. As a result, implementation of runtime enforcement concepts may suffer from scattering and tangling. This reduces the modularity and compose-ability of the specifications of runtime enforcement concepts. Moreover, adoption of the elements of the underlying languages in specifications causes the specifications to become too specific to the employed programming languages and platforms. This reduces the reusability and comprehensibility of the specifications, and increases their complexity. To facilitate a natural representation of runtime enforcement concepts, this thesis introduces a computation model termed as Event Composition Model, which respects the characteristic features of the runtime enforcement concepts. This computation model offers a set of novel linguistic abstractions, called events, event modules, reactors, reactor chains, event composition language and event constraint language. Events represent changes in the states of interest. Event modules are means to group events, have input- output interfaces, and implementations. Reactors are the implementations of event modules. Reactor chains are groups of related reactors that process events in a sequence. The event composition language facilitates selecting the events of interest; and the event constraint language facilitates defining constraints among reactors or event modules. An important issue is how to implement Event Composition Model effectively, by using current programming languages. For this purpose, the thesis evaluates the relevant programming languages with respect to their support for implementing Event Composition Model. The evaluation reveals that none of the existing languages can implement the model such that the desired quality attributes, such as modularity, abstractness and compose-ability are accomplished. Nevertheless, aspect-oriented languages offer promising features for this matter. The thesis introduces the EventReactor language, as the successor of the Compose* aspect-oriented language, that implements Event Composition Model. The language is open-ended for new sorts of events and reactor types. This helps to represent new sorts of concepts. It makes use of the Prolog language as its event composition language. Reactors and reactor chains are parameterizable, and are defined separately from event modules. This increases the reusability of event modules and their implementations. The systems of today are more and more implemented using multiple languages and this trend seems to continue also in the near future. The current runtime enforcement frameworks, unfortunately, fall short in supporting software implemented in different programming languages. In Event Composition Model, the event composition language facilitates selecting events from systems implemented in various languages. In the EventReactor language, the specifications are defined independently from any programming language, and the compiler of EventReactor facilitates generating code for Java, C and .Net languages. As a result, the specifications can be reused for software developed in different languages. It is now more and more usual that applications are designed to run on distributed system architectures. Unfortunately, most runtime enforcement frameworks cannot be utilized for distributed systems. There are a few runtime enforcement frameworks that can work with distributed architectures. These systems, however, adopt specifications that contain information about the underlying process structure. This increases the complexity and reduces the reusability of the specifications if the process structure of software changes. The EventReactor language addresses this problem with the support of distribution transparency. There are two basic ways in utilizing the EventReactor language: a) as an underlying language for the specification languages of runtime enforcement frameworks; b) as an implementation language of runtime enforcement techniques. This thesis explains Event Composition Model, its implementation the EventReactor language, and the compiler of this language with the use of illustrative examples. The thesis makes use of an example runtime enforcement technique called Recoverable Process to evaluate the suitability of the EventReactor language in representing the concepts of interest naturally.

Runtime enforcement techniques are introduced in the literature to cope with the failures that occur while software is being executed in its target environment. These techniques may also offer diagnosis and recovery actions to respectively identify the causes of the failures and to heal them. Since the development of runtime enforcement techniques can be complex, error-prone and costly, runtime enforcement frameworks are proposed to ease the development process. To this aim, these frameworks support various languages to specify the desired properties of software, to express the necessary diagnosis rules for detecting the causes of failures, and to define the recovery strategies. Based on the specifications, runtime enforcement frameworks generate code and integrate it with the software to be verified and/or healed. The code is usually generated in the same language that is used to implement the software, or in an intermediate language that abstracts the software. Unfortunately, the specification languages employ the elements of the programming languages of the generated code, and therefore, they fall short in representing the runtime enforcement concepts naturally. By the term concept we mean a fundamental abstraction or definition that exists in most runtime enforcement techniques. As a result, implementation of runtime enforcement concepts may suffer from scattering and tangling. This reduces the modularity and compose-ability of the specifications of runtime enforcement concepts. Moreover, adoption of the elements of the underlying languages in specifications causes the specifications to become too specific to the employed programming languages and platforms. This reduces the reusability and comprehensibility of the specifications, and increases their complexity. To facilitate a natural representation of runtime enforcement concepts, this thesis introduces a computation model termed as Event Composition Model, which respects the characteristic features of the runtime enforcement concepts. This computation model offers a set of novel linguistic abstractions, called events, event modules, reactors, reactor chains, event composition language and event constraint language. Events represent changes in the states of interest. Event modules are means to group events, have input- output interfaces, and implementations. Reactors are the implementations of event modules. Reactor chains are groups of related reactors that process events in a sequence. The event composition language facilitates selecting the events of interest; and the event constraint language facilitates defining constraints among reactors or event modules. An important issue is how to implement Event Composition Model effectively, by using current programming languages. For this purpose, the thesis evaluates the relevant programming languages with respect to their support for implementing Event Composition Model. The evaluation reveals that none of the existing languages can implement the model such that the desired quality attributes, such as modularity, abstractness and compose-ability are accomplished. Nevertheless, aspect-oriented languages offer promising features for this matter. The thesis introduces the EventReactor language, as the successor of the Compose* aspect-oriented language, that implements Event Composition Model. The language is open-ended for new sorts of events and reactor types. This helps to represent new sorts of concepts. It makes use of the Prolog language as its event composition language. Reactors and reactor chains are parameterizable, and are defined separately from event modules. This increases the reusability of event modules and their implementations. The systems of today are more and more implemented using multiple languages and this trend seems to continue also in the near future. The current runtime enforcement frameworks, unfortunately, fall short in supporting software implemented in different programming languages. In Event Composition Model, the event composition language facilitates selecting events from systems implemented in various languages. In the EventReactor language, the specifications are defined independently from any programming language, and the compiler of EventReactor facilitates generating code for Java, C and .Net languages. As a result, the specifications can be reused for software developed in different languages. It is now more and more usual that applications are designed to run on distributed system architectures. Unfortunately, most runtime enforcement frameworks cannot be utilized for distributed systems. There are a few runtime enforcement frameworks that can work with distributed architectures. These systems, however, adopt specifications that contain information about the underlying process structure. This increases the complexity and reduces the reusability of the specifications if the process structure of software changes. The EventReactor language addresses this problem with the support of distribution transparency. There are two basic ways in utilizing the EventReactor language: a) as an underlying language for the specification languages of runtime enforcement frameworks; b) as an implementation language of runtime enforcement techniques. This thesis explains Event Composition Model, its implementation the EventReactor language, and the compiler of this language with the use of illustrative examples. The thesis makes use of an example runtime enforcement technique called Recoverable Process to evaluate the suitability of the EventReactor language in representing the concepts of interest naturally.

International audience; Runtime enforcement is a powerful technique to ensure that a program will respect a given set of properties. We extend previous work on this topic in several directions. Firstly, we propose a generic notion of enforcement monitors based on a memory device and finite sets of control states and enforcement operations. Moreover, we specify their enforcement abilities w.r.t. the general Safety-Progress classification of properties. Furthermore, we propose a systematic technique to produce a monitor from the automaton recognizing a given safety, guarantee, obligation or response property. Finally, we show that this notion of enforcement monitors is more amenable to implementation and encompasses previous runtime enforcement mechanisms.

International audience; The underlying property, its definition and representation play a major role when monitoring a system. Having a suitable and convenient framework to express properties is thus a concern for runtime analysis. It is desirable to delineate in this framework the sets of properties for which runtime analysis approaches can be applied to. This paper presents a unified view of runtime verification and enforcement of properties in the Safety-Progress classification. Firstly, we extend the Safety-Progress classification of properties in a runtime context. Secondly, we characterize the set of properties which can be verified (monitorable properties) and enforced (enforceable properties) at runtime. We propose in particular an alternative definition of ''property monitoring'' to the one classically used in this context. Finally, for the delineated sets of properties, we define specialized verification and enforcement monitors.