Differential testing case study
385
This image contains artifacts necessary to reproduce the case study from the papers
Joshua Schneider, David Basin, Srdan Krstic, and Dmitriy Traytel: A Formally Verified Monitor for Metric First-Order Temporal Logic (tag 1.3.0)
David Basin, Thibault Dardinier, Lukas Heimes, Srdan Krstic, Martin Raszyk, Joshua Schneider, and Dmitriy Traytel: A Formally Verified, Optimized Monitor for Metric First-Order Dynamic Logic (tag 1.4.0)
Please see https://docs.docker.com/ for more information about installing and using Docker. Run the following commands to start a container with this image
$ docker pull infsec/verified-monpoly-exps:VERSION
$ docker run -it infsec/verified-monpoly-exps:VERSION
where VERSION should be replaced with the appropriate tag. To reproduce
the results from one of the papers, use the tag referenced above, otherwise use
latest.
Running these commands opens an interactive shell running inside the container. From this shell you can view the individual experiments in the folders exp1, exp2, exp3, exp4, exp5, and exp6. The version tagged with 1.3.0 contains exp1 through exp4, while 1.4.0 contains exp1 through exp6.
The monitors involved in the experiments have their own docker images:
The experiments are summarized below. In particular, the experiment in the folder exp4 corresponds to the description of the differential testing experiments in both papers. Experiments in folders exp5 and exp6 correspond to the description in paper 2.
The folder "examples" contains the minimal examples mentioned in the papers. The examples are subdivided between the two papers that report them (folders examples-paper1 and examples-paper2). In each subfolder (e.g., monpoly1) you can run
$ ./run.sh
to view and compare the output of the tools.
Note that the MonPoly examples in examples-paper1 are run with the version of MonPoly that was patched to address these problematic examples, hence the printed outputs match.
To rerun all experiments, navigate back to the initial folder (/home/root/monpoly) and run
$ ./experiments.sh
to start all experiments. This will take a long time (roughly a day) and significant disk space (~15GB), since all the generated random logs will be saved for later inspection. If you want to run a specific experiment (e.g., exp4), execute
$ cd exp4
$ ./experiments.sh
You can also adjust the extensiveness of the experiments by modifying the
REPETITIONS parameter in each experiments.sh file to a smaller number.
After the script has finished, any difference in the output between a tool (depending on the experiment) and the oracle is saved in a file
exp4/reports/<log_identifier>_diff_<tool name>
All verdicts are saved in the files
exp4/verdicts/<log_identifier>_<tool name>
exp4/verdicts/<log_identifier>_oracle_<tool name>
where <log_identifier> has the following structure:
<experiment_name>_<repetition_number>_<formula_identifier>_<event_rate>_<index_rate>_part<log_timespan>_seed<random_seed>
For example: random_1_-F-2-0-1_20_20_part60_seed16864
The <formula_identifier> has the following structure:
-F-<formula_size>-<free_variable_number>-<repetition_number>
For example: -F-2-0-1
This folder structure is the same in every experiment (exp1 through exp6).
To run a single test for MonPoly:
$ monpoly -sig exp4/fmas/<formula_identifier>_future.sig \
-formula exp4/fmas/<formula_identifier>_future.mfotl \
-log exp4/logs/<log_identifier> -no_rw -nofilteremptytp -nofilterrel -nonewlastts
Tun run a single test for DejaVu:
# DejaVu
$ ./dejavu-original exp4/fmas/<formula_identifier>.qtl exp4/logs/<log_identifier>_dejavu
To run VeriMon, use
# VeriMon
$ verimon -sig exp4/fmas/<formula_identifier>.sig \
-formula exp4/fmas/<formula_identifier>.mfotl \
-log exp4/logs/<log_identifier>_oracle -no_rw -nofilteremptytp -nofilterrel -nonewlastts
Note that the test inputs are generated with random seeds. Therefore, the results may change from run to run.
exp1: Random logs and fixed (star, linear, and triangle) formulas.
Monitored formulas have the form
((ONCE[0,10) A(...)) AND B(...)) AND EVENTUALLY[0,10) C(...)
where the variable patters are the following.
Star: A(w,x), B(w,y), C(w,z)
Linear: A(w,x), B(x,y), C(y,z)
Triangle: A(x,y), B(y,z), C(z,x)
The comparison with DejaVu uses non-metric past-only variants of the formulas.
exp2: Random logs and the fixed formula P1 from
exp3: Random logs and the "data race" formula from https://github.com/havelund/dejavu/blob/master/out/examples/locks/dataraces/prop.qtl
exp4: Random logs and random formulas for differential testing of MonPoly and DejaVu against VeriMon+. The experiment is as described in
exp5: Random logs and random formulas for performance evaluation of MonPoly, VeriMon, VeriMon+, Aerial and Hydra. The experiment is described in the performance evaluation part of the paper:
After running experiments.sh, run the table.sh script to get the table as shown in the paper. The table can be found in table.txt file generated by the script.
exp6: Random logs and random formulas for differential testing of Aerial and Hydra against VeriMon+. The experiment is described in the differential testing part of the paper:
To run individual experiments with Aerial, Hydra, and VeriMon and to obtain comparable results run:
# Aerial
$ aerial -fmla exp6/fmas/<formula_identifier>.mdl \
-log exp6/logs/<log_identifier> \
-mode naive | sed '/^[A-Z]/d' | grep false | sort -n
# Hydra
$ hydra exp6/fmas/<formula_identifier>.mdl logs/<log_identifier> | sed '/^[A-Z]/d'
# VeriMon
$ verimon -sig exp6/fmas/<formula_identifier>.sig \
-formula exp6/fmas/<formula_identifier>.mdl \
-log exp6/logs/<log_identifier> \
-negate -no_rw -nofilteremptytp -nofilterrel \
| sed 's/@//g;s/. (time point /:/g;s/)://g;s/ true/:false/g' \
| awk -F':' -v d=10 '{print $1,($2 % d),$3}' OFS=':' | sed 's/:false/ false/g'
Content type
Image
Digest
Size
455.9 MB
Last updated
over 6 years ago
docker pull infsec/verified-monpoly-exps