Automated checks for deterministic monitor behaviour using OCaml

Abstract

Monitors are computing entities that observe the execution of other programs with the aim of inferring properties about these programs. Typically, when sufficient runtime behaviour is observed, monitors produce a verdict, which usually takes the form of a rejection or an acceptance flag. Since monitors are considered to be part of the Trusted Computing Base (TCB), they are expected to behave correctly, and one correctness criteria is that they should exhibit deterministic behaviour. One definition which describes determinism in monitors is the notion of controllability. In his recent work, Francalanza presents two definitions for this notion - an initial plain definition, and a more tractable definition which relies on a symbolic monitor analysis termed Symbolic Controllability. The latter definition targets to solve the weaknesses entailed by the initial definition for Controllability through the use of symbolic events and conditions. Francalanza also claims that the definitions are implementable, and that the definition of Symbolic Controllability is more expressive than its counterpart. This project verifies the implementability claims of these two definitions, especially that of Symbolic Controllability through implementing these mathematically-specified procedures in terms of the functional programming language of OCaml; Functional languages traditionally lend themselves well to direct implementations of formal specifications. Therefore, by producing a constructive algorithm for these declarative definitions presented we were able to produce a tool checking for monitor determinism.