arXiv subjects

Adrian Francalanza

Publications and source records attributed to Adrian Francalanza.

At least 37 records · Page 2Linked to original sources

arXiv2020

Behavioural Types for Memory and Method Safety in a Core Object-Oriented Language

We present a type-based analysis ensuring memory safety and object protocol completion in the Java-like language Mungo. Objects are annotated with usages, typestates-like specifications of the admissible sequences of method calls. The analysis entwines usage checking, controlling the order in which methods are called, with a static check determining whether references may contain null values. The analysis prevents null pointer dereferencing and memory leaks and ensures that the intended usage protocol of every object is respected and completed. The type system has been implemented in the form of a type checker.

cs.PL↗

arXiv2019

An Operational Guide to Monitorability

Monitorability delineates what properties can be verified at runtime. Although many monitorability definitions exist, few are defined explicitly in terms of the guarantees provided by monitors, i.e., the computational entities carrying out the verification. We view monitorability as a spectrum: the fewer monitor guarantees that are required, the more properties become monitorable. We present a monitorability hierarchy and provide operational and syntactic characterisations for its levels. Existing monitorability definitions are mapped into our hierarchy, providing a unified framework that makes the operational assumptions and guarantees of each definition explicit. This provides a rigorous foundation that can inform design choices and correctness claims for runtime verification tools.

cs.LO↗

arXiv2019

Heaps Don't Lie: Countering Unsoundness with Heap Snapshots

Static analyses aspire to explore all possible executions in order to achieve soundness. Yet, in practice, they fail to capture common dynamic behavior. Enhancing static analyses with dynamic information is a common pattern, with tools such as Tamiflex. Past approaches, however, miss significant portions of dynamic behavior, due to native code, unsupported features (e.g., invokedynamic or lambdas in Java), and more. We present techniques that substantially counteract the unsoundness of a static analysis, with virtually no intrusion to the analysis logic. Our approach is reified in the HeapDL toolchain and consists in taking whole-heap snapshots during program execution, that are further enriched to capture significant aspects of dynamic behavior, regardless of the causes of such behavior. The snapshots are then used as extra inputs to the static analysis. The approach exhibits both portability and significantly increased coverage. Heap information under one set of dynamic inputs allows a static analysis to cover many more behaviors under other inputs. A HeapDL-enhanced static analysis of the DaCapo benchmarks computes 99.5% (median) of the call-graph edges of unseen dynamic executions (vs. 76.9% for the Tamiflex tool).

cs.PL↗

arXiv2019

The Cost of Monitoring Alone

We compare the succinctness of two monitoring systems for properties of infinite traces, namely parallel and regular monitors. Although a parallel monitor can be turned into an equivalent regular monitor, the cost of this transformation is a double-exponential blowup in the syntactic size of the monitors, and a triple-exponential blowup when the goal is a deterministic monitor. We show that these bounds are tight and that they also hold for translations between corresponding fragments of Hennessy-Milner logic with recursion over infinite traces.

cs.LO↗

arXiv2019

Adventures in Monitorability: From Branching to Linear Time and Back Again

This paper establishes a comprehensive theory of runtime monitorability for Hennessy-Milner logic with recursion, a very expressive variant of the modal $μ$-calculus. It investigates the monitorability of that logic with a linear-time semantics and then compares the obtained results with ones that were previously presented in the literature for a branching-time setting. Our work establishes an expressiveness hierarchy of monitorable fragments of Hennessy-Milner logic with recursion in a linear-time setting and exactly identifies what kinds of guarantees can be given using runtime monitors for each fragment in the hierarchy. Each fragment is shown to be complete, in the sense that it can express all properties that can be monitored under the corresponding guarantees. The study is carried out using a principled approach to monitoring that connects the semantics of the logic and the operational semantics of monitors. The proposed framework supports the automatic, compositional synthesis of correct monitors from monitorable properties.

cs.LO↗

arXiv2018

A Survey of Challenges for Runtime Verification from Advanced Application Domains (Beyond Software)

Runtime verification is an area of formal methods that studies the dynamic analysis of execution traces against formal specifications. Typically, the two main activities in runtime verification efforts are the process of creating monitors from specifications, and the algorithms for the evaluation of traces against the generated monitors. Other activities involve the instrumentation of the system to generate the trace and the communication between the system under analysis and the monitor. Most of the applications in runtime verification have been focused on the dynamic analysis of software, even though there are many more potential applications to other computational devices and target systems. In this paper we present a collection of challenges for runtime verification extracted from concrete application domains, focusing on the difficulties that must be overcome to tackle these specific challenges. The computational models that characterize these domains require to devise new techniques beyond the current state of the art in runtime verification.

cs.SE↗

arXiv2018

Developing Theoretical Foundations for Runtime Enforcement

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.

cs.LO↗

arXiv2018

On Runtime Enforcement via Suppressions

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.

cs.LO↗

arXiv2017

A Survey of Runtime Monitoring Instrumentation Techniques

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.

cs.LO↗

arXiv2017

Reliability and Fault-Tolerance by Choreographic Design

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.

cs.PL↗

arXiv2017

Proceedings Second International Workshop on Pre- and Post-Deployment Verification Techniques

This volume contains the proceedings of PrePost 2017 (the Second International Workshop on Pre- and Post-Deployment Verification Techniques), taking place on 19th September 2017 in Torino, Italy, as a satellite event of the 13th International Conference on integrated Formal Methods (iFM 2017). PrePost aims to bridge two areas of research and academic communities: on one hand techniques for analysis of systems prior to deployment, on the other techniques for the analysis of systems once they have already been deployed. The workshop brings together researchers working in the field of computer-aided validation, programming languages and verification to discuss the connections and interplay between pre- and post-deployment verification techniques. This includes exploring relationships between techniques such as classic model checking and testing, with ones such as runtime verification and statistical model checking, between type systems that may be checked either statically or dynamically through techniques such as runtime monitoring, gradual typing and contracts.

cs.LO↗

arXiv2016

Determinizing Monitors for HML with Recursion

We examine the determinization of monitors for HML with recursion. We demonstrate that every monitor is equivalent to a deterministic one, which is at most doubly exponential in size with respect to the original monitor. When monitors are described as CCS-like processes, this doubly exponential bound is optimal. When (deterministic) monitors are described as finite automata (as their LTS), then they can be exponentially more succinct than their CCS process form.

cs.LO↗

arXiv2016

Preliminary Results Towards Contract Monitorability

This paper discusses preliminary investigations on the monitorability of contracts for web service descriptions. There are settings where servers do not guarantee statically whether they satisfy some specified contract, which forces the client (i.e., the entity interacting with the server) to perform dynamic checks. This scenario may be viewed as an instance of Runtime Verification, where a pertinent question is whether contracts can be monitored for adequately at runtime, otherwise stated as the monitorability of contracts. We consider a simple language of finitary contracts describing both clients and servers, and develop a formal framework that describes server contract monitoring. We define monitor properties that potentially contribute towards a comprehensive notion of contract monitorability and show that our simple contract language satisfies these properties.

cs.LO↗

arXiv2016

Proceedings First Workshop on Pre- and Post-Deployment Verification Techniques

The PrePost (Pre- and Post-Deployment Verification Techniques) workshop aimed at bringing together researchers working in the field of computer-aided validation and verification to discuss the connections and interplay between pre- and post-deployment verification techniques. Examples of the topics covered by the workshop are the relationships between classic model checking and testing on the one hand and runtime verification and statistical model checking on the other, and between type systems that may be checked either statically or dynamically through techniques such as runtime monitoring.

cs.LO↗

arXiv2015

Unlocking Blocked Communicating Processes

We study the problem of disentangling locked processes via code refactoring. We identify and characterise a class of processes that is not lock-free; then we formalise an algorithm that statically detects potential locks and propose refactoring procedures that disentangle detected locks. Our development is cast within a simple setting of a finite linear CCS variant â although it suffices to illustrate the main concepts, we also discuss how our work extends to other language extensions.

cs.PL↗

arXiv2015

Improving Runtime Overheads for detectEr

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.

cs.SE↗

arXiv2015

On Synchronous and Asynchronous Monitor Instrumentation for Actor-based systems

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.

cs.LO↗

arXiv2014

Compositional Reasoning for Explicit Resource Management in Channel-Based Concurrency

We define a pi-calculus variant with a costed semantics where channels are treated as resources that must explicitly be allocated before they are used and can be deallocated when no longer required. We use a substructural type system tracking permission transfer to construct coinductive proof techniques for comparing behaviour and resource usage efficiency of concurrent processes. We establish full abstraction results between our coinductive definitions and a contextual behavioural preorder describing a notion of process efficiency w.r.t. its management of resources. We also justify these definitions and respective proof techniques through numerous examples and a case study comparing two concurrent implementations of an extensible buffer.

cs.LO↗