A type-checking approach to ensure monitor correctness

Abstract

Monitors are software entities that are instrumented onto a system to observe its behaviour and (possibly) react in response to the observed behaviour. Monitor actions that are triggered in response to the detected behaviour range from basic notifications to adaptive actions that can a ect the structure and future behaviour of the system being monitored. Since monitors are considered to form part of the trusted computing base, ensuring that a monitor does not perform unsafe operations on the system is imperative to preserve the system’s integrity. Nevertheless, monitors rarely come equipped with any correctness guarantees. The behavioural specifications from which monitors are generated, are typically expressed through full-blown programming languages, domain specific languages or logic scripts. Hence, language-based approaches are well-suited to ensure correct monitor behaviour. Typechecking is one such widely-accepted languagebased approach, that is used to verify the absence of certain errors, by approximating the runtime behaviour of a program from its textual description. In this dissertation we investigate the application of typechecking as means of ensuring monitor correctness. More specifically, we extend the preliminary work presented in [1], where the authors develop a runtime adaptation framework for Erlang actor systems. This framework is accompanied by a declarative type system which guarantees that any well-typed monitoring script, will never lead to synchronisation errors at runtime, as a preliminary attempt to ensure correct monitor behaviour. However, despite its merits this type system has a number of shortcomings. The current type system conservatively rejects certain useful and well-behaved adaptation scripts. Furthermore, type safety is guaranteed against synchronisation errors, however, there are other erroneous behaviours which can be detected statically. Finally, the current specification of the type system is not directly amenable to an implementation since it specifies what constitutes a valid adaptation script, rather than how to carry out typechecking. In this dissertation we revisit this declarative type system and address these issues. More specifically, we begin by alter the typing rules of the current declarative type system, in order to extend the set of typeable scripts and accept useful well-behaved adaptation scripts that are rejected by the declarative type system of [1]. Furthermore, we also give stronger guarantees on the set of well-typed adaptation scripts, by showing that any scripts that are accepted by the extended declarative type system, will never lead to a synchronisation or a release error at runtime. Finally, in order to be able to derive a typechecking algorithm, we formulate an algorithmic type system and show that it corresponds to the extended declarative type system, from which we implement a typechecker that can automatically determine whether an adaptation script is well-typed or not.