Paper: Parametric timed model checking for guaranteeing timed opacity [AS19].
The version of IMITATOR used to run the experiments is IMITATOR v2.10.4 "Butter Jellyfish".
We conducted the experiments on a Dell XPS 13 9365 (2017) equipped with an Intel Core i7-7500U CPU @ 2.70GHz running Linux Mint 18.2 64 bits with 8 GiB memory.
For all case studies, the following command was used:
> ./imitator-v2.10.4-amd64 [case_study.imi] -mode EFunsafe -incl -merge -output-result
All benchmarks prefixed with STAC come from the STAC library. They were manually converted (by ourselves) from Java programs to PTAs.
In the tables, 📄 gives access to the IMITATOR model, 💾 gives access to the original Java program (if any) and 🖼️ gives access to the graphical representation (in PDF) of the IMITATOR model. 📊 gives access to the "official" result, and 📰 gives access to the log of IMITATOR.
Methodology: we run the original model, and compute all execution times. We then run a self-composition model and compute all execution times. The model is said to be non-vulnerable if the computation times are equal, vulnerable if the set of execution times for the self-composition is empty, and (vulnerable) otherwise.
Constraints can be compared using PolyOp if necessary.
The presence of parameters even in these non-parametric timed opacity checking experiments comes from the fact that the computation time is considered to be a parameter, and from the fact that for programs we abstract away user-input values using IMITATOR parameters.
| Original model | Transformed PTA | Result | ||||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| Name | Ref | Program | Model | |A| | |X| | |P| | Model | |A| | |X| | |P| | Instantiated | Self-composition | Total time (s) | Vulnerable? |
| [VNN18, Fig.5] | [VNN18] | 📄🖼️ | 1 | 1 | 2 | 📄🖼️ | 2 | 3 | 3 | 📊📰 | 📊📰 | 0.02 | (Vulnerable) | |
| [GMR07, Fig. 1b] | [GMR07] | 📄🖼️ | 1 | 1 | 1 | 📄🖼️ | 2 | 3 | 1 | 📊📰 | 📊📰 | 0.04 | (Vulnerable) | |
| [GMR07, Fig. 2a] | [GMR07] | 📄🖼️ | 1 | 1 | 1 | 📄🖼️ | 2 | 3 | 1 | 📊📰 | 📊📰 | 0.05 | (Vulnerable) | |
| [GMR07, Fig. 2b] | [GMR07] | 📄🖼️ | 1 | 1 | 1 | 📄🖼️ | 2 | 3 | 1 | 📊📰 | 📊📰 | 0.02 | (Vulnerable) | |
| Web privacy problem | [BCLR15] | 📄🖼️ | 1 | 2 | 1 | 📄🖼️ | 2 | 4 | 1 | 📊📰 | 📊📰 | 0.07 | (Vulnerable) | |
| Coffee | 📄🖼️ | 1 | 2 | 1 | 📄🖼️ | 2 | 5 | 1 | 📊📰 | 📊📰 | 0.05 | Not vulnerable | ||
| Fischer-HRSV02 | [HRSV02] | 📄🖼️ | 3 | 2 | 1 | 📄🖼️ | 6 | 5 | 1 | 📊📰 | 📊📰 | 5.83 | (Vulnerable) | |
| STAC:1:n | 💾 | 📄🖼️ | 1 | 2 | 4 | 📄🖼️ | 2 | 3 | 6 | 📊📰 | 📊📰 | 0.12 | (Vulnerable) | |
| STAC:1:v | 💾 | 📄🖼️ | 1 | 2 | 4 | 📄🖼️ | 2 | 3 | 6 | 📊📰 | 📊📰 | 0.11 | Vulnerable | |
| STAC:3:n | 💾 | 📄🖼️ | 1 | 2 | 5 | 📄🖼️ | 2 | 3 | 8 | 📊📰 | 📊📰 | 0.72 | Not vulnerable | |
| STAC:3:v | 💾 | 📄🖼️ | 1 | 2 | 5 | 📄🖼️ | 2 | 3 | 8 | 📊📰 | 📊📰 | 0.74 | (Vulnerable) | |
| STAC:4:n | 💾 | 📄🖼️ | 1 | 2 | 5 | 📄🖼️ | 2 | 3 | 8 | 📊📰 | 📊📰 | 6.4 | Vulnerable | |
| STAC:4:v | 💾 | 📄🖼️ | 1 | 2 | 5 | 📄🖼️ | 2 | 3 | 8 | 📊📰 | 📊📰 | 265.52 | Vulnerable | |
| STAC:5:n | 💾 | 📄🖼️ | 1 | 2 | 4 | 📄🖼️ | 2 | 3 | 6 | 📊📰 | 📊📰 | 0.24 | Not vulnerable | |
| STAC:11A:v | 💾 | 📄🖼️ | 1 | 2 | 5 | 📄🖼️ | 2 | 3 | 8 | 📊📰 | 📊📰 | 47.77 | (Vulnerable) | |
| STAC:11B:v | 💾 | 📄🖼️ | 1 | 2 | 5 | 📄🖼️ | 2 | 3 | 8 | 📊📰 | 📊📰 | 59.35 | (Vulnerable) | |
| STAC:12c:v | 💾 | 📄🖼️ | 1 | 2 | 5 | 📄🖼️ | 2 | 3 | 8 | 📊📰 | 📊📰 | 18.44 | Vulnerable | |
| STAC:12e:n | 💾 | 📄🖼️ | 1 | 2 | 5 | 📄🖼️ | 2 | 3 | 8 | 📊📰 | 📊📰 | 0.58 | Vulnerable | |
| STAC:12e:v | 💾 | 📄🖼️ | 1 | 2 | 5 | 📄🖼️ | 2 | 3 | 8 | 📊📰 | 📊📰 | 1.1 | (Vulnerable) | |
| STAC:14:n | 💾 | 📄🖼️ | 1 | 2 | 5 | 📄🖼️ | 2 | 3 | 8 | 📊📰 | 📊📰 | 22.34 | (Vulnerable) | |
| Original model | PTA (self-composition) | Result | |||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|
| Name | Ref | Program | |A| | |X| | |P| | Model | |A| | |X| | |P| | Time (s) | Result |
| [VNN18, Fig.5] | [VNN18] | 1 | 1 | 📄🖼️ | 2 | 3 | 4 | 0.02 | 📊📰 | ||
| [GMR07, Fig. 1b] | [GMR07] | 1 | 1 | 📄🖼️ | 2 | 3 | 3 | 0.03 | 📊📰 | ||
| [GMR07, Fig. 2] | [GMR07] | 1 | 1 | 📄🖼️ | 2 | 3 | 3 | 0.05 | 📊📰 | ||
| Web privacy problem | [BCLR15] | 1 | 2 | 2 | 📄🖼️ | 2 | 4 | 3 | 0.07 | 📊📰 | |
| Coffee | 1 | 2 | 3 | 📄🖼️ | 2 | 5 | 4 | 0.1 | 📊📰 | ||
| Fischer-HRSV02 | [HRSV02] | 3 | 2 | 1 | 📄🖼️ | 6 | 5 | 2 | 7.86 | 📊📰 | |
| Fischer-HRSV02 | [HRSV02] | 3 | 2 | 2 | 📄🖼️ | 6 | 5 | 3 | 7.53 | 📊📰 | |
| STAC:3:v | 💾 | 2 | 📄🖼️ | 2 | 3 | 9 | 0.93 | 📊📰 | |||
A script to reproduce all experiments (including binaries, models and detailed instructions) is available at Zenodo.