infsec/benchmark repository overview

⁠A Benchmark Generator for Online First-Order Monitoring

This docker image contains a randomized benchmark generator useful for attesting the correctness and performance of online first-order monitors.

⁠Version information

The version 1.2.2 is currently the latest one.

Version 1.2.2 has an additional flag (-s)

Version 1.2.1 is described in the paper:
Srđan Krstić and Joshua Schneider: A Benchmark Generator for Online First-Order Monitoring⁠

Version 1.0.0 is described in the paper:
Srđan Krstić and Joshua Schneider: Stream Characteristics for First-Order Monitoring⁠

⁠Getting Started

Note that this is a guide for the latest version of the Docker image

Assuming that you have Docker (version 19.03.8 or higher) installed on your local machine pull the image

$ docker pull infsec/benchmark

The benchmark generator consists of three components: stream generator, stream replayer, and monitoring oracle. For ease of use create the following aliases in your .bash_profile (or a similar shell configuration file):

alias generator="docker run -i -v `pwd`:/work infsec/benchmark generator"
alias replayer="docker run -i -v `pwd`:/work infsec/benchmark replayer"
alias oracle="docker run -i -v `pwd`:/work infsec/benchmark oracle"

Note that this mounts the current working directory under the name /work within the Docker container. Hence, one can access all the files below the current directory seamlessly using relative paths.

⁠Stream generator

Now you are ready to use the benchmark generator. Note that it is designed to produce random, but reproducible output. So the output of all the commands shown here should be the same on your machine as well. To get different random output, one needs to alter the random seed of the stream generator. For example the command

$ generator -S -e 2 3  > events.csv

creates a log with the time span 3 and the event rate 2 (flag -e). Hence there are 6 events in the output, two events for each time-stamp value (0, 1, and 2). To see the log type:

$ cat events.csv
C, tp=0, ts=0, x0=373321178, x1=271925315
B, tp=0, ts=0, x0=355617325, x1=141336768
B, tp=1, ts=1, x0=977202503, x1=263078228
C, tp=1, ts=1, x0=782304503, x1=947669864
A, tp=2, ts=2, x0=78200211, x1=606967315
A, tp=2, ts=2, x0=870269555, x1=943366250

Note that if you omit the time-span parameter (value 3 in the above command), the generator will create an unbounded stream of events with increasing time-stamps. In order to stop it you must kill the docker container running the generator.

For more details on the available generator flags type

$ generator --help

⁠Stream replayer

The stream replayer component when invoked as such

$ replayer -a 10 < events.csv
C, tp=0, ts=0, x0=373321178, x1=271925315
B, tp=0, ts=0, x0=355617325, x1=141336768
;;
B, tp=1, ts=1, x0=977202503, x1=263078228
C, tp=1, ts=1, x0=782304503, x1=947669864
;;
A, tp=2, ts=2, x0=78200211, x1=606967315
A, tp=2, ts=2, x0=870269555, x1=943366250
;;

reads events from the events.csv file (in the format as output by the generator) and outputs at the rate 10 times higher (flag -a) than the event rate of the log in the events.csv file. It additionally outputs the terminator symbols (;;) after every change of the time-point value.

Both the input and the output format of the replayer coincide with the output format of the generator. It is the official CSV format from the first RV competition⁠ modified slightly to accommodate the emission time and watermarks. It is described by the following grammar

  [<emission time>']<event type>, tp=<time-point>, ts=<time-stamp>, <attribute 1>=<value 1>, ..., <attribute N>=<value N>
| [<emission time>'>]WATERMARK <time-stamp><
| ;;

The replayer can also be used as a converter between different log formats. For example, the command

$ replayer -a 0 -f verimon < events.csv > events.log

reads and converts as fast as possible (-a 0) the log from the events.csv file into a format for the Verimon monitor⁠ which implements the oracle component of this benchmark generator. The converted log is saved in the event.log file.

For more details on the available replayer flags type

$ replayer --help

⁠Monitoring oracle

To invoke the oracle component type

$ oracle -S < events.log

which generates expected violations for the star formula (flag -S) on the log in events.log file. Assuming that the events.log file was generated as shown in this guide, there will be no violations.

The star formula is (ONCE [0,10) A(w,x)) IMPLIES B(w,y) IMPLIES ALWAYS [0,10) NOT C(w,z) with free variables w, x, y, and z.

Finally to see some violations type

$ generator -S -x 0.3 100 | replayer -f verimon -a 10 | oracle -S
@6. (time point 6): (375807605,108120159,958655852,20678312)
@7. (time point 7): (422305181,899366530,60448027,556360567) (489398226,131914366,219704697,362617624)
@24. (time point 24): (425257936,965546899,935381368,770633021)
@28. (time point 28): (36975499,166155535,290875578,966978378)
@37. (time point 37): (429161962,202410300,517705227,239332724)
@39. (time point 39): (327275929,44304729,154847132,711194168)
@53. (time point 53): (942745710,305012306,799373689,816709398)
@62. (time point 62): (254989956,671082106,926485855,7625044)
@70. (time point 70): (405983317,828645373,450039636,867253007)
@71. (time point 71): (524049753,906748705,21002200,107596742)
@82. (time point 82): (740932296,899485677,419462054,71436905)
@83. (time point 83): (6125029,619317531,522160185,258388318)

This command uses all three components of the benchmark generator. First, the stream generator creates a log with time span 100 and violation rate of 30% (flag -x 0.3) for the star formula (flag -S). Then replayer reproduces it 10 times faster (-a 10) and converts it to the format readable by the oracle. Then the oracle finds all violations of the star formula, which are printed here.

The format of the violations is as follows:

@<time-stamp> (time point <time-poinnt>): ([<val1>, ..., <valN>])

where <val1>, ..., <valN> are assignments to the free variables (if any) of the formula for which the log violates it.

Since the oracle is a wrapper for a fairly complex tool, for more details on its supported flags type

$ oracle --help