Search

Your search keyword '"runtime enforcement"' showing total 11 results
Start Over Descriptor "runtime enforcement" Topic computer security
11 results on '"runtime enforcement"'

1. INVITED: Safety Guard: Runtime Enforcement for Safety-Critical Cyber-Physical Systems.

Author

Meng Wu, Haibo Zeng, Chao Wang, and Huafeng Yu

Subjects
COMPUTER security, COMPUTER systems, DATA privacy, DATA security, MALWARE
Abstract

Due to their safety-critical nature, cyber-physical systems (CPS) must tolerate faults and security attacks to remain fail-operational. However, conventional techniques for improving safety, such as testing and validation, do not meet this requirement, as shown by many of the real-world system failures in recent years, often with major economic and public-safety implications. We aim to improve the safety of critical CPS through synthesis of runtime enforcers, named safety guards, which are reactive components attached to the original systems to protect them against catastrophic failures. That is, even if the system occasionally malfunctions due to unknown defects, transient errors, or malicious attacks, the guard always reacts instantaneously to ensure that the combined system satisfies a predefined set of safety properties, and the deviation from the original system is kept at minimum. We illustrate the main ideas of this approach with examples, discuss the advantages compared to existing approaches, and point out some research challenges. [ABSTRACT FROM AUTHOR]

Published
2017
Full Text
View/download PDF

2. Modeling runtime enforcement with mandatory results automata.

Author

Dolzhenko, Egor, Ligatti, Jay, and Reddy, Srikar

Subjects
*COMPUTER security, *COMPUTER security software, *MACHINE theory, *DATA security, *COMMON Language Runtime (Computer science), *DATA analysis
Abstract

This paper presents a theory of runtime enforcement based on mechanism models called mandatory results automata (MRAs). MRAs can monitor and transform security-relevant actions and their results. The operational semantics of MRAs is simple and enables straightforward definitions of concrete MRAs. Moreover, the definitions of policies and enforcement with MRAs are simple and expressive. Putting all of these features together, we argue that MRAs make good general models of runtime mechanisms, upon which a theory of runtime enforcement can be based. We develop some enforceability theory by characterizing the policies deterministic and non-deterministic MRAs can and cannot enforce. [ABSTRACT FROM AUTHOR]

Published
2015
Full Text
View/download PDF

3. Runtime enforcement monitors: composition, synthesis, and enforcement abilities.

Author

Falcone, Yliès, Mounier, Laurent, Fernandez, Jean-Claude, and Richier, Jean-Luc

Subjects
ROBOT programming, COMPUTER software execution, TECHNOLOGICAL complexity, MACHINE theory, ROBOTICS, COMPUTER security, BOOLEAN algebra, AUTOMATION, COMPUTER logic
Abstract

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. [ABSTRACT FROM AUTHOR]

Published
2011
Full Text
View/download PDF

4. Controlling Interactions with Libraries in Android Apps Through Runtime Enforcement

Author

Daniela Micucci, Leonardo Mariani, Oliviero Riganelli, Riganelli, O, Micucci, D, and Mariani, L

Subjects
Proactive library, FOS: Computer and information sciences, Correctness, Resource usage, Computer science, Self-healing, 02 engineering and technology, Computer security, computer.software_genre, ING-INF/05 - SISTEMI DI ELABORAZIONE DELLE INFORMAZIONI, Computer Science - Software Engineering, Software, Android, On demand, Policy enforcement, 0202 electrical engineering, electronic engineering, information engineering, Computer Science (miscellaneous), Android (operating system), Enforcement, Runtime enforcement, business.industry, INF/01 - INFORMATICA, 020207 software engineering, Resource leak, Software Engineering (cs.SE), Control and Systems Engineering, 020201 artificial intelligence & image processing, business, computer, Proactive library, self-healing, Android, resource leak, resource usage, policy enforcement, runtime enforcement
Abstract

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)

Published
2019

5. GUARDIA: specification and enforcement of javascript security policies without VM modifications

Author

Jens Nicolay, Elisa Gonzalez Boix, Angel Luis Scull Pupo, Informatics and Applied Informatics, Faculty of Sciences and Bioengineering Sciences, and Software Languages Lab

Subjects
JavaScript, Reflection (computer programming), Computer science, Computer Networks and Communications, Security policy, Overhead (engineering), Access control, Reflection, 0102 computer and information sciences, 02 engineering and technology, web security, Internet security, Computer security, computer.software_genre, 01 natural sciences, DSL, Runtime Enforcement, human-computer interaction, 0202 electrical engineering, electronic engineering, information engineering, Web application, computer.programming_language, business.industry, 020207 software engineering, Transparency (human–computer interaction), Language Design, 010201 computation theory & mathematics, Computer Vision and Pattern Recognition, business, computer, Software
Abstract

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.

Published
2018
Full Text
View/download PDF

6. Verifying Policy Enforcers

Author

Leonardo Mariani, Daniela Micucci, Yliès Falcone, Oliviero Riganelli, Università degli Studi di Milano-Bicocca = University of Milano-Bicocca (UNIMIB), Université Grenoble Alpes [2016-2019] (UGA [2016-2019]), Compiler Optimization and Run-time Systems (CORSE), Inria Grenoble - Rhône-Alpes, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire d'Informatique de Grenoble (LIG ), Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Centre National de la Recherche Scientifique (CNRS)-Université Grenoble Alpes [2016-2019] (UGA [2016-2019])-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Centre National de la Recherche Scientifique (CNRS)-Université Grenoble Alpes [2016-2019] (UGA [2016-2019]), Laboratoire d'Informatique de Grenoble (LIG ), Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Centre National de la Recherche Scientifique (CNRS)-Université Grenoble Alpes [2016-2019] (UGA [2016-2019]), Università degli Studi di Milano-Bicocca [Milano] (UNIMIB), Riganelli, O, Micucci, D, Mariani, L, and Falcone, Y

Subjects
FOS: Computer and information sciences, Computer science, Formal Languages and Automata Theory (cs.FL), Computer Science - Formal Languages and Automata Theory, 02 engineering and technology, [INFO.INFO-SE]Computer Science [cs]/Software Engineering [cs.SE], Computer security, computer.software_genre, Computer Science - Software Engineering, Software, Android, Policy enforcement, policy enforcement, 0202 electrical engineering, electronic engineering, information engineering, self-healing, Android (operating system), business.industry, proactive library, INF/01 - INFORMATICA, 020207 software engineering, resource usage, Software Engineering (cs.SE), runtime enforcement, API, Proactive library, Self-healing, Android, Resource usage, API, Policy enforcement, Runtime enforcement, 020201 artificial intelligence & image processing, [INFO.INFO-ES]Computer Science [cs]/Embedded Systems, Heuristics, business, computer
Abstract

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)

Published
2017

7. Predictive runtime enforcement

Author

Stavros Tripakis, Viorel Preoteasa, Yliès Falcone, Thierry Jéron, Srinivas Pinisetty, Hervé Marchand, Aalto University, Lawrence Berkeley National Laboratory [Berkeley] (LBNL), SUpervision of large MOdular and distributed systems (SUMO), Inria Rennes – Bretagne Atlantique, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-LANGAGE ET GÉNIE LOGICIEL (IRISA-D4), Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA), Université de Rennes (UR)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-IMT Atlantique (IMT Atlantique), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT)-Université de Rennes (UR)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT)-Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-IMT Atlantique (IMT Atlantique), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT), Compiler Optimization and Run-time Systems (CORSE), Inria Grenoble - Rhône-Alpes, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire d'Informatique de Grenoble (LIG ), Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Centre National de la Recherche Scientifique (CNRS)-Université Grenoble Alpes [2016-2019] (UGA [2016-2019])-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Centre National de la Recherche Scientifique (CNRS)-Université Grenoble Alpes [2016-2019] (UGA [2016-2019]), Université de Bretagne Sud (UBS)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National de Recherche en Informatique et en Automatique (Inria)-École normale supérieure - Rennes (ENS Rennes)-Centre National de la Recherche Scientifique (CNRS)-Université de Rennes 1 (UR1), Université de Rennes (UNIV-RENNES)-CentraleSupélec-IMT Atlantique Bretagne-Pays de la Loire (IMT Atlantique), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT)-Université de Bretagne Sud (UBS)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-École normale supérieure - Rennes (ENS Rennes)-Centre National de la Recherche Scientifique (CNRS)-Université de Rennes 1 (UR1), Berkeley University of California (UC BERKELEY), LANGAGE ET GÉNIE LOGICIEL (IRISA-D4), Université de Rennes 1 (UR1), Université de Rennes (UNIV-RENNES)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Institut National de Recherche en Informatique et en Automatique (Inria)-Télécom Bretagne-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-Université de Rennes 1 (UR1), Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Institut National de Recherche en Informatique et en Automatique (Inria)-Télécom Bretagne-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA), Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Institut National de Recherche en Informatique et en Automatique (Inria)-Télécom Bretagne-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-Inria Rennes – Bretagne Atlantique, Institut National de Recherche en Informatique et en Automatique (Inria), ACM, University of California [Berkeley] (UC Berkeley), University of California (UC), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Institut National de Recherche en Informatique et en Automatique (Inria)-Télécom Bretagne-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-Université de Rennes (UR)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Institut National de Recherche en Informatique et en Automatique (Inria)-Télécom Bretagne-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA), and Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Télécom Bretagne-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)

Subjects
Monitoring, Property (programming), Computer science, Distributed computing, 0211 other engineering and technologies, 02 engineering and technology, [INFO.INFO-SE]Computer Science [cs]/Software Engineering [cs.SE], Co-simulation, Computer security, computer.software_genre, Automata, Theoretical Computer Science, 0202 electrical engineering, electronic engineering, information engineering, Enforcement, Timed automata, Runtime enforcement, ta113, Monitor synthesis, 021110 strategic, defence & security studies, Sequence, Runtime verification, 020207 software engineering, Blocking (computing), Automaton, Automated theorem proving, Hardware and Architecture, 020201 artificial intelligence & image processing, [INFO.INFO-ES]Computer Science [cs]/Embedded Systems, Runtime monitoring, computer, Software
Abstract

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.

Published
2017
Full Text
View/download PDF

8. Runtime enforcement using Büchi games

Author

Yliès Falcone, Matthieu Renard, Antoine Rollet, Laboratoire Bordelais de Recherche en Informatique (LaBRI), Université de Bordeaux (UB)-Centre National de la Recherche Scientifique (CNRS)-École Nationale Supérieure d'Électronique, Informatique et Radiocommunications de Bordeaux (ENSEIRB), Institut Polytechnique de Bordeaux (Bordeaux INP), Université Grenoble Alpes [2016-2019] (UGA [2016-2019]), Compiler Optimization and Run-time Systems (CORSE), Inria Grenoble - Rhône-Alpes, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire d'Informatique de Grenoble (LIG ), Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Centre National de la Recherche Scientifique (CNRS)-Université Grenoble Alpes [2016-2019] (UGA [2016-2019])-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Centre National de la Recherche Scientifique (CNRS)-Université Grenoble Alpes [2016-2019] (UGA [2016-2019]), Laboratoire d'Informatique de Grenoble (LIG ), Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Centre National de la Recherche Scientifique (CNRS)-Université Grenoble Alpes [2016-2019] (UGA [2016-2019]), Région Nouvelle-Aquitaine, Bordeaux INP, ACM, and Université de Bordeaux (UB)-École Nationale Supérieure d'Électronique, Informatique et Radiocommunications de Bordeaux (ENSEIRB)-Centre National de la Recherche Scientifique (CNRS)

Subjects
021110 strategic, defence & security studies, [INFO.INFO-GT]Computer Science [cs]/Computer Science and Game Theory [cs.GT], Computer science, Distributed computing, Runtime verification, Runtime Verification, 0211 other engineering and technologies, 020207 software engineering, 02 engineering and technology, 16. Peace & justice, Computer security, computer.software_genre, Automata, Automaton, [INFO.INFO-FL]Computer Science [cs]/Formal Languages and Automata Theory [cs.FL], Runtime Enforcement, [INFO.INFO-SY]Computer Science [cs]/Systems and Control [cs.SY], 0202 electrical engineering, electronic engineering, information engineering, Leverage (statistics), Games, Enforcement, Computer Science::Operating Systems, computer
Abstract

International audience; We leverage Büchi games for the runtime enforcement of regular properties with uncontrollable events. Runtime enforcement consists in modifying the execution of a running system to have it satisfy a given regular property, modelled by an automaton. We revisit runtime enforcement with uncontrollable events and propose a framework where we model the runtime enforcement problem as a Büchi game and synthesise sound, compliant, and optimal enforcement mechanisms as strategies. We present algorithms and a tool implementing enforcement mechanisms. We reduce the complexity of the computations performed by enforcement mechanisms at runtime by pre-computing decisions of enforcement mechanisms ahead of time.

Published
2017
Full Text
View/download PDF

9. Runtime Enforcement of Regular Timed Properties by Suppressing and Delaying Events

Author

Thierry Jéron, Yliès Falcone, Hervé Marchand, Srinivas Pinisetty, Compiler Optimization and Run-time Systems (CORSE), Inria Grenoble - Rhône-Alpes, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire d'Informatique de Grenoble (LIG ), Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Centre National de la Recherche Scientifique (CNRS)-Université Grenoble Alpes [2016-2019] (UGA [2016-2019])-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Centre National de la Recherche Scientifique (CNRS)-Université Grenoble Alpes [2016-2019] (UGA [2016-2019]), SUpervision of large MOdular and distributed systems (SUMO), LANGAGE ET GÉNIE LOGICIEL (IRISA-D4), Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA), CentraleSupélec-Télécom Bretagne-Université de Rennes 1 (UR1), Université de Rennes (UNIV-RENNES)-Université de Rennes (UNIV-RENNES)-Institut National de Recherche en Informatique et en Automatique (Inria)-École normale supérieure - Rennes (ENS Rennes)-Université de Bretagne Sud (UBS)-Centre National de la Recherche Scientifique (CNRS)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-CentraleSupélec-Télécom Bretagne-Université de Rennes 1 (UR1), Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA), Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-Inria Rennes – Bretagne Atlantique, Institut National de Recherche en Informatique et en Automatique (Inria), Aalto University, Inria Rennes – Bretagne Atlantique, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-LANGAGE ET GÉNIE LOGICIEL (IRISA-D4), Université de Rennes (UR)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Institut National de Recherche en Informatique et en Automatique (Inria)-Télécom Bretagne-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-Université de Rennes (UR)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Institut National de Recherche en Informatique et en Automatique (Inria)-Télécom Bretagne-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA), and Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Télécom Bretagne-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)

Subjects
ta113, Computer science, 020207 software engineering, 02 engineering and technology, [INFO.INFO-SE]Computer Science [cs]/Software Engineering [cs.SE], 16. Peace & justice, Computer security, computer.software_genre, Automaton, monitoring, runtime enforcement, 0202 electrical engineering, electronic engineering, information engineering, timed specifications, 020201 artificial intelligence & image processing, [INFO.INFO-ES]Computer Science [cs]/Embedded Systems, Enforcement, verification, computer, Software
Abstract

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.

Published
2016
Full Text
View/download PDF

10. Runtime Enforcement of Security Policies on Black Box Reactive Programs

Author

PiessensFrank, MilushevDimiter, MassacciFabio, NgoMinh, Rajamani, Sriram K, Walker, David, and Computer Systems

Subjects
Black box (phreaking), Class (computer programming), SDG 16 - Peace, Computer science, Event (computing), Distributed computing, SDG 16 - Peace, Justice and Strong Institutions, computer.software_genre, Security policy, Computer security, Computer Graphics and Computer-Aided Design, Justice and Strong Institutions, Black Box Mechanism, Reactive Program, Automaton, Virtual machine, Runtime Enforcement, Enforcement, Hypersafety Policy, Machine code, computer, Software
Abstract

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

Published
2015
Full Text
View/download PDF

11. Runtime Enforcement Monitors: composition, synthesis, and enforcement abilities

Author

Laurent Mounier, Jean-Luc Richier, Yliès Falcone, Jean-Claude Fernandez, Verification models and techniques applied to testing and control of reactive systems (VERTECS), Inria Rennes – Bretagne Atlantique, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), VERIMAG (VERIMAG - IMAG), Centre National de la Recherche Scientifique (CNRS)-Institut National Polytechnique de Grenoble (INPG)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Université Joseph Fourier - Grenoble 1 (UJF), Validation de Systèmes, Composants et Objets logiciels (VASCO), Laboratoire d'Informatique de Grenoble (LIG), Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Institut National Polytechnique de Grenoble (INPG)-Centre National de la Recherche Scientifique (CNRS)-Université Pierre Mendès France - Grenoble 2 (UPMF)-Université Joseph Fourier - Grenoble 1 (UJF)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Institut National Polytechnique de Grenoble (INPG)-Centre National de la Recherche Scientifique (CNRS)-Université Pierre Mendès France - Grenoble 2 (UPMF)-Université Joseph Fourier - Grenoble 1 (UJF), Université Joseph Fourier - Grenoble 1 (UJF)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Institut National Polytechnique de Grenoble (INPG)-Centre National de la Recherche Scientifique (CNRS), and Université Pierre Mendès France - Grenoble 2 (UPMF)-Université Joseph Fourier - Grenoble 1 (UJF)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Institut National Polytechnique de Grenoble (INPG)-Centre National de la Recherche Scientifique (CNRS)-Université Pierre Mendès France - Grenoble 2 (UPMF)-Université Joseph Fourier - Grenoble 1 (UJF)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Institut National Polytechnique de Grenoble (INPG)-Centre National de la Recherche Scientifique (CNRS)

Subjects
Safety-progress classification, Monitor synthesis, Computer science, Property (programming), Control (management), 020207 software engineering, 02 engineering and technology, 16. Peace & justice, Computer security, computer.software_genre, Monito, Theoretical Computer Science, Automaton, Set (abstract data type), Hardware and Architecture, 0202 electrical engineering, electronic engineering, information engineering, 020201 artificial intelligence & image processing, [INFO.INFO-ES]Computer Science [cs]/Embedded Systems, Enforcement, Composition (language), computer, Software, Runtime enforcement, Composition
Abstract

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.

Published
2011
Full Text
View/download PDF

Catalog

Books, media, physical & digital resources
See catalog results