检测数据泄漏？

Question

我有一棵元素树。我从一些元素中收集数据并使用该数据创建一组节点。我想要一个断言来检查，如果只访问节点集，则不可能访问其他数据，例如树的其他元素中的数据。也就是我要保证不泄露数据

这是我的元素树：

sig Element {
    data: Data,
    children: set Element
}

我从一些元素中收集数据。我把数据塞进节点：

sig Node {
    data: Data
}

如果某人只能访问节点集，则不会有数据泄漏，因为节点只包含有意从树中的元素中获取的数据。

但是，出于调试目的，我向节点添加了一个字段以引用作为节点数据源的元素：

sig Node {
    data: Data,
    represents: Element
}

由于疏忽，represents 字段未被删除。现在，可以访问节点集的人也可以访问树，因此可以看到比他应该看到的更多的数据。因此，存在数据泄露的可能性。

我想创建一个断言来检查模型是否存在潜在的数据泄漏：

assert No_data_leakage { ??? }

直觉上，我希望断言是这样说的：在这个模型中的值域 (univ) 中，只能访问节点集的人只能访问节点集中的数据值节点，仅此而已。我该如何表达？

下面是我的模型的简化版本。

open util/ordering[Element]
open util/ordering[Node]

sig Element {
    data: Data,
    children: set Element
}
one sig Root extends Element {}

sig Data {}

sig Node {
    data: Data,
    represents: Element
}

fact No_disconnected_elements {
    all e: Element |
        (e = Root) or (e in Root.^children)
}

fact Each_element_has_one_parent {
    no disj e, e', e'': Element | 
        (e in e'.children) and (e in e''.children) 
}

fact No_loops {
    no e: Element | e in e.^children
}

fact First_Node_data_is_first_Element_data {
    (Node <: first).data = (Element <: first).data
    (Node <: first).represents = (Element <: first)
}

fact Last_Node_data_is_last_Element_data {
    (Node <: last).data = (Element <: last).data
    (Node <: last).represents = (Element <: last)
}

fact Every_element_has_different_data {
   no disj e, e': Element | e.data = e'.data
}

run {} for 3 but 2 Node

assert No_data_leaks {
    // How to express this?
}

Answer 1

见http://alloytools.org/quickguide/meta.html

有一个元功能允许您 'iterate' 在 Atom 的字段上。

assert no_data_leaks {
   all f : Node$.subfields| f.value[Node] in Data
}

检测数据泄漏？

Detecting data leakage?

alloy