Monitoring the Internet Computer (Artifact)

This artifact accompanies the paper Monitoring the Internet Computer, which will be presented at the 25th International Symposium on Formal Methods (FM 2023). It provides the policy formulas described in Section 3.2 of the paper, the raw log files that were used in the evaluation, and all tools necessary to reproduce the experimental results, specifically those reported in Table 2 and Figure 5 in the paper.

See README.md for additional information and instructions.

Erratum (August 14, 2023): Unlike stated in Table 1 of the paper, the block-validation-latency policy included in this artifact does not contain a future operator. The operator was present in an earlier version of the policy. It was removed because it was not required given the structure of the log data. The future operator can be added by inserting

EVENTUALLY [0,0]

at the end of line 50 of the file policy-monitoring/mfotl-policies/block_validation_latency/formula.mfotl. We did not observe a meaningful change in the results when we repeated the experiments using both the included and the modified policy.