超属性的灰盒监控（扩展版）
计算机科学中的逻辑
2019-10-07 v3 密码学与安全
形式语言与自动机理论
摘要
许多重要的系统属性，尤其在安全与隐私领域，无法静态验证。因此运行时验证是一种颇具吸引力的替代方案。用于超属性的逻辑，如 HyperLTL，支持一类丰富的此类属性。我们首先表明 HyperLTL 的黑盒监控一般而言不可行，并提出了一种灰盒方法。灰盒监控意味着在运行时对系统进行分析，这给可监控性（解决监控问题的可行性）带来了新的限制。因此，作为本文的另一贡献，我们细化了经典的监控性概念，既包括迹属性也包括超属性，同时考量监控器的可计算性。随后，我们通过将基于 SMT 的静态验证器用于运行时，将该方法应用于监控称为分布式数据最小性的隐私超属性，其表述为一条 HyperLTL 属性。
引用
@article{arxiv.1906.08731,
title = {Gray-box Monitoring of Hyperproperties (Extended Version)},
author = {Sandro Stucki and César Sánchez and Gerardo Schneider and Borzoo Bonakdarpour},
journal= {arXiv preprint arXiv:1906.08731},
year = {2019}
}
备注
This is an extended version of a paper presented at the 23rd International Symposium on Formal Methods (FM '19). This version contains full proofs, a description of the proof-of-concept monitor for DDM, and experimental results that were not included in the original publication