如何建模双向关系并使其成为强制性的？

Question

我正在开发一个简单的基于角色的授权模型，以 https://profsandhu.com/journals/tissec/p207-ahn.pdf 为灵感。到目前为止的代码是：

abstract sig Object {}

abstract sig Operation {}

sig User, Transaction extends Object {
    by: some Permission
} {
    by.on = this
}

one sig View, Update, Add, Delete extends Operation {}

sig Permission {
    to: one Operation,
    on: one Object
}

pred show {
    #Permission > 0
}

run show

生成的第一个 instance 已经显示我的模型有两个问题：

当权限与用户有 "on" 关系时，反向关系 "by" 也必须存在；
同一用户的两个权限可以删除它，这没有意义。对于用户的特定操作，应该始终有零个或一个权限。

有什么解决办法吗？

Answer 1

您可以将这些约束添加为 "facts":

fact {
    all p: Permission, u: User | p.on = u implies p in u.by
    all u: User | all disj p1,p2 : u.by | p1.to != p2.to
}

现在要验证最后一个事实，您可能还想检查同一操作的两个权限绝不会由同一用户拥有：

assert sameOperationImpliesDifferentUser {
    all disj p1, p2: Permission | p1.to = p2.to implies no (p1.on & p2.on & User)
}
check sameOperationImpliesDifferentUser

Answer 2

The first instance generated already shows two issues with my model:

When a permission has an "on" relationship to a user, the reverse relationship "by" must be there as well;

在 Alloy 中设置双向 link 通常是个坏主意，因为在两个方向上遍历都很容易。当您沿着最方便的方向制作模型时，模型会容易得多。您始终可以使用函数或宏向后遍历它们。 @wmeyer 正确地向您展示了如何约束反向 link 但是您的模型变得更加复杂，因此更难调试。

Two permissions on the same user can delete it, which doesn't make sense. There should be always zero or one permission for a particular operation on a user.

为什么这没有意义？据我所知，这些限制很难执行并且提供的价值很小。如果您在此模型中获得角色，我可以看到您最终可能会获得一个对象的多个相同权限。约束模型可能会导致模型没有解。丹尼尔杰克逊还指出，最好的工作方式是尽量减少限制。

如果您仍然想强制执行无重复权限，我会引入一个拥有权限的 Role 对象。

我理解（我认为）您为什么希望用户扩展对象，但这确实会使模型的解决方案难以浏览。角色也可以提供帮助。

所以我的 2cts 模型是：

abstract sig Object {}

enum Operation { View, Update, Add, Delete }

sig Transaction extends Object {}

sig User extends Object {
    role : set Role
}

sig Role {
    permit : Operation lone -> Object
}

有解决办法：

┌─────────┬─────┐
│this/User│role │
├─────────┼─────┤
│User⁰    │Role²│
│         ├─────┤
│         │Role³│
├─────────┼─────┤
│User¹    │Role⁰│
│         ├─────┤
│         │Role¹│
│         ├─────┤
│         │Role³│
└─────────┴─────┘

┌─────────┬─────────────┐
│this/Role│permit       │
├─────────┼───────┬─────┤
│Role⁰    │Delete⁰│User¹│
├─────────┼───────┼─────┤
│Role¹    │Update⁰│User⁰│
│         ├───────┼─────┤
│         │View⁰  │User¹│
├─────────┼────┬──┴─────┤
│Role²    │Add⁰│User¹   │
├─────────┼────┴──┬─────┤
│Role³    │Add⁰   │User⁰│
│         ├───────┼─────┤
│         │Update⁰│User¹│
└─────────┴───────┴─────┘

如何建模双向关系并使其成为强制性的？

How to model a bi-directional relationship and make it mandatory?

alloy