-
Bidirectional Runtime Enforcement of First-Order Branching-Time Properties
Authors:
Luca Aceto,
Ian Cassar,
Adrian Francalanza,
Anna Ingolfsdottir
Abstract:
Runtime enforcement is a dynamic analysis technique that instruments a monitor with a system in order to ensure its correctness as specified by some property. This paper explores bidirectional enforcement strategies for properties describing the input and output behaviour of a system. We develop an operational framework for bidirectional enforcement and use it to study the enforceability of the sa…
▽ More
Runtime enforcement is a dynamic analysis technique that instruments a monitor with a system in order to ensure its correctness as specified by some property. This paper explores bidirectional enforcement strategies for properties describing the input and output behaviour of a system. We develop an operational framework for bidirectional enforcement and use it to study the enforceability of the safety fragment of Hennessy-Milner logic with recursion (sHML). We provide an automated synthesis function that generates correct monitors from sHML formulas, and show that this logic is enforceable via a specific type of bidirectional enforcement monitors called action disabling monitors.
△ Less
Submitted 27 February, 2023; v1 submitted 9 January, 2022;
originally announced January 2022.
-
On Runtime Enforcement via Suppressions
Authors:
Luca Aceto,
Ian Cassar,
Adrian Francalanza,
Anna Ingolfsdottir
Abstract:
Runtime enforcement is a dynamic analysis technique that uses monitors to enforce the behaviour specified by some correctness property on an executing system. The enforceability of a logic captures the extent to which the properties expressible via the logic can be enforced at runtime. We study the enforceability of Hennessy-Milner Logic with Recursion (muHML) with respect to suppression enforceme…
▽ More
Runtime enforcement is a dynamic analysis technique that uses monitors to enforce the behaviour specified by some correctness property on an executing system. The enforceability of a logic captures the extent to which the properties expressible via the logic can be enforced at runtime. We study the enforceability of Hennessy-Milner Logic with Recursion (muHML) with respect to suppression enforcement. We develop an operational framework for enforcement which we then use to formalise when a monitor enforces a muHML property. We also show that the safety syntactic fragment of the logic, sHML, is enforceable by providing an automated synthesis function that generates correct suppression monitors from sHML formulas.
△ Less
Submitted 3 July, 2018;
originally announced July 2018.
-
Developing Theoretical Foundations for Runtime Enforcement
Authors:
Ian Cassar,
Adrian Francalanza,
Luca Aceto,
Anna Ingolfsdottir
Abstract:
The ubiquitous reliance on software systems increases the need for ensuring that systems behave correctly and are well protected against security risks. Runtime enforcement is a dynamic analysis technique that utilizes software monitors to check the runtime behaviour of a software system with respect to a correctness specification. Whenever the runtime behaviour of the monitored system is about to…
▽ More
The ubiquitous reliance on software systems increases the need for ensuring that systems behave correctly and are well protected against security risks. Runtime enforcement is a dynamic analysis technique that utilizes software monitors to check the runtime behaviour of a software system with respect to a correctness specification. Whenever the runtime behaviour of the monitored system is about to deviate from the specification (either due to a programming bug or a security hijack attack), the monitors apply enforcement techniques to prevent this deviation.
Current Runtime Enforcement techniques require that the correctness specification defines the behaviour of the enforcement monitor itself. This burdens the specifier with not only having to define property that needs to be enforced, but also with having to specify how this should be enforced at runtime; we thus relieve the specifier from this burden by resorting to a highly expressive logic. Using a logic we allow the specifier to define the correctness specification as a logic formula from which we can automatically synthesise the appropriate enforcement monitor.
Highly expressive logics can, however, permit for defining a wide variety of formulae, some of which cannot actually be enforced correctly at runtime. We thus study the enforceability of Hennessy Milner Logic with Recursion for which we identify a subset that allows for defining enforceable formulae. This allows us to define a synthesis function that translates enforceable formulae into enforcement monitors. As our monitors are meant to ensure the correct behaviour of the monitored system, it is imperative that they work correctly themselves. We thus study formal definitions that allow us to ensure that our enforcement monitors behave correctly.
△ Less
Submitted 12 November, 2018; v1 submitted 24 April, 2018;
originally announced April 2018.
-
Towards Runtime Adaptation of Actor Systems
Authors:
Ian Cassar
Abstract:
In this dissertation we focus on providing effective adaptations that can be localised and applied to specific concurrent actors, thereby only causing a temporary disruption to the parts of the system requiring mitigation, while leaving the rest of the system intact. We make the application of localised adaptations efficient through incremental synchronisation, whereby the specifier can strategica…
▽ More
In this dissertation we focus on providing effective adaptations that can be localised and applied to specific concurrent actors, thereby only causing a temporary disruption to the parts of the system requiring mitigation, while leaving the rest of the system intact. We make the application of localised adaptations efficient through incremental synchronisation, whereby the specifier can strategically suspend specific parts of the system, whenever this is strictly required for ensuring that adaptations are effectively applied. We also study static analysis techniques to determine whether the specified incremental synchronisation is in some sense adequate for local adaptations to be carried out.
We thus identify a number of generic adaptations that can be applied to any actor system, regardless of its design and the code that it executes. We implement the identified adaptations as an extension of an existing Runtime Verification tool for actor-systems, thereby creating a RA framework for monitoring and mitigating actor systems. In parallel to our implementation we also develop a formal model of our RA framework that further serves to guide our implementation. This model also enables us to better understand the subtle errors that erroneously specified adaptation scripts may introduce. We thus develop a static type system for detecting and rejecting erroneous adaptation scripts prior to deployment, thereby providing the specifier with assistance for writing valid scripts. Although the static typesystem analyses scripts with respect to certain assumptions, we do not assume that the monitored system abides by these assumptions. We therefore augment our RA framework with dynamic checks for halting monitoring whenever the system deviates from our assumption. Based on this dynamically checked model of our RA framework, we prove type soundness for our static type system.
△ Less
Submitted 31 August, 2017;
originally announced September 2017.
-
Reliability and Fault-Tolerance by Choreographic Design
Authors:
Ian Cassar,
Adrian Francalanza,
Claudio Antares Mezzina,
Emilio Tuosto
Abstract:
Distributed programs are hard to get right because they are required to be open, scalable, long-running, and tolerant to faults. In particular, the recent approaches to distributed software based on (micro-)services where different services are developed independently by disparate teams exacerbate the problem. In fact, services are meant to be composed together and run in open context where unpred…
▽ More
Distributed programs are hard to get right because they are required to be open, scalable, long-running, and tolerant to faults. In particular, the recent approaches to distributed software based on (micro-)services where different services are developed independently by disparate teams exacerbate the problem. In fact, services are meant to be composed together and run in open context where unpredictable behaviours can emerge. This makes it necessary to adopt suitable strategies for monitoring the execution and incorporate recovery and adaptation mechanisms so to make distributed programs more flexible and robust. The typical approach that is currently adopted is to embed such mechanisms in the program logic, which makes it hard to extract, compare and debug. We propose an approach that employs formal abstractions for specifying failure recovery and adaptation strategies. Although implementation agnostic, these abstractions would be amenable to algorithmic synthesis of code, monitoring and tests. We consider message-passing programs (a la Erlang, Go, or MPI) that are gaining momentum both in academia and industry. Our research agenda consists of (1) the definition of formal behavioural models encompassing failures, (2) the specification of the relevant properties of adaptation and recovery strategy, (3) the automatic generation of monitoring, recovery, and adaptation logic in target languages of interest.
△ Less
Submitted 23 August, 2017;
originally announced August 2017.
-
A Survey of Runtime Monitoring Instrumentation Techniques
Authors:
Ian Cassar,
Adrian Francalanza,
Luca Aceto,
Anna Ingólfsdóttir
Abstract:
Runtime Monitoring is a lightweight and dynamic verification technique that involves observing the internal operations of a software system and/or its interactions with other external entities, with the aim of determining whether the system satisfies or violates a correctness specification. Compilation techniques employed in Runtime Monitoring tools allow monitors to be automatically derived from…
▽ More
Runtime Monitoring is a lightweight and dynamic verification technique that involves observing the internal operations of a software system and/or its interactions with other external entities, with the aim of determining whether the system satisfies or violates a correctness specification. Compilation techniques employed in Runtime Monitoring tools allow monitors to be automatically derived from high-level correctness specifications (aka. properties). This allows the same property to be converted into different types of monitors, which may apply different instrumentation techniques for checking whether the property was satisfied or not. In this paper we compare and contrast the various types of monitoring methodologies found in the current literature, and classify them into a spectrum of monitoring instrumentation techniques, ranging from completely asynchronous monitoring on the one end and completely synchronous monitoring on the other.
△ Less
Submitted 23 August, 2017;
originally announced August 2017.
-
Improving Runtime Overheads for detectEr
Authors:
Ian Cassar,
Adrian Francalanza,
Simon Said
Abstract:
We design monitor optimisations for detectEr, a runtime-verification tool synthesising systems of concurrent monitors from correctness properties for Erlang programs. We implement these optimisations as part of the existing tool and show that they yield considerably lower runtime overheads when compared to the unoptimised monitor synthesis.
We design monitor optimisations for detectEr, a runtime-verification tool synthesising systems of concurrent monitors from correctness properties for Erlang programs. We implement these optimisations as part of the existing tool and show that they yield considerably lower runtime overheads when compared to the unoptimised monitor synthesis.
△ Less
Submitted 16 March, 2015;
originally announced March 2015.
-
On Synchronous and Asynchronous Monitor Instrumentation for Actor-based systems
Authors:
Ian Cassar,
Adrian Francalanza
Abstract:
We study the impact of synchronous and asynchronous monitoring instrumentation on runtime overheads in the context of a runtime verification framework for actor-based systems. We show that, in such a context, asynchronous monitoring incurs substantially lower overhead costs. We also show how, for certain properties that require synchronous monitoring, a hybrid approach can be used that ensures tim…
▽ More
We study the impact of synchronous and asynchronous monitoring instrumentation on runtime overheads in the context of a runtime verification framework for actor-based systems. We show that, in such a context, asynchronous monitoring incurs substantially lower overhead costs. We also show how, for certain properties that require synchronous monitoring, a hybrid approach can be used that ensures timely violation detections for the important events while, at the same time, incurring lower overhead costs that are closer to those of an asynchronous instrumentation.
△ Less
Submitted 11 February, 2015;
originally announced February 2015.
