mirror of
https://github.com/hanzoai/bot-formal-models.git
synced 2026-10-30 18:46:45 +00:00
36 lines
1.0 KiB
Plaintext
36 lines
1.0 KiB
Plaintext
------------------------------ MODULE NodesCommandPolicy_BadNoDeclareCheck ------------------------------
|
|
EXTENDS Naturals, FiniteSets
|
|
|
|
(******************************************************************************
|
|
* Negative test: BUGGY node command policy that forgets to require declaredCommands.
|
|
******************************************************************************)
|
|
|
|
CONSTANTS
|
|
Commands,
|
|
PlatformDefaults,
|
|
ExtraAllow,
|
|
Deny,
|
|
DeclaredByNode,
|
|
Cmd
|
|
|
|
ASSUME
|
|
/\ Commands /= {}
|
|
/\ PlatformDefaults \subseteq Commands
|
|
/\ ExtraAllow \subseteq Commands
|
|
/\ Deny \subseteq Commands
|
|
/\ DeclaredByNode \subseteq Commands
|
|
|
|
EffectiveAllowlist == (PlatformDefaults \cup ExtraAllow) \ Deny
|
|
|
|
\* BUG: ignore DeclaredByNode
|
|
IsAllowed(cmd) == (cmd \in EffectiveAllowlist)
|
|
|
|
Inv_AllowedImpliesDeclared == \A c \in Commands: IsAllowed(c) => (c \in DeclaredByNode)
|
|
|
|
VARIABLE dummy
|
|
Init == dummy = 0
|
|
Next == dummy' = dummy
|
|
Spec == Init /\ [][Next]_<<dummy>>
|
|
|
|
=============================================================================
|