利用前缀树高效监控超性质
计算机科学中的逻辑
2021-01-19 v1
摘要
超性质，如非干扰与观测确定性，将多条计算迹相互关联，因而无法由孤立考察计算的工具进行监控。我们介绍了最新版 RVHyper（一个用于超性质的运行时验证工具）中所实现的监控方法。该工具的输入是以时序逻辑 HyperLTL 给出的规范，HyperLTL 通过引入迹量词与迹变量扩展了线性时序逻辑（LTL）。RVHyper 顺序处理执行迹，直至检测到违反规范的情况。此时，将以一组迹的形式返回反例。RVHyper 采用一系列优化：对规范进行预处理分析，以及一种在监控过程中最小化需存储迹的过程。本文中，我们引入一种新颖的迹存储技术，将迹排列为树状结构以利用部分相等的迹。我们在安全信息流控制、纠错码与硬件设计对称性方面的已有基准上评估 RVHyper。作为安全领域之外的一个示例应用，我们展示了 RVHyper 如何用于检测硬件设计中的伪依赖。
引用
@article{arxiv.2101.07109,
title = {Efficient Monitoring of Hyperproperties using Prefix Trees},
author = {Bernd Finkbeiner and Christopher Hahn and Marvin Stenger and Leander Tentrup},
journal= {arXiv preprint arXiv:2101.07109},
year = {2021}
}
备注
arXiv admin note: text overlap with arXiv:1807.00758, arXiv:1906.00798