mirror of
https://github.com/hanzoai/bot-formal-models.git
synced 2026-11-02 20:15:35 +00:00
32 lines
936 B
Plaintext
32 lines
936 B
Plaintext
----------- MODULE GatewayAuthTrustedProxyHeaderSpoofHarness_BadTrustHeadersAlways -----------
|
|
EXTENDS Naturals
|
|
|
|
(******************************************************************************
|
|
* Negative model:
|
|
* BUG: forwarded identity headers are trusted even when the connection is not
|
|
* from a trusted proxy.
|
|
******************************************************************************)
|
|
|
|
CONSTANTS
|
|
TrustedProxy,
|
|
HeaderClaimsUser,
|
|
BackendAcceptsUser
|
|
|
|
ASSUME
|
|
/\ TrustedProxy \in BOOLEAN
|
|
/\ HeaderClaimsUser \in BOOLEAN
|
|
/\ BackendAcceptsUser \in BOOLEAN
|
|
|
|
\* BUG: ignore TrustedProxy bit
|
|
Authorized == HeaderClaimsUser /\ BackendAcceptsUser
|
|
|
|
Inv_NoSpoofWithoutTrustedProxy ==
|
|
(~TrustedProxy /\ HeaderClaimsUser /\ BackendAcceptsUser) => ~Authorized
|
|
|
|
VARIABLE dummy
|
|
Init == dummy = 0
|
|
Next == dummy' = dummy
|
|
Spec == Init /\ [][Next]_<<dummy>>
|
|
|
|
=============================================================================
|