Как смоделировать двунаправленные отношения и сделать их обязательными? - PullRequest
Новая
       14

Как смоделировать двунаправленные отношения и сделать их обязательными?

1 голос
/ 07 февраля 2020

Я разрабатываю простую модель авторизации на основе ролей, используя 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

Первый экземпляр , сгенерированный уже, показывает две проблемы с моей моделью:

  1. Когда у разрешения есть «on» отношение к пользователю, там также должна быть обратная связь «по»;
  2. Два разрешения для одного и того же пользователя могут удалить его, что не имеет смысла. Всегда должно быть ноль или одно разрешение для конкретной операции для пользователя.

Есть идеи как решить?

Ответы [ 2 ]

0 голосов
/ 11 февраля 2020

Первый сгенерированный экземпляр уже показывает две проблемы с моей моделью:

Когда разрешение имеет отношение «к пользователю», должно быть и обратное отношение «по»;

Обычно плохой идеей является наличие двунаправленных связей в Alloy, поскольку их легко перемещать в обоих направлениях. Модели значительно проще, когда вы просто делаете их в наиболее удобном направлении. Вы всегда можете использовать функцию или макрос, чтобы пройти их назад. @wmeyer правильно показывает, как ограничить обратную ссылку, но ваша модель становится намного более сложной и, следовательно, более сложной для отладки.

Два разрешения для одного пользователя могут удалить его, что не имеет смысла , Всегда должно быть ноль или одно разрешение для конкретной операции для пользователя.

Почему это не имеет смысла? Подобные ограничения трудно применять и, насколько я понимаю, очень мало значат. Если вы получите роли в этой модели, я мог бы увидеть, что у вас может быть несколько идентичных разрешений для объекта. Ограничение модели может привести к тому, что у модели не будет решений. Даниэль Джексон также указывает, что лучший способ работать - это минимизировать ограничения.

Если вы по-прежнему хотите применять не повторяющиеся разрешения, я бы представил объект Role, который содержит разрешения.

I Я понимаю (я думаю), почему вы хотите, чтобы пользователь расширил объект, но это делает решения модели неудобными для просмотра. Здесь также может помочь роль.

Итак, моя модель 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¹│
└─────────┴───────┴─────┘
0 голосов
/ 08 февраля 2020

Вы можете добавить эти ограничения как «факты»: 

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
...