Runtime Verification¶

A partial view of the program model¶

Let us recall the calculator server and its transition model.

From its initial state Q0, the transition system modelling the behaviour of calc_server:loop/1 can follow three different paths. This branching structure is induced by the receive expression, that introduces a choice between which clause to execute, depending on the pattern match that succeeds. The transition model thus gives us an exhaustive description of the paths that the calculator server can take at runtime, affording us full visibility about what the program is able to do. Notably, this information is available prior to runtime, and is what certain static verification techniques such as model checking rely upon.

There are however cases where static approaches cannot be employed, e.g. the program transition model is not available, or is infeasible to construct. Runtime Verification is a post-deployment technique that can be used instead of, or in tandem with, static techniques to increase correctness assurances about a program under scrutiny. RV uses monitors—computational entities consisting of logically-distinct instrumentation and analyser units—to observe the execution of the program under scrutiny. detectEr is one such RV tool for asynchronous component systems that can analyse the behaviour of programs running on, or outside the EVM.

Post-deployment verification techniques such as RV often to not have access to the entire transition model of a program. Rather, their view of the system is limited to just to the sequence of events generated by the current program execution. This linear sequence of program event is known as the (execution) trace. For instance, our calculator program might generate the trace of events ‘<0.10.0> ? {<0.16.0>, stp}.<0.10.0>:<0.16.0> ! {bye, 1}’. This corresponds to the (finite) path traversal Q0 → Srv ? {Clt, stp} → Q3 → Srv:Clt ! {bye, Tot} in the transition model above, where Srv = <0.10.0>, Clt = <0.16.0>, and Tot = 1.

Is one execution trace enough?¶

One natural question that may occur to you at this point is whether a mere sliver of the (more expressive) program transition model is sufficient for us to conclude anything of value about the program under analysis. Answers to this question depend on various aspects:

What logic are we using to express properties? There are logics that can reason about states of the program transition model (e.g. μ-calculus, HML, CTL), while others can only reason on traces (e.g., LTL).
Are the traces we consider finite or infinite? By and large, a number of logics used for model checking reason about infinite traces. RV typically produces finite traces, and this means that such logics need to be semantically adapted to the runtime setting, or studied to determine which subsets of them are amenable to runtime monitoring.
How many traces do we have available? There are cases where more than one trace is available, e.g. the program is executed multiple times, or the program consists of concurrent components that produce different interleaved executions. This produces additional runtime information that one may leverage.

This field of study is called monitorability, and has been treated at length in various works¹. For us, it is enough to know that sHML—the logic detectEr uses—is runtime monitorable with respect to violations².

Violation

Any program that violates a property expressed as a sHML formula can be detected by finding an execution trace that contains the violating program behaviour.

The intuition as to why this is the case is as follows. Recall that the sHML formula [α]φ requires that all the outgoing paths from some state of the program transition model satisfy the symbolic action α, and the next state then satisfies the continuation φ. To show that a program transition model (not just one path!) violates the sHML property, it suffices to find one path in the transition model that goes against the what property stipulates.

Now, in our runtime setting, the program under scrutiny is sure to follow at least one such path in the model, which is precisely the one it takes as it executes. This path, observable as an execution trace, is processed by runtime analysers to yield monitoring verdicts. In our case of safety properties, the verdict an analyser gives is either no or end:

no corresponds to a property violation, ff,
end means that the analyser does not have sufficient information in the trace to be able to conclude whether the program violates the property. This is the case, since there might be other traces (i.e., other paths in the program transition model) that can contain the violating behaviour. We refer to this type of verdict as an inconclusive verdict.

The verdicts that runtime analysers flag are irrevocable. These are verdicts that once given, cannot be retracted and changed. For our purposes, this makes sense. Why? Because in the case of safety properties, an analyser that changes its verdict, sometimes flagging no and at other times, end, would be useless. We want that if the program violates a property, then it stays that way, and the analyser persists its given verdict.

Note

Often it is assumed that the program and model correspond, i.e., the program model captures the behaviour of the program implementation. In the sequel, whenever we say that the program (or program implementation) violates a stipulated property, it also means that the model violates that property.

We next learn how runtime analysers from sHML specifications can be synthesised.

Citations needed ↩
Citations needed ↩