11institutetext: IMDEA Software Institute, Spain 22institutetext: Universidad
Politécnica de Madrid (UPM), Spain 33institutetext: CIFASIS, Argentina

# Retroactive Parametrized Monitoring

Paloma Pedregal(🖂) 1122 Felipe Gorostiaga(🖂) 1133 César Sánchez 11

###### Abstract

In online monitoring, we first synthesize a monitor from a formal
specification, which later runs in tandem with the system under study,
incrementally receiving its progress and evolving with the system. In offline
monitoring the trace is logged as the system progresses to later do post-
mortem analysis after the system has finished executing.

In this paper we propose _retroactive dynamic parametrization_ , a technique
that allows a monitor to revisit the past log as it progresses, while still
executing in an online manner. This feature allows new monitors to be
incorporated into a running system and to revisit the past for particular
behaviors based on new information discovered. Retroactive parametrization
also allows a monitor to lazily ignore events and revisit and process them
later, when it discovers that it should have followed those events. We
showcase the use of retroactive dynamic parametrization to monitor denial of
service attacks on a network using network logs.

##  1 Introduction

Runtime verification (RV) is a lightweight formal dynamic verification
technique that analyzes a single trace of execution using a monitor derived
from a specification (see [19, 2]). The initial specification languages to
describe monitors in RV where borrowed from property languages for static
verification, including linear temporal logic (LTL) [23], adapted to finite
traces [3, 20] or extensions [8]. Most RV languages describe a monolithic
monitor that later processes the events received. Dynamic parametrization
(also known as parametric trace slicing) allows quantifying over objects and
spawn monitors that follow independently the actual objects observed, like in
Quantified Event Automata (QEA) [1].

Stream runtime verification [12, 22, 4](SRV), pioneered by Lola [7] defines
monitors by declaring the dependencies between output streams and input
streams. The initial application domain of Lola was the testing of synchronous
hardware. Temporal testers [24] were later proposed as a monitoring technique
for LTL based on Boolean streams. Copilot [22, 12, 21] is a DSL that, similar
to Lola, declares dependencies between streams in a Haskell-based style, to
generate C monitors. Lola2.0 [9] extends Lola allowing dynamically
parametrized streams, similarly to QEA. Stream runtime verification has also
been extended recently to asynchronous and real-time systems [11, 6, 18, 13].
HLola[5, 14, 16] is an implementation of Lola as an embedded DSL in Haskell,
which allows borrowing datatypes from Haskell directly as Lola expressions,
and using features like higher-order functions to ease the development of
specifications and the runtime system. In this paper we use HLola and extend
it with capabilities for retroactive dynamic parametrization.

In some situations we want to monitor a property that we define once the
system is already running, and we cannot or do not wish to stop and restart
the monitor. Therefore, the monitor will receive online the events of a suffix
of the original trace. At this point, we must decide to either (1) _ignore_
that the monitor is plugged in the middle of the trace and let it work under
the premise that it is watching the whole history, (2) _encode the lack of
knowledge_ about the beginning of the trace in the specification, or, (3) if
the beginning of the trace was preserved in a _log_ or a database and it is
accessible, allow the monitor to collaborate with the log to process the
missing past and then continue to process the future events online. The first
option is the most natural and in many cases a good solution, while the second
option has been explored in [17], but these two options ignore the beginning
of the trace and thus we have to pick one of them if the trace is not
preserved. The third option proposes a novel combination of _offline+online
monitoring_ , which offers the possibility of accessing the past of the trace.
Moreover, enriching an SRV monitor with the ability of accessing the past
allows the description of properties that revisit the past exploiting
information discovered at a later time.

In this paper we show an instance of this combination of online and offline
monitoring to implement a novel dynamic instantiation of monitors called
_retroactive dynamic parametrization_ that combines dynamic parametrization
with the ability to revisit the past of a live stream of events.

This paper is structured as follows. Section 2 introduces SRV and static
parametrization, Section 3 presents the syntax and semantics of the operators
that enable retroactive dynamic parametrization, Section 4 shows how we have
implemented these features in our tool, Section 5 includes an empirical
evaluation of the tool, and finally Section 6 concludes.

##  2 Preliminaries

Stream Runtime Verification (SRV) generalizes monitoring algorithms to
arbitrary data, where temporal dependencies are maintained but datatypes are
generalized using multi-sorted interpreted signatures, which we call data
theories. The signatures are interpreted in the sense that every functional
symbol f used to construct terms of a given type is accompanied with an
evaluation function $f$ (the interpretation) that allows the computation of
values (given values of the arguments). In this paper we use the extensible
tool HLola, an implementation of Lola [7] developed as an embedded DSL in
Haskell. We show in Section 4 how HLola allows the easy implementation of new
powerful features as libraries with no changes to the core engine, leveraging
the extensibility and expressiveness of the data theories of the tool. In this
paper we show how retroactive parametrization is implemented in HLola.

A Lola specification $\langle I,O,E\rangle$ consists of  (1) a set of typed
input stream variables $I$, which correspond to the inputs observed by the
monitor;  (2) a set of typed output stream variables $O$ which represent the
outputs of the monitor as well as intermediate observations; and  (3) defining
equations, which associate every output $y\in O$ with a stream expression
$E_{y}$ that describes declaratively the intended values of $y$ (in terms of
the values of inputs and output streams).  The set of _stream expressions_ of
a given type is built from constants and function symbols as constructors (as
usual), and also from _offset expressions_ of the form $s$[$k$|$d$] where $s$
is a stream variable, $k$ is an integer number and $d$ is a value of the type
of $s$ (used as default). For example, altitude[-1|0.0] represents the value
of stream altitude in the previous step of time, with 0.0 as the value used at
the initial instant. We can define a stream alt_ok which checks that the
altitude is always below a predefined threshold, for example 100 meters:

---
1 |  input Double altitude
2 |  output Bool alt_ok = altitude[now] < 100

Given values of the input streams, the formal semantics of a Lola
specification is defined denotationally as the unique collection of streams of
values that satisfies all equations. The existence and uniqueness of streams
of outputs are guaranteed when specifications are not cyclic.

Moreover, online efficient monitoring algorithms can be synthesized for
specifications with (bounded) future accesses [7, 25]. Efficiency here means
that resources (time and space) are independent of the length of the trace and
can be calculated statically, and that each individual output can be generated
immediately. HLola can be efficiently monitored in this trace-length
independent sense [5]. As a byproduct of its design, HLola allows _static
parametrization_ in stream definitions, this is, streams that abstract away
some concrete values, which can be instantiated by the compiler. Following the
previous example, we can define a more generic version of the stream alt_ok as
follows:

---
1 |  input Double altitude
2 |  output Bool alt_checker <Double threshold> = altitude[now] < threshold
3 |  output Bool alt_ok = (altchecker 100)[now]

Static parametrization does not allow instantiations of a parametric stream
with a value that is discovered at runtime. In static parametrization
parameters must be known in static time before the monitor starts running. In
the following sections we will detail the reason of this limitation and we
offer alternatives to implement dynamic parametrization, analysing their pros
and cons.

####  2.0.1 Nested Monitors.

The keystone of the design of HLola is to use datatypes and functions from
Haskell as the data theories of Lola. In turn, HLola also allows using Lola
specifications as datatypes, via a function $\mathit{runSpec}$ that executes a
specification over the input trace and produces a value of the result type. As
a consequence, we can use Lola as a data theory within Lola itself, an
approach that we have called _nested monitors_ [15]. Nested monitors allows
writing functions on streams as SRV specifications, creating and executing
these specifications dynamically. Nested specifications are particularly
useful when the caller monitor can invoke a nested monitor passing a sub-trace
of the original trace as input. The HLola operator $s$[:$n$] creates a list
with the next $n$ values of the stream $s$. We often use slices as input
streams for nested specifications, but any list of values of the appropriate
type can be used. The type of the stream $x$ determines the type of the value
returned when the specification is invoked dynamically.

Defining a _nested_ specification involves giving it a name and adding an
extra clause: return $x$ when $y$ where $x$ is a stream of any type and $y$ is
a Boolean stream. The type of the stream $x$ determines the type of the value
returned when the specification is invoked dynamically. Once we have defined a
nested specification, we can execute it using the function runSpec.

###### Example 1

The following specification calculates whether input numeric streams r and s
will cross within the following $50$ instants. We define a topmost
specification as follows, where stream willCross invokes the nested
specification crossspec with the slices containing the next $50$ events of r
and s as input.

---
1 | use innerspec crossspec
2 |  input Double r
3 |  input Double s
4 |  output Bool willCross = runSpec (crossspec r[:50] s[:50])

In our example, the nested specification crossspec is:

---
1 |  innerspec Bool crossspec
2 |  input Double r
3 |  input Double s
4 |  output Bool cross =
5 |  sign (r[now] \- s[now]) /= sign (r[-1|r[now]] \- s[-1|s[now]])
6 | return cross when cross

The output stream cross simply checks that the relative order of the streams r
and s changes. A nested specification with a clause return $x$ when $y$
returns the value of $x$ at the first time $y$ becomes $\mathbf{true}$, or the
last value of $x$ if $y$ never holds. Therefore, if $y$ becomes
$\mathbf{true}$ in the middle of an execution, the monitor does not have to
run until the end to compute a value and can anticipate the result, so nested
specifications can be incrementally computed as new elements of the input
slice are available, and return the outcome as soon as it is definite. ∎

##  3 Combinig Online and Offline Monitoring

We introduce features to combine offline and online runtime verification. We
start with nested monitors that can access past events when new information is
discovered.

###  3.1 Retroactive Nested Monitors

###### Example 2

Consider monitoring network traffic, where the monitor receives the source and
destination of an IP packet, and the packets per second in the last hundred
instants. We want to detect whether an address has received too many packets
in the last hundred instants, specified as follows: if the packet flow is low,
then there is no attack, but when the flow rate is above a predefined
threshold (threshold_pps) we have to inspect the last hundred packets and
check if a given address is under attack. We use the following specification
to check the heuristics and trigger the finer analysis of the tail of the
trace when necessary.

---
1 |  input Int packets_per_second
2 |  output Int counter = counter[-1|0] \+ 1
3 |  output Bool under_attack =
4 |  if packets_per_second[now] > threshold_pps then
5 |  let past = pastRetriever counter[now] in
6 | runSpec (finerSpec ‘withTrace‘ past)
7 |  else False

The auxiliary stream counter indicates pastRetriever which events it has to
recover. We use if $\cdot$ then $\cdot$ else $\cdot$ instead of the Boolean
operator (&&) to stress the fact that the nested specification is only
executed when the threshold is exceeded. Then, we define the nested
specification finerSpec as follows:

---
1 |  innerspec Bool finerSpec
2 |  input String destination
3 |  output (Map String Int) entropy =
4 |  insertWith (+) destination[now] 1 entropy[-1|empty]
5 |  output Bool under_attack = maximum (elems entropy[now]) > threshold_dest
6 | return under_attack when under_attack

The function insertWith cmb k v m inserts the element v associated to the key
k into the map m, combining v with the previous value m[k] using cmb if it
exists. The function elems m returns the list of values in the map m, and the
function maximum ls returns the maximum in the list ls. The nested
specification will return $\mathbf{true}$ as soon as under_attack becomes
$\mathbf{true}$, and $\mathbf{false}$ if such stream is always
$\mathbf{false}$ until the end of the (sub)trace. ∎

Note how this specification detects an attack at most one hundred instants
after it happens. Also, the nested monitors in this example are created,
executed and destroyed at every instant. In Section 4, we explain how we can
implement dynamic parametrization by keeping the nested monitors alive across
the trace.

###  3.2 (Forward) Dynamic Parametrization

We introduce now a novel operator over, which lets us instantiate a parametric
stream over dynamic values. The over operator takes a parametric stream strm
of type S with a parameter of type P, and a stream params of sets of values of
type P, and creates an expression of type Map P S, whose keys at any given
instant are the values in params[now], and where the value associated to each
key is the instantiation of s over the key.

Using the over operator we can dynamically instantiate a parametric stream
over a set of parameters that are discovered while processing the trace of
input.

###### Example 3

The specification below checks that every pair (source, destination) follows
the TCP $3$-way handshake in which (1) the source sends a packet SYN, then (2)
the destination sends SYN/ACK and then (3) the source sends ACK. The following
state machine described in HLola captures this:

---
1 |  input String source
2 |  input String destination
3 |  input PacketType p_type
4 |  data PacketType = SYN | SYNACK | ACK
5 |  .............. deriving (Generic,Read,FromJSON,Eq)
6 |  data State = Uninit | Error | SYNED | SYNACKED
7 |  .............. deriving (Generic,Read,FromJSON,Eq)
8 |  output State state <(String, String) srcdest> = let
9 |  prev_state = (state srcdest)[-1|Uninit]
10 | in
11 |  if srcdest /= (source[now], destination[now]) then prev_state
12 |  else if p_type[now] == SYN....&& prev_state == Uninit.. then SYNED
13 |  else if p_type[now] == SYNACK && prev_state == SYNED....then SYNACKED
14 |  else if p_type[now] == ACK....&& prev_state == SYNACKED then Uninit
15 |  else Error

However, we cannot know statically for which pair of addresses we have to
instantiate this parametrized stream. Therefore, we define a set of parameters
(in this case, a set of pairs of addresses) that we need to follow:

---
16 |  output (Set (String, String)) params =
17 |  insert (source[now], destination[now]) params[-1,empty]

At every instant, we add the current pair (source[now], destination[now]) to
the set of parameters. We are now ready to parametrize the parametric stream
state over the values of params:

---
18 |  output Bool all_ok = let
19 | states = elems (state ‘over‘ params)
20 |  in all (/= Error) states

Note that we simply check that all the values in the map generated by the over
expression are different from Error, this is, that no pair of addresses is in
the Error state. This specification follows each pair of addresses
independently. One thing to note is that we never remove parameters from
params, and as a consequence, the set can grow indefinitely, even though it is
not necessary. In fact, we can remove the previous pair of source and
destination when the previous type of message was ACK. The reason why we keep
the parametric stream alive for one more instant before removing it is to let
all_ok check that the behavior was correct. ∎

Every time a new value is incorporated to the set of parameters, we spawn a
new monitor parametrized with the new value. Then, we preserve the state of
this monitor between instants in an auxiliary stream, executing the nested
monitor alongside the outer monitor until the auxiliary monitor is no longer
needed, that is, until its associated parameter is removed from the set.

The nested monitors just described will process the same events as the root
monitor, but it is often the case that only some of the events are relevant to
a specific parametrized stream. We can use _subtracing_ to only update a
subset of the parametrized streams at every instant.

###  3.3 Subtracing

Parametrized streams are internal monitors that observe the same trace as
their parent. However, it is often the case that parametrized streams only
care about the events that are related to their parameter, as in Example 3,
where the events irrelevant to an instantiation do not change its state.
Subtracing lets the nested stream focus only on its relevant subtrace.
Moreover, subtracing enables the possibility of updating only the nested
monitors that may be affected at the current instant. To implement subtracing
we introduce the operator updating that lets us specify the parameters of the
monitors that have to process the current event.

For example, we can use subtracing in Example 3 redefining the streams state
and all_ok as follows:

---
8 |  output State state <(String, String) srcdest> = let
9 |  prev_state = (state srcdest)[-1|Uninit]
10 |  in.. if p_type[now] == SYN....&& prev_state == Uninit.. then SYNED
11 |  else if p_type[now] == SYNACK && prev_state == SYNED....then SYNACKED
12 |  else if p_type[now] == ACK....&& prev_state == SYNACKED then Uninit
13 |  else Error
18 |  output Bool all_ok = let
19 |  currentpair = singleton (source[now], destination[now])
20 | states = elems (state ‘over‘ params ‘updating‘ currentpair)
21 |  in all (/= Error) states

Using subtracing, we can separate the parent trace from the traces received by
the nested monitors, who will only observe a subtrace of the original trace.
This is depicted in Fig. 1.

Figure 1: Subtracing of a parametrized stream s over parameters p0 and p1. At
every instant of the $\mathit{root}$ monitor we show the sets of dynamic
parameters on top, and the sets of parameters to update below.

In the example above, the monitor follows the dynamically parametrized stream
once the parameter has been discovered. In fact, the monitor may not even have
access to the past of the trace because the online runtime monitoring
infrastructure erases past events once they are processed. The only
alternative is to monitor a parametrized stream after its parameter is
discovered (like in Lola2.0 [10]).

If the infrastructure keeps the past events of the trace, we can combine
_retroactive nested monitors_ with _dynamic parametrization_ when a new
parameter is discovered, effectively implementing _retroactive dynamic
parametrization_.

###  3.4 Retroactive Dynamic Parametrization

Static parametrization in HLola is limited because the monitor cannot know the
state of a parametric stream over an arbitrary parameter in the middle of the
trace unless the parameter is determined statically before the monitor starts
running. One alternative to circumvent this limitation is to statically
instantiate the stream with every potentially interesting parameter. This
strategy is reasonable if the stream can only be parametrized with a domain of
parameters with few elements, like Boolean or a small enumerated type, but it
becomes unfeasible when the space of potential parameters is large.

Instead, we propose an alternative technique: that the monitor revisits the
past of the trace every time it discovers a new parameter to instantiate the
parametric stream and from that point continue to monitor the new stream
online.

To implement this feature we add a special clause withInit to the over
operator that allows specifying an _initializer_ , which indicates how the
nested monitor can update its state up to the current instant. An initializer
will typically call an external program with the corresponding arguments that
indicate an offline infrastructure how to efficiently retrieve the elements of
past of the trace that are relevant to the parameter.

###### Example 4

Suppose we are monitoring file accesses in a file system, and we want to
assess that every time a file is read or written, it must have been created
previously. We could use _forward dynamic parametrization_ as in Example 3 to
follow all open files.

---
1 |  input String file_id
2 |  input OpType operation
3 |  data State =..Created | NE | Error deriving (Generic,Read,FromJSON,Eq)
4 |  data OpType = Create..| RW deriving (Generic,Read,FromJSON,Eq)
5 |  output State state <String fid> = let
6 |  prev_state = (state fid)[-1|NE] in
7 |  if (operation[now] == Create && prev_state == NE)
8 |  || (operation[now] == RW.... && prev_state == Created)
9 |  then Created else Error
10 |  output (Set String) params = insert file_id[now] params[-1,empty]
11 |  output Bool all_ok = let
12 |  fid = singleton file_id[now]
13 | states = elems (state ‘over‘ params ‘updating‘ fid)
14 |  in all (/= Error) states

In this example we define datatypes to capture the state of a file id (Created
or NE, “non existent”) and also the type of operations (Create or RW, “read or
write”). Just like in Example 3, we define the state machine and we check that
all the values are different from Error. ∎

Although this specification is valid, if most of the created files are never
read or written (or only some read or writes are relevant for the
specification), this forward monitor would be following many open files
unnecessarily.

###### Example 5

We can use _retroactive_ monitoring to only create the dynamic parameters when
the corresponding file id is read or written, and use the retroactive
capability to inspect the past of the trace and see if the file was created
previously. We redefine the streams params and all_ok accordingly.

---
10 |  output (Set String) params = let
11 | prev_params = params[-1,empty]
12 |  in if operation == RW then
13 |  insert file_id[now] prev_params
14 |  else prev_params
15 |  output Bool all_ok = let
16 |  fid = singleton file_id[now]
17 | states = elems (state ‘over‘ params ‘updating‘ fid ‘withInit‘ initer)
18 |  in all (/= Error) states

The new stream of parameters only adds a file id when it is read or written.
The new over expression specifies an initializer initer (whose definition is
not shown in the specification) that calls an external program to retrieve the
past of the corresponding parameter. The external program may use an index to
efficiently retrieve only the events in the past relevant to the current file
id. In fact, the program could fetch only the open events associated with the
file id, making the installation phase even faster. ∎

Non-retroactive dynamic parametrization avoids retrieving old events at the
expense of not preserving the semantics of static parametrization. Instead,
the parametrized stream considers that the trace only started when the
parameter was first instantiated shows up. We depict this conceptual
difference in Fig. 2.

Figure 2: Subtracing and retroactive effects in a parametrized stream s over
p0 and p1. We show the sets of dynamic parameters on top, a the parameters to
update below. The events in grey are those retrieved by the corresponding
initializer.

##### Maybe over.

We now describe additional operators that introduce useful syntactic sugar.
The operator mover (called _maybe over_) allows the discovery of a single
parameter in the middle of the trace. Instead of applying a parametrized
stream over a stream of sets of values, the operator mover takes the
parametric stream and a stream of type Maybe P, creating an expression of type
Maybe S. As in the original over, if it is retroactive or not depends on the
presence of withInit. This syntactic sugar simply creates a stream of sets of
parameters which will contain at most one element at every instant, and
returns the only value in the map when the map is not empty.

###### Example 6

To illustrate mover, we instantiate the specification in Section 2 with a
parametric threshold that is received in the middle of the trace.

---
1 |  input Double altitude
2 |  input Double threshold
3 |  output Bool alt_checker <Double threshold> = altitude[now] < threshold
4 |  output (Maybe Double) mthreshold = let
5 |  prev_mthreshold = mthreshold[-1|Nothing]
6 |  in if prev_mthreshold == Nothing && threshold[now] > 0
7 |  then Just threshold[now]
8 |  else prev_mthreshold
9 |  output Bool alt_ok = let
10 | mok = alt_checker ‘mover‘ mthreshold
11 |  in mok /= Just False

The value of mthreshold will be the first positive value of threshold, and
Nothing until then. The stream alt_ok will be $\mathbf{false}$ only when the
threshold has been set and the current altitude is greater than the
established threshold. We can use the operator withInit to add an initializer
and also revisit the past of the trace to see if the altitude had been
exceeded before the actual value was determined. ∎

##### Subtrace filter with expression.

The operator when lets us replace the updating clause with an expression that
indicates when a parameter should be updated. For example, we can specify
which file id to update using the when operator in Example 4 as follows:

---
18 |  output Bool all_ok = let
19 |  states = elems (state ‘over‘ params ‘when‘ (== file_id[now]))
20 |  in all (/= Error) states

The syntactic sugar will calculate the set of parameters
$\\{\texttt{\footnotesize{}p}\text{ such that
}e(\texttt{\footnotesize{}p})\\}$, where $e$ is the expression associated to
the when clause. Note that if we use when, the engine has to check the
condition $e$ over every live parameter to see if the corresponding stream has
to be updated. It is more efficient to directly specify the set of parameters
to update, if possible.

##  4 Implementation

The implementation of the novel operators in HLola is based on the rich type
expressivity of the tool, which include the ability to handle the Lola
language itself as a data theory within HLola [15].

Dynamically mapping a parametric stream strm with a stream of set of
parameters params of type Set P, creates an auxiliary stream x_over_params of
type Map P FrozenMonitor that associates, at every instant, each parameter $p$
in params with the state of the nested monitor corresponding to s<$p$>. The
value of x ‘over‘ params is simply the projection of the parametrized streams
in the frozen monitors of x_over_params[now]. There are three possibilities
for the behavior of the auxiliary stream for a given parameter $p$:

  1. (1)

$\texttt{\footnotesize{}{\color[rgb]{0.58984375,0.1953125,0.36328125}\definecolor[named]{pgfstrokecolor}{rgb}{0.58984375,0.1953125,0.36328125}{$p$}}}\in\texttt{\footnotesize{}params{\footnotesize{}{[}-1{|}$\emptyset${]}}}\setminus\texttt{\footnotesize{}params{\footnotesize{}{[now]}}}$:
the parameter was in the set in the previous instant, but it is no longer in
the set in the current instant. In this case, $p$ and its associated value are
deleted from the map x_over_params[-1|$\emptyset$].

  2. (2)

$\texttt{\footnotesize{}{\color[rgb]{0.58984375,0.1953125,0.36328125}\definecolor[named]{pgfstrokecolor}{rgb}{0.58984375,0.1953125,0.36328125}{$p$}}}\in\texttt{\footnotesize{}params{\footnotesize{}{[}-1{|}$\emptyset${]}}}\cap\texttt{\footnotesize{}params{\footnotesize{}{[now]}}}$:
the parameter was in the set and it is still in the set now. If $p$ is in
updating, we feed the current event to the monitor associated with $p$ and let
it progress one step. Then, the value of the parametrized stream in the nested
monitor is associated with $p$ in the returned map.

  3. (3)

$\texttt{\footnotesize{}{\color[rgb]{0.58984375,0.1953125,0.36328125}\definecolor[named]{pgfstrokecolor}{rgb}{0.58984375,0.1953125,0.36328125}{$p$}}}\in\texttt{\footnotesize{}params{\footnotesize{}{[now]}}}\setminus\texttt{\footnotesize{}params{\footnotesize{}{[}-1{|}$\emptyset${]}}}$:
the parameter was not in the set, but it is now. The monitor for $p$ is
installed, executing the initializer (possibly revisiting the past) to get the
monitor up to date and ready to continue online. Once the monitor is
installed, we proceed as in the previous case, checking whether $p$ is in
updating to decide to inject the current event, and associating the value of
s<$p$> to $p$ in the returned map. Note that the past is only revisited when a
new parameter is discovered. Once the stream is instantiated with the
parameter, its corresponding nested monitor will continue executing over the
future of the trace online.

A nested monitor can be installed with an empty initializer and at the same
time $p$ may not be in updating. In this case the nested monitor has not
processed any event, the value of s<$p$> is non existent and the sets
params[now] and
$\mathit{keys}(\texttt{\footnotesize{}x\\_over\\_params{\footnotesize{}{[now]}}})$
differ.

Since we want HLola to support initialization from different sources (e.g. a
DBMS, a blockchain node, or plain log files) the initializer of the internal
monitors typically invokes an external program. This external program, called
_adapter_ , is in charge of recovering the trace and formatting it adequately
for the monitor. The following is the architecture of our approach.

##  5 Empirical Evaluation

We report in this section an empirical evaluation of retroactive dynamic
parametrization. We have used HLola to implement several algorithms for the
detection of distributed denial of service attacks (DDOS). All the experiments
were executed on a Linux machine with $256$GB of RAM and $72$ virtual cores
(Xeon Gold 6154 @3GHz) running Ubuntu 20.04. The monitors were generated using
the implementation of HLola111Available at https://github.com/imdea-
software/hlola/ described in [14]. For conciseness we use RP to refer to
retroactive parametrization, non-RP to implementations that do not use
retroactive parametrization (and use dynamic parametrization instead). We
evaluate empirically the following hypotheses:

  * (H1)

RP is functionally equivalent to non-RP.

  * (H2)

RP and non-RP run at similar speeds, particularly when most dynamic
instantiations turn out to be irrelevant.

  * (H3)

RP consumes significantly less memory than non-RP, particularly when most
instantiations are irrelevant.

  * (H4)

Aggregated RP—where the monitor receives summaries of the trace that indicate
if further processing is necessary—is functionally equivalent to RP.

  * (H5)

Aggregated RP is much more efficient than RP and non-RP without aggregation.

The datasets for the experiments are (anonymized) samples of real network
traffic collected by a Juniper MX408 router that routes the traffic of an
academic network used by several tens of thousand of users (students and
researchers) simultaneously, routing approximately $15$ Gbps of traffic on
average. The sampling ratio provided by the routers was $1$ to $100$
flows222Most detection systems use a much slower sampling of $1$ to $1000$ or
even less. Each flow contains the metadata of the traffic sampled, with
information such as source and destination ports and addresses, protocols and
timestamps, but does not carry information about the contents of the packets.
These flows are stored in aggregated batches of $5$ minutes encoded in the
netflow format.

Our monitors implement fourteen known DDOS network attacks detection
algorithms. An attack is detected if the volume of connections to a
destination address surpasses a fixed attack-specific threshold, and those
connections come from a sufficiently large number of different attackers,
identified by source IP address. The number of different source addresses
communicating with a destination is known as the _entropy_ of the destination.
Each attack is concerned with a different port and protocol and considers a
different entropy as potentially dangerous.

In order to process the network data needed by the monitors, we developed a
Python adapter that uses nfdump, a toolset to collect and process netflow
data. The tool nfdump can be used to obtain all the flows in a batch,
optionally applying some simple filters, or to obtain summarized information
about all the flows in the batch. For example, nfdump can provide all the
flows received, filtered by a protocol or address, as well as the volume of
traffic to the IP address that has received the most connections of a specific
kind.

In our empirical evaluation we use four datasets in which we knew whether each
attack was present:

  * (D1)

One batch of network flows with an attack based on malformed UDP packets (UDP
packets with destination port $0$). This batch contains $419938$ flows, with
less than $1\%$ malformed UDP packets. The threshold for this attack is $2000$
packets per second, which is surpassed in this batch for one single address,
for which the entropy of $5$ is exceeded.

  * (D2)

One batch of network flows with no attack, containing $361867$ flows, of which
only $66$ are malformed UDP packets (roughly, $0.001\%$).

  * (D3)

One batch of network flows with no attack, but with many origin IP addresses
and $100$ destination addresses. Based on D2, we modified the source and
destination IP addresses.

  * (D4)

Intervals with several batches, where only one batch has an attack based on
malformed UDP packets.

The monitors in our experiments follow the same attack description: _In a
batch of 5 minutes of flow records, an address is under attack if it receives
more than $t_{0}$ packets per second or bits per second from more than $t_{1}$
different source addresses (where $t_{0}$ and $t_{1}$ depend on the attack)._
We have implemented monitors in three different ways333Due to space
constraints, we have included the specifications for (S1), (S2) and (S3) in
Appendix 0.A.

  * (S1)

Brute force: using dynamic parametrization the monitor calculates the number
of packets and bits per second (which we call “volume”) for all potential
target IP addresses. It also computes the entropy for each potential target
address and for each attack. For every flow, the monitor internally updates
the information about the source address, destination and volume.

  * (S2)

Retroactive: the monitor also analyses all flows, calculating the volume of
packets for each address, but in this case the monitor lazily avoids
calculating the entropy. The monitor only calculates the entropy, using RP,
when the volume of traffic for an address surpasses the threshold. The monitor
uses the _over_ operator to revisit the past flows of the batch filtered by
that attack, using the Python adapter which produces the subset of the flows
required to compute the entropy. The monitoring then continues calculating the
entropy until the end of the batch.

  * (S3)

Aggregated: the monitor receives a summary of a $5$ minute batch of network
data, as a single event containing $14$ attack markers. The monitor is based
on the ability of the backend to pre-process batches using nfdump to
obtain—for each attack and for the whole batch—the maximum volume of traffic
for any IP address. If an attack marker is over the threshold, the monitor
spawns a nested monitor that retrieves a subsets of the flows for that batch
and attack, which behaves as in S2.

The aggregation of data provides a first, coarse overview serving as a
necessary condition to spawn the expensive nested monitor. This is
particularly useful because attacks are infrequent and the ratio of false
positives of the summary detection is relatively low.

In the first experiment we run the three implementations against dataset (D4).
In this interval of multiple batches, only one of which contains an attack,
all three implementations identify the batch with the attack and correctly
detect the kind of attack and target address. This confirms empirically
hypotheses (H1) and (H4).

In the second experiment we run specifications (S1) and (S2) against datasets
(D1), (D2) and (D3). The results are reported in the following table:

|  (D1) (Attack) |  (D2) (No Attack) |  (D3) (No Attack)
---|---|---|---
(S1) (Brute force) | 18m12.146s | 15m51.599s | 16m34.795s
(S2) (Retroactive) | 20m43.921s | 17m19.844s | 19m30.518s
(S3) (Aggregated) | 0m16.208s | 0m2.109s | 0m2.115s

We can see that the running times for the brute force and retroactive
implementations are similar, while the aggregated implementation is extremely
fast in comparison, which empirically confirms (H2) and (H5). This is because
(S3) exploits the summarized information, and does not find any marker over
the threshold for the datasets (D2) and (D3) so the flows within the batch are
never individually processed. For dataset (D1), a nested monitor will be
executed because one of the markers (for the attack with malformed UPD
packets) is over the threshold, but it will only try to detect the attack
corresponding to that marker, and it will only receive a small subset of the
flows (less than $1\%$ of the flows of the batch are relevant for the attack).
If all the markers for all the attacks were over their threshold and all the
flows were implicated in the attacks, the time required would be closer to the
retroactive implementation. The ad-hoc aggregation of data by the external
tool is very efficient, as is the verification of this data by the monitor, so
this implementation is especially advantageous when the positives (or false
positives) are expected to be infrequent, and when most of the data can be
filtered out before executing the nested monitor.

|  |
---|---|---
(a) (S1) with (D1) | (b) (S1) with (D2) | (c) (S1) with (D3)
|  |
(d) (S2) with (D1) | (e) (S2) with (D1) | (f) (S2) with (D3)
Figure 3: Memory usage of the brute force (a), (b), (c) and retroactive (d),
(e), (f).

In a third experiment we run a version of specifications (S1) and
(S2)—instrumented with capabilities to measure memory consumption—on (D1),
(D2) and (D3). The results, reported in Fig. 3, empirically confirm (H3). For
the three datasets, the memory used by the brute force approach increases
linearly over time, as it has to keep track of the volume and IP entropy for
every attack and every potential target address. On the other hand, the memory
usage of the retroactive implementation remains close to constant, with a
sudden increase when an attack is detected and the past flows have to be
retrieved and processed.

##  6 Conclusions

In this paper we have introduced the concept of retroactive dynamic
parametrization. In dynamic parametrization, proposed in QEA and Lola2.0 a new
monitor (which is an instance of a generic monitor) is instantiated the first
time a parameter is discovered. In retroactive dynamic parametrization the
decision to instantiate a dynamic parametric monitor can be taken later in the
future, for example when a given parameter is discovered to be interesting.

Effectively implementing retroactive parametrization requires the ability to
revisit the history of the computation, a task that can be efficiently
implemented with a logging system. Therefore, retroactive parametrization
allows a fruitful combination of offline and online monitoring. Retroactive
parametrization also allows monitors to be created in the middle of an
execution without requiring to process the whole trace from the beginning.

We have implemented this technique in HLola and empirically evaluated its
efficiency, illustrating that it can efficiently detect distributed denial of
service attacks in realistic network traffic.

## References

  * [1] Barringer, H., Falcone, Y., Havelund, K., Reger, G., Rydeheard, D.: Quantified event automata: Towards expressive and efficient runtime monitors. In: Proc of the 18th Int’l Symp. on Formal Methods (FM’12). LNCS, vol. 7436, pp. 68–84. Springer (2012)
  * [2] Bartocci, E., Falcone, Y. (eds.): Lectures on Runtime Verification - Introductory and Advanced Topics, LNCS, vol. 10457. Springer (2018). https://doi.org/10.1007/978-3-319-75632-5, https://doi.org/10.1007/978-3-319-75632-5
  * [3] Bauer, A., Leucker, M., Schallhart, C.: Monitoring of real-time properties. In: Proc. of the 26th Int’l Conf. on Foundations of Software Technology and Theoretical Computer Science (FSTTCS’06). LNCS, vol. 4337, pp. 260–272. Springer (2006). https://doi.org/10.1007/11944836_25
  * [4] Bozzelli, L., Sánchez, C.: Foundations of boolean stream runtime verification. Theoretical Computer Science 631, 118–138 (2016). https://doi.org/10.1016/j.tcs.2016.04.019, http://dx.doi.org/10.1016/j.tcs.2016.04.019
  * [5] Ceresa, M., Gorostiaga, F., Sánchez, C.: Declarative stream runtime verification (hLola). In: Proc. of the 18th Asian Symposium on Programming Languages and Systems (APLAS’20). LNCS, vol. 12470, pp. 25–43. Springer (2020). https://doi.org/10.1007/978-3-030-64437-6_2
  * [6] Convent, L., Hungerecker, S., Leucker, M., Scheffel, T., Schmitz, M., Thoma, D.: TeSSLa: Temporal stream-based specification language. In: Proc. of the 21th Brazilian Symp. on Formal Methods (SBMF’18). LNCS, vol. 11254, pp. 144–162. Springer (2018). https://doi.org/10.1007/978-3-030-03044-5_10
  * [7] D’Angelo, B., Sankaranarayanan, S., Sánchez, C., Robinson, W., Finkbeiner, B., Sipma, H.B., Mehrotra, S., Manna, Z.: LOLA: Runtime monitoring of synchronous systems. In: Proc. of the 12th Int’l Symp. of Temporal Representation and Reasoning (TIME’05). pp. 166–174. IEEE CS Press (2005). https://doi.org/10.1109/TIME.2005.26
  * [8] Eisner, C., Fisman, D., Havlicek, J., Lustig, Y., McIsaac, A., Campenhout, D.V.: Reasoning with temporal logic on truncated paths. In: Proc. of the 15th Int’l Conf. on Computer Aided Verification (CAV’03). LNCS, vol. 2725, pp. 27–39. Springer (2003). https://doi.org/10.1007/978-3-540-45069-6_3
  * [9] Faymonville, P., Finkbeiner, B., Schirmer, S., Torfah, H.: A stream-based specification language for network monitoring. In: Proc. of the 16th Int’l Conf. on Runtime Verification (RV’16). LNCS, vol. 10012, pp. 152–168. Springer (2016). https://doi.org/10.1007/978-3-319-46982-9_10
  * [10] Faymonville, P., Finkbeiner, B., Schledjewski, M., Schwenger, M., Stenger, M., Tentrup, L., Hazem, T.: StreamLAB: Stream-based monitoring of cyber-physical systems. In: Proc. of the 31st Int’l Conf. on Computer-Aided Verification (CAV’19). LNCS, vol. 11561, pp. 421–431. Springer (2019). https://doi.org/0.1007/978-3-030-25540-4_24
  * [11] Faymonville, P., Finkbeiner, B., Schwenger, M., Torfah, H.: Real-time stream-based monitoring. CoRR abs/1711.03829 (2017)
  * [12] Goodloe, A.E., Pike, L.: Monitoring distributed real-time systems: A survey and future directions. Tech. rep., NASA Langley Research Center (2010)
  * [13] Gorostiaga, F., Sánchez, C.: Striver: Stream runtime verification for real-time event-streams. In: Proc. of the 18th Int’l Conf. on Runtime Verification (RV’18). LNCS, vol. 11237, pp. 282–298. Springer (2018). https://doi.org/10.1007/978-3-030-03769-7_16
  * [14] Gorostiaga, F., Sánchez, C.: HLola: a very functional tool for extensible stream runtime verification. In: Proc. of the 27th Int’l Conf on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’21). Part II. pp. 349–356. LNCS, Springer (2021). https://doi.org/10.1007/978-3-030-72013-1_18
  * [15] Gorostiaga, F., Sánchez, C.: Nested monitors: Monitors as expressions to build monitors. In: Feng, L., Fisman, D. (eds.) Runtime Verification. pp. 164–183. Springer International Publishing, Cham (2021). https://doi.org/10.1007/978-3-030-88494-9_9
  * [16] Gorostiaga, F., Sánchez, C.: Stream runtime verification of real-time event streams with the Striver language. International Journal on Software Tools for Technology Transfer 23, 157–183 (2021). https://doi.org/10.1007/s10009-021-00605-3, https://link.springer.com/article/10.1007/s10009-021-00605-3
  * [17] Gorostiaga, F., Sánchez, C.: Monitorability of expressive verdicts. In: Deshmukh, J.V., Havelund, K., Perez, I. (eds.) NASA Formal Methods. pp. 693–712. Springer International Publishing, Cham (2022)
  * [18] Leucker, M., Sánchez, C., Scheffel, T., Schmitz, M., Schramm, A.: Tessla: Runtime verification of non-synchronized real-time streams. In: Proc. of the 33rd ACM/SIGAPP Symposium on Applied Computing (SAC’17). pp. 1925–1933. ACM Press (2018). https://doi.org/10.1145/3167132.3167338, https://dl.acm.org/doi/10.1145/3167132.3167338, track on Software Verification and Testing Track (SVT)
  * [19] Leucker, M., Schallhart, C.: A brief account of runtime verification. J. Logic Algebr. Progr. 78(5), 293–303 (2009)
  * [20] Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems. Springer-Verlag, New York (1992)
  * [21] Perez, I., Dedden, F., Goodloe, A.: Copilot 3. Tech. Rep. NASA/TM–2020–220587, NASA Langley Research Center (April 2020)
  * [22] Pike, L., Goodloe, A., Morisset, R., Niller, S.: Copilot: A hard real-time runtime monitor. In: Proc. of the 1st Int’l Conf. on Runtime Verification (RV’10). LNCS, vol. 6418, pp. 345–359. Springer (2010). https://doi.org/10.1007/978-3-642-16612-9_26
  * [23] Pnueli, A.: The temporal logic of programs. In: Proceedings of the 18th IEEE Symposium on Foundations of Computer Science (FOCS’77),. pp. 46–67. IEEE CS Press (1977)
  * [24] Pnueli, A., Zaks, A.: PSL model checking and run-time verification via testers. In: 14th International Symposium on Formal Methods (FM’06). LNCS, vol. 4085, pp. 573–586. Springer-Verlag (2006)
  * [25] Sánchez, C.: Online and offline stream runtime verification of synchronous systems. In: Proc. of the 18th Int’l Conf. on Runtime Verification (RV’18). LNCS, vol. 11237, pp. 138–163. Springer (2018). https://doi.org/10.1007/978-3-030-03769-7_9

##  Appendix 0.A Specifications of the Empirical Evaluation

In this appendix we show the specifications that we have used to empirically
evaluate the different techniques of retroactive dynamic parameterization in
the context of network attack detection.

The first specification analyzes summaries of batches of flows, executing a
nested specification over the current batch (indicated by file_id and the
suspected attack when one of the markers is above a predefined threshold:

---
1 | use innerspec flowAnalyzer
2 |  input String fileid
3 |  input Int marker<AttackData>
4 |  output [String] attacked_IPs = map detect attacks
5 |  where detect atk = (attack_detection atk)[now]
6 |  define String attack_detection <AttackData atk> =
7 |  if (marker atk)[now] > threshold atk then
8 |  runSpec (flowAnalyzer atk ‘withTrace‘ pastRetriever atk fileid[now])
9 |  else "No attack"

The constant attacks is a list of the attack data of the $14$ different
attacks that the monitor can detect. The nested specification flowAnalyzer can
use retroactive dynamic parameterization or (the less efficient) non-
retroactive dynamic parameterization.

The second specification analyzes individual flows:

---
1 |  type Entropy = Map.Map String (Set.Set String)
2 |  type Histogram = Map.Map String Int
3 | \-- packets, bits, starttime, endtime
4 |  type AddressInfo = Map.Map String (Int, Int, Int, Int)
5 |  input String fileid
6 |  input Flow flow
7 |  define Int flowCounter = flowCounter[-1|0] \+ 1
8 |  define Bool firstFlow = fileId[now] /= fileid [-1|""]
9 |  define Bool lastFlow = fileid[now] /= fileId[1|""]
10 |  output [String] attacked_IPs = map detect attacks
11 |  where detect atk = (attack_detection atk)[now]
12 |  define String attack_detection <AttackData atk> =
13 |  if (markerRate atk)[now] > threshold atk then
14 |  if (ipEntropy atk)[now] > maxEntropy atk then
15 |  (maxDestAddress atk)[now]
16 |  else "Over threshold but not entropy"
17 |  else "No attack"

---
18 |  define Int markerRate <AttackData atk> =
19 |  if timeDur == 0 then 0
20 |  else (getMarker addrData)[now] ‘div‘ timeDur
21 | where
22 | timeDur = getTE addrData - geTS addrData
23 |  addrData = (addrInfo atk)[now] ! (maxDestAddress atk)[now]
24 |  define String maxDestAddress <AttackData atk> =
25 |  if occurrencesCurrent > occurrencesPrev
26 |  then currentAddr else previousMaxAddr
27 | where
28 |  currentAddr = destAddr[now]
29 |  currentHist = (attackHist atk)[now]
30 | occurrencesCurrent = currentHist ! currentAddr
31 | occurrencesPrev = currentHist ! previousMaxAddr
32 |  previousMaxAddr = (maxDestAddress atk)[-1|""]
33 |  define AddrInfo addrInfo <AttackData atk> =
34 |  insertWith updateValue destAddr[now] flow[now] prev
35 | where
36 |  prev = if firstFlow[now] then empty else (addrInfo atk) [-1|empty]....
37 | updateValue (p,b,ts,te) (p’,b’,ts’,te’) = (p+p’,b+b’,min ts ts’,max te te’)
38 |  define Histogram attackHist <AttackData atk> =
39 |  insertWith (+) destAddr[now] 1 hist
40 | where
41 |  hist = if firstFlow[now] then empty else (attackHist atk) [-1|empty]....

The specification defines many auxiliary types to carry information about the
destination addresses. It also needs to keep the flowCounter to perform
retroactive dynamic parameterization. As in the previous case, the stream
attacked_IPs maps the parametric stream attack_detection over the list of
attacks. The stream attack_detection checks that the marker (bits per seconds
or packets per second) of the attack and the IP entropy of any address do not
exceed the thresholds. If the thresholds are exceeded, the IP address most
accessed (which is calculated in maxDestAddress) is considered to be under
attack. The stream markerRate calculates the bits per seconds or packets per
second of an attack. The stream maxDestAddress calculates the most accessed
address, comparing the accesses of the current destination address
(destAddr[now]) with the accesses of the previously most accessed address
((maxDestAddress atk)[-1|""]). The binary operator (!) retrieves an element
from a map. The stream addrInfo keeps a map of the packets, bits, start time
and endtime per destination address. Similarly, the stream attackHist keeps a
map of the number of accesses per destination address.

The IP entropy used in line $14$ can be defined using brute force, or
retroactice dynamic parameterization. We will first the see brute force
version.

---
1 |  define Int ipEntropy <AttackData atk> =
2 |  size ((ipEntropyAllAddr atk)[now] ! (maxDestAddress atk)[now])
3 |  define Entropy ipEntropyAllAddr <AttackData atk> =
4 |  insertWith union destAddr[now] (singleton srcAddr[now]) prevEntropy
5 | where
6 |  prevEntropy = if firstFlow[now] then empty
7 |  ..................else (ipEntropyAllAddr atk) [-1|empty]....

In this specification we calculate the ip entropy of every address at all
times, and we simply return the size of the set of different origin IP
addresses of the most accesseed IP. The entropy calculation that uses
retroactive parameterization is the following.

---
1 |  define Int ipEntropy <AttackData atk> =
2 | maybe 0 size mset
3 | where
4 | mset = setSrcForDestAddr atk
5 |  .......... ‘mover‘ maybeAddress attData
6 |  .......... ‘withInit‘ initer atk (maxDestAddress atk)[now] flowCounter[now]
7 |  define (Set String) setSrcForDestAddr <AttackData atk> <String dst> =
8 |  insert srcAddr[now] prevSet
9 | where
10 |  prevSet = if firstFlow[now] then empty
11 |  ..............else (setSrcForDestAddr atk) [-1|empty]....
12 |  define (Maybe String) maybeAddress <AttackData atk> =
13 |  if (maxOverThreshold atk)[now]
14 |  then Just (maxDestAddress atk)[now]
15 |  else Nothing

In this case, we define a parametric stream setSrcForDestAddr that calculates
the set of different origin IPs of a destination address. We define an
auxiliary stream maybeAddress that contains the most accessed address, if it
exceeds the threshold. The definition of ipEntropy will instantiate
dynamically the stream setSrcForDestAddr with the most accessed address once
it exceeds the threshold, with an initializer specific to the suspected attack
and address.