Search

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

1. A process calculus approach to detection and mitigation of PLC malware

Author

Massimo Merro, Andrei Munteanu, and Ruggero Lanotte

Subjects
Programmable logic controller, Correctness, PLC correctness, Mitigation, General Computer Science, SIMPLE (military communications protocol), business.industry, Computer science, Process calculus, Process (computing), Deadlock, computer.software_genre, Theoretical Computer Science, Embedded system, Malware detection, Malware, Runtime enforcement, Actuator, business, computer
Abstract

We define a simple process calculus, based on Hennessy and Regan's Timed Process Language, for specifying networks of communicating programmable logic controllers (PLCs) enriched with monitors enforcing specification compliance at runtime. We define a synthesis algorithm that given an uncorrupted PLC returns a monitor that enforces the correctness of the PLC, even when injected with malware that may forge/drop actuator commands and inter-controller communications. Then, we strengthen the capabilities of our monitors by allowing the insertion of actions to mitigate malware activities. This gives us deadlock-freedom monitoring: malware may not drag monitored controllers into deadlock states. Our enforcing monitors represent a formal mechanism for prompt detection of malicious activities within PLCs. Finally, we illustrate our results by implementing in Simulink a non-trivial Water Transmission Network (WTN) system, and testing the effectiveness of our monitors in detecting and mitigating three different attacks targeting the PLCs of our WTN.

Published
2021
Full Text
View/download PDF

2. Testing Real-Time Systems With Runtime Enforcement

Author

Sébastien Faucou, Louis-Marie Givel, Matthias Brun, Jean-Luc Béchennec, Olivier Roux, Laboratoire des Sciences du Numérique de Nantes (LS2N), Université de Nantes - UFR des Sciences et des Techniques (UN UFR ST), Université de Nantes (UN)-Université de Nantes (UN)-École Centrale de Nantes (ECN)-Centre National de la Recherche Scientifique (CNRS)-IMT Atlantique Bretagne-Pays de la Loire (IMT Atlantique), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT), Centre National de la Recherche Scientifique (CNRS), ESEO-TRAME (TRAME), ESEO-Tech, Université Bretagne Loire (UBL)-Université Bretagne Loire (UBL), Université de Nantes (UN), and École Centrale de Nantes (ECN)

Subjects
formal methods, Computer science, 02 engineering and technology, computer.software_genre, parametric timed model, RTOS, 0202 electrical engineering, electronic engineering, information engineering, Electrical and Electronic Engineering, Enforcement, Real-time operating system, Real-time testing, Model-based testing, real-time testing, ACM: D.: Software/D.2: SOFTWARE ENGINEERING/D.2.5: Testing and Debugging, Formal methods, ACM: D.: Software/D.4: OPERATING SYSTEMS/D.4.5: Reliability, ACM: D.: Software/D.4: OPERATING SYSTEMS/D.4.7: Organization and Design/D.4.7.4: Real-time systems and embedded systems, 020202 computer hardware & architecture, model-based testing, runtime enforcement, real-time systems, Hardware and Architecture, Kernel (statistics), Operating system, [INFO.INFO-ES]Computer Science [cs]/Embedded Systems, 020201 artificial intelligence & image processing, Scenario testing, computer, Software
Abstract

International audience; —When testing a time-critical system, some scenarios can be hard to run when acting only on the input sequence. The proper execution of a given scenario might require for instance a minimal execution time for a given piece of software. Execution times are notoriously difficult to control because they depend not only on the inputs, but also on the state of the micro-architecture. In this paper, we propose a method, based on runtime enforcement, which forces a system to run such a scenario. We also describe an implementation in the context of a RTOS for embedded control systems. Our method starts with a parametric formal model of the system where the parameters are delays that can be added to simulate longer execution times. The domain of acceptable parameter values to run the target scenario is computed offline. Online, a framework plugged in the RTOS observes the execution of the system and injects delays when needed.

Published
2018
Full Text
View/download PDF

3. 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

4. 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

5. 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

6. 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

7. 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

8. 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

9. 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

10. 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

11. What can you verify and Enforce at Runtime?

Author

Jean-Claude Fernandez, Yliès Falcone, Laurent Mounier, 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), and 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
Computer science, Property (programming), Distributed computing, Context (language use), 0102 computer and information sciences, 02 engineering and technology, computer.software_genre, 01 natural sciences, Set (abstract data type), 0202 electrical engineering, electronic engineering, information engineering, Enforcement, Representation (mathematics), property, Database, Runtime verification, 020207 software engineering, 16. Peace & justice, expressiveness, runtime enforcement, 010201 computation theory & mathematics, Theory of computation, runtime verification, [INFO.INFO-ES]Computer Science [cs]/Embedded Systems, computer, Software, Information Systems
Abstract

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.

Published
2011

Catalog

Books, media, physical & digital resources
See catalog results