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

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已经显示出我的模型有两个问题：

1. [当权限与用户具有“开启”关系时，也必须存在反向关系“ by”；
2. 对同一用户的两个权限可以将其删除，这没有意义。用户的特定操作应始终为零或一个权限。

关于如何解决的任何想法？

Answer 1

您可以将这些约束添加为“事实”：

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

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

[当权限与用户具有“开启”关系时，也必须存在反向关系“ by”；

在Alloy中具有双向链接通常是个坏主意，因为它很容易在两个方向上移动。仅在最方便的方向进行建模时，模型就容易得多。您始终可以使用函数或宏向后遍历它们。 @wmeyer正确地显示了如何约束反向链接，但是您的模型变得更加复杂，因此难以调试。

对同一用户的两个权限可以将其删除，这没有意义。用户的特定操作应始终为零或一个权限。

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

如果您仍然不希望强制执行重复的权限，那么我将引入一个保留权限的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¹│
└─────────┴───────┴─────┘