Temporal Mode-Checking for Runtime Monitoring of Privacy Policies
Temporal Mode-Checking for Runtime Monitoring of Privacy Policies
复制标题
用于隐私策略运行时监控的时间模式检查
DOI：
--
复制
发表时间：
2014
期刊：
影响因子：
--
通讯作者：
Anupam Datta
中科院分区：
文献类型：
--
作者：
Omar Chowdhury;Limin Jia;D. Garg;Anupam Datta
一阶时态逻辑片段对于表示许多实际的隐私和安全策略很有用。以往的工作提出了两种检查事件轨迹（审计日志）是否符合策略的策略：在线监测和离线审计。尽管在线监测在空间和时间上是高效的，但现有技术坚持认为策略的所有子公式的满足实例必须适合缓存，这在一些子公式具有无限支持时限制了表达能力。相比之下，离线审计是暴力方法，可以处理更多的策略，但效率不高。本文提出了一种新的在线监测算法，该算法在可能的情况下缓存满足实例，在不可能的情况下回退到暴力搜索。我们的关键技术见解是一种对变量基础的新的流和时间敏感的静态检查，称为时态模式检查，它确定哪些子公式适合这种缓存，哪些不适合，从而指导我们的算法。我们证明了我们算法的正确性，并在合成轨迹和实际策略上评估了其性能。
这是2014年第26届国际计算机辅助验证会议（CAV）上发表的题为“隐私策略运行时监测的时态模式检查”的论文的扩展版本。本文所表达的所有观点仅代表作者的观点。
Fragments of first-order temporal logic are useful for representing many practical privacy and security policies. Past work has proposed two strategies for checking event trace (audit log) compliance with policies: online monitoring and offline audit. Although online monitoring is spaceand timeefficient, existing techniques insist that satisfying instances of all subformulas of the policy be amenable to caching, which limits expressiveness when some subformulas have infinite support. In contrast, offline audit is brute force and can handle more policies but is not as efficient. This paper proposes a new online monitoring algorithm that caches satisfying instances when it can, and falls back to the brute force search when it cannot. Our key technical insight is a new flowand time-sensitive static check of variable groundedness, called the temporal mode check, which determines subformulas for which such caching is feasible and those for which it is not and, hence, guides our algorithm. We prove the correctness of our algorithm and evaluate its performance over synthetic traces and realistic policies. z This is the extended version of the paper titled “Temporal Mode-Checking for Runtime Monitoring of Privacy Policies” that appears in the 26th International Conference on Computer Aided Verification (CAV) 2014. All the opinions expressed in this paper represent only the authors’ views.
基于历史的访问控制和信誉系统的逻辑框架
影响因子：
1.2
作者：
Krukow K
通讯作者：
Krukow K