mirror of
https://github.com/johndoe6345789/metabuilder.git
synced 2026-04-24 13:54:57 +00:00
645 lines
23 KiB
Plaintext
645 lines
23 KiB
Plaintext
---------------------------- MODULE integrations ----------------------------
|
|
(***************************************************************************
|
|
* Integration Ecosystem Specification for MetaBuilder *
|
|
* *
|
|
* This specification models the integration ecosystem including: *
|
|
* - Webhook management and delivery *
|
|
* - OAuth application framework *
|
|
* - API key management *
|
|
* - Third-party app directory *
|
|
* - Event subscriptions and filtering *
|
|
* - Rate limiting and quota management *
|
|
***************************************************************************)
|
|
|
|
EXTENDS Naturals, Sequences, FiniteSets, TLC
|
|
|
|
CONSTANTS
|
|
Users, \* Set of all users
|
|
Tenants, \* Set of tenants
|
|
Webhooks, \* Set of webhook IDs
|
|
OAuthApps, \* Set of OAuth application IDs
|
|
APIKeys, \* Set of API key IDs
|
|
EventTypes, \* Set of event types to subscribe to
|
|
MaxWebhooksPerTenant, \* Maximum webhooks per tenant
|
|
MaxKeysPerUser, \* Maximum API keys per user
|
|
RateLimitPerHour \* API calls allowed per hour
|
|
|
|
VARIABLES
|
|
userLevels, \* User -> Permission Level
|
|
userTenants, \* User -> Tenant
|
|
webhookConfigs, \* Set of webhook configurations
|
|
webhookQueue, \* Sequence of pending webhook deliveries
|
|
webhookDeliveries, \* Set of delivery records
|
|
oauthApps, \* Set of OAuth application records
|
|
oauthTokens, \* Set of OAuth token records
|
|
apiKeys, \* Set of API key records
|
|
apiCallCounts, \* (User/App, Hour) -> Call count
|
|
eventSubscriptions, \* Set of event subscriptions
|
|
integrationAuditLog \* Sequence of integration events
|
|
|
|
vars == <<userLevels, userTenants, webhookConfigs, webhookQueue,
|
|
webhookDeliveries, oauthApps, oauthTokens, apiKeys,
|
|
apiCallCounts, eventSubscriptions, integrationAuditLog>>
|
|
|
|
-----------------------------------------------------------------------------
|
|
(* Type Definitions *)
|
|
|
|
PermissionLevel == 1..6
|
|
|
|
WebhookStatus == {"active", "paused", "disabled"}
|
|
DeliveryStatus == {"pending", "success", "failed", "retrying"}
|
|
OAuthAppStatus == {"active", "suspended", "revoked"}
|
|
APIKeyStatus == {"active", "expired", "revoked"}
|
|
|
|
WebhookConfig == [
|
|
id: Webhooks,
|
|
tenantId: Tenants,
|
|
ownerId: Users,
|
|
url: STRING,
|
|
status: WebhookStatus,
|
|
events: SUBSET EventTypes,
|
|
secret: STRING,
|
|
createdAt: Nat
|
|
]
|
|
|
|
WebhookDelivery == [
|
|
id: Nat,
|
|
webhookId: Webhooks,
|
|
eventType: EventTypes,
|
|
payload: STRING,
|
|
status: DeliveryStatus,
|
|
attempts: Nat,
|
|
timestamp: Nat
|
|
]
|
|
|
|
OAuthApp == [
|
|
id: OAuthApps,
|
|
tenantId: Tenants,
|
|
ownerId: Users,
|
|
name: STRING,
|
|
status: OAuthAppStatus,
|
|
scopes: SUBSET STRING,
|
|
redirectUri: STRING,
|
|
clientId: STRING,
|
|
createdAt: Nat
|
|
]
|
|
|
|
OAuthToken == [
|
|
id: Nat,
|
|
appId: OAuthApps,
|
|
userId: Users,
|
|
tenantId: Tenants,
|
|
accessToken: STRING,
|
|
scopes: SUBSET STRING,
|
|
expiresAt: Nat,
|
|
createdAt: Nat
|
|
]
|
|
|
|
APIKey == [
|
|
id: APIKeys,
|
|
userId: Users,
|
|
tenantId: Tenants,
|
|
name: STRING,
|
|
key: STRING,
|
|
status: APIKeyStatus,
|
|
scopes: SUBSET STRING,
|
|
expiresAt: Nat,
|
|
createdAt: Nat
|
|
]
|
|
|
|
EventSubscription == [
|
|
id: Nat,
|
|
subscriberId: Users \cup OAuthApps,
|
|
tenantId: Tenants,
|
|
eventType: EventTypes,
|
|
filters: STRING,
|
|
active: BOOLEAN
|
|
]
|
|
|
|
TypeOK ==
|
|
/\ userLevels \in [Users -> PermissionLevel]
|
|
/\ userTenants \in [Users -> Tenants]
|
|
/\ webhookConfigs \subseteq WebhookConfig
|
|
/\ webhookQueue \in Seq(WebhookDelivery)
|
|
/\ webhookDeliveries \subseteq WebhookDelivery
|
|
/\ oauthApps \subseteq OAuthApp
|
|
/\ oauthTokens \subseteq OAuthToken
|
|
/\ apiKeys \subseteq APIKey
|
|
/\ apiCallCounts \in [(Users \cup OAuthApps) \X Nat -> Nat]
|
|
/\ eventSubscriptions \subseteq EventSubscription
|
|
/\ integrationAuditLog \in Seq([
|
|
user: Users \cup {"system"},
|
|
action: STRING,
|
|
targetId: Nat \cup Webhooks \cup OAuthApps \cup APIKeys,
|
|
tenant: Tenants,
|
|
timestamp: Nat
|
|
])
|
|
|
|
-----------------------------------------------------------------------------
|
|
(* Permission Checks *)
|
|
|
|
\* Admin level (4+) required for integration management
|
|
CanManageIntegrations(user, tenant) ==
|
|
/\ userLevels[user] >= 4
|
|
/\ userTenants[user] = tenant
|
|
|
|
\* User level (2+) required for API keys
|
|
CanManageAPIKeys(user) ==
|
|
userLevels[user] >= 2
|
|
|
|
-----------------------------------------------------------------------------
|
|
(* Helper Functions *)
|
|
|
|
\* Count webhooks for a tenant
|
|
CountWebhooksForTenant(tenant) ==
|
|
Cardinality({w \in webhookConfigs : w.tenantId = tenant})
|
|
|
|
\* Count API keys for a user
|
|
CountKeysForUser(user) ==
|
|
Cardinality({k \in apiKeys : k.userId = user /\ k.status = "active"})
|
|
|
|
\* Get API call count for current hour
|
|
GetCallCount(identity, hour) ==
|
|
IF <<identity, hour>> \in DOMAIN apiCallCounts
|
|
THEN apiCallCounts[<<identity, hour>>]
|
|
ELSE 0
|
|
|
|
\* Check if rate limit exceeded
|
|
RateLimitExceeded(identity, hour) ==
|
|
GetCallCount(identity, hour) >= RateLimitPerHour
|
|
|
|
-----------------------------------------------------------------------------
|
|
(* Initial State *)
|
|
|
|
Init ==
|
|
/\ userLevels \in [Users -> PermissionLevel]
|
|
/\ userTenants \in [Users -> Tenants]
|
|
/\ webhookConfigs = {}
|
|
/\ webhookQueue = <<>>
|
|
/\ webhookDeliveries = {}
|
|
/\ oauthApps = {}
|
|
/\ oauthTokens = {}
|
|
/\ apiKeys = {}
|
|
/\ apiCallCounts = [x \in (Users \cup OAuthApps) \X Nat |-> 0]
|
|
/\ eventSubscriptions = {}
|
|
/\ integrationAuditLog = <<>>
|
|
|
|
-----------------------------------------------------------------------------
|
|
(* Webhook Operations *)
|
|
|
|
\* Admin creates a webhook
|
|
CreateWebhook(user, wid, url, events, secret) ==
|
|
/\ CanManageIntegrations(user, userTenants[user])
|
|
/\ wid \in Webhooks
|
|
/\ wid \notin {w.id : w \in webhookConfigs}
|
|
/\ CountWebhooksForTenant(userTenants[user]) < MaxWebhooksPerTenant
|
|
/\ events \subseteq EventTypes
|
|
/\ events /= {}
|
|
/\ LET newWebhook == [
|
|
id |-> wid,
|
|
tenantId |-> userTenants[user],
|
|
ownerId |-> user,
|
|
url |-> url,
|
|
status |-> "active",
|
|
events |-> events,
|
|
secret |-> secret,
|
|
createdAt |-> Len(integrationAuditLog)
|
|
] IN
|
|
/\ webhookConfigs' = webhookConfigs \cup {newWebhook}
|
|
/\ integrationAuditLog' = Append(integrationAuditLog, [
|
|
user |-> user,
|
|
action |-> "create_webhook",
|
|
targetId |-> wid,
|
|
tenant |-> userTenants[user],
|
|
timestamp |-> Len(integrationAuditLog)
|
|
])
|
|
/\ UNCHANGED <<userLevels, userTenants, webhookQueue, webhookDeliveries,
|
|
oauthApps, oauthTokens, apiKeys, apiCallCounts,
|
|
eventSubscriptions>>
|
|
|
|
\* Admin updates webhook status
|
|
UpdateWebhookStatus(user, wid, newStatus) ==
|
|
/\ \E w \in webhookConfigs :
|
|
/\ w.id = wid
|
|
/\ CanManageIntegrations(user, w.tenantId)
|
|
/\ newStatus \in WebhookStatus
|
|
/\ webhookConfigs' = (webhookConfigs \ {w}) \cup
|
|
{[w EXCEPT !.status = newStatus]}
|
|
/\ integrationAuditLog' = Append(integrationAuditLog, [
|
|
user |-> user,
|
|
action |-> "update_webhook_status",
|
|
targetId |-> wid,
|
|
tenant |-> w.tenantId,
|
|
timestamp |-> Len(integrationAuditLog)
|
|
])
|
|
/\ UNCHANGED <<userLevels, userTenants, webhookQueue, webhookDeliveries,
|
|
oauthApps, oauthTokens, apiKeys, apiCallCounts,
|
|
eventSubscriptions>>
|
|
|
|
\* System enqueues webhook delivery
|
|
EnqueueWebhook(wid, eventType, payload, deliveryId) ==
|
|
/\ \E w \in webhookConfigs :
|
|
/\ w.id = wid
|
|
/\ w.status = "active"
|
|
/\ eventType \in w.events
|
|
/\ deliveryId \notin {d.id : d \in webhookDeliveries}
|
|
/\ LET delivery == [
|
|
id |-> deliveryId,
|
|
webhookId |-> wid,
|
|
eventType |-> eventType,
|
|
payload |-> payload,
|
|
status |-> "pending",
|
|
attempts |-> 0,
|
|
timestamp |-> Len(integrationAuditLog)
|
|
] IN
|
|
/\ webhookQueue' = Append(webhookQueue, delivery)
|
|
/\ webhookDeliveries' = webhookDeliveries \cup {delivery}
|
|
/\ UNCHANGED <<userLevels, userTenants, webhookConfigs, oauthApps,
|
|
oauthTokens, apiKeys, apiCallCounts, eventSubscriptions,
|
|
integrationAuditLog>>
|
|
|
|
\* System attempts webhook delivery
|
|
AttemptDelivery(deliveryId) ==
|
|
/\ Len(webhookQueue) > 0
|
|
/\ \E d \in webhookDeliveries :
|
|
/\ d.id = deliveryId
|
|
/\ d.status \in {"pending", "retrying"}
|
|
/\ webhookDeliveries' = (webhookDeliveries \ {d}) \cup
|
|
{[d EXCEPT
|
|
!.status = "success",
|
|
!.attempts = @ + 1
|
|
]}
|
|
/\ webhookQueue' = Tail(webhookQueue)
|
|
/\ UNCHANGED <<userLevels, userTenants, webhookConfigs, oauthApps,
|
|
oauthTokens, apiKeys, apiCallCounts, eventSubscriptions,
|
|
integrationAuditLog>>
|
|
|
|
\* Webhook delivery fails
|
|
FailDelivery(deliveryId) ==
|
|
/\ \E d \in webhookDeliveries :
|
|
/\ d.id = deliveryId
|
|
/\ d.status \in {"pending", "retrying"}
|
|
/\ d.attempts < 3
|
|
/\ webhookDeliveries' = (webhookDeliveries \ {d}) \cup
|
|
{[d EXCEPT
|
|
!.status = "retrying",
|
|
!.attempts = @ + 1
|
|
]}
|
|
/\ UNCHANGED <<userLevels, userTenants, webhookConfigs, webhookQueue,
|
|
oauthApps, oauthTokens, apiKeys, apiCallCounts,
|
|
eventSubscriptions, integrationAuditLog>>
|
|
|
|
\* Webhook delivery permanently fails
|
|
PermanentFailDelivery(deliveryId) ==
|
|
/\ \E d \in webhookDeliveries :
|
|
/\ d.id = deliveryId
|
|
/\ d.status = "retrying"
|
|
/\ d.attempts >= 3
|
|
/\ webhookDeliveries' = (webhookDeliveries \ {d}) \cup
|
|
{[d EXCEPT !.status = "failed"]}
|
|
/\ webhookQueue' = SelectSeq(webhookQueue, LAMBDA x : x.id /= deliveryId)
|
|
/\ UNCHANGED <<userLevels, userTenants, webhookConfigs, oauthApps,
|
|
oauthTokens, apiKeys, apiCallCounts, eventSubscriptions,
|
|
integrationAuditLog>>
|
|
|
|
-----------------------------------------------------------------------------
|
|
(* OAuth Application Management *)
|
|
|
|
\* Admin creates OAuth app
|
|
CreateOAuthApp(user, appId, name, scopes, redirectUri) ==
|
|
/\ CanManageIntegrations(user, userTenants[user])
|
|
/\ appId \in OAuthApps
|
|
/\ appId \notin {a.id : a \in oauthApps}
|
|
/\ LET newApp == [
|
|
id |-> appId,
|
|
tenantId |-> userTenants[user],
|
|
ownerId |-> user,
|
|
name |-> name,
|
|
status |-> "active",
|
|
scopes |-> scopes,
|
|
redirectUri |-> redirectUri,
|
|
clientId |-> "client_" \o appId,
|
|
createdAt |-> Len(integrationAuditLog)
|
|
] IN
|
|
/\ oauthApps' = oauthApps \cup {newApp}
|
|
/\ integrationAuditLog' = Append(integrationAuditLog, [
|
|
user |-> user,
|
|
action |-> "create_oauth_app",
|
|
targetId |-> appId,
|
|
tenant |-> userTenants[user],
|
|
timestamp |-> Len(integrationAuditLog)
|
|
])
|
|
/\ UNCHANGED <<userLevels, userTenants, webhookConfigs, webhookQueue,
|
|
webhookDeliveries, oauthTokens, apiKeys, apiCallCounts,
|
|
eventSubscriptions>>
|
|
|
|
\* User authorizes OAuth app
|
|
AuthorizeOAuthApp(user, appId, tokenId, scopes) ==
|
|
/\ \E app \in oauthApps :
|
|
/\ app.id = appId
|
|
/\ userTenants[user] = app.tenantId
|
|
/\ app.status = "active"
|
|
/\ scopes \subseteq app.scopes
|
|
/\ tokenId \notin {t.id : t \in oauthTokens}
|
|
/\ LET
|
|
currentTime == Len(integrationAuditLog)
|
|
newToken == [
|
|
id |-> tokenId,
|
|
appId |-> appId,
|
|
userId |-> user,
|
|
tenantId |-> userTenants[user],
|
|
accessToken |-> "token_" \o tokenId,
|
|
scopes |-> scopes,
|
|
expiresAt |-> currentTime + 3600,
|
|
createdAt |-> currentTime
|
|
]
|
|
IN
|
|
/\ oauthTokens' = oauthTokens \cup {newToken}
|
|
/\ integrationAuditLog' = Append(integrationAuditLog, [
|
|
user |-> user,
|
|
action |-> "authorize_oauth_app",
|
|
targetId |-> appId,
|
|
tenant |-> userTenants[user],
|
|
timestamp |-> currentTime
|
|
])
|
|
/\ UNCHANGED <<userLevels, userTenants, webhookConfigs, webhookQueue,
|
|
webhookDeliveries, oauthApps, apiKeys, apiCallCounts,
|
|
eventSubscriptions>>
|
|
|
|
\* Admin revokes OAuth app
|
|
RevokeOAuthApp(user, appId) ==
|
|
/\ \E app \in oauthApps :
|
|
/\ app.id = appId
|
|
/\ CanManageIntegrations(user, app.tenantId)
|
|
/\ app.status /= "revoked"
|
|
/\ oauthApps' = (oauthApps \ {app}) \cup
|
|
{[app EXCEPT !.status = "revoked"]}
|
|
/\ integrationAuditLog' = Append(integrationAuditLog, [
|
|
user |-> user,
|
|
action |-> "revoke_oauth_app",
|
|
targetId |-> appId,
|
|
tenant |-> app.tenantId,
|
|
timestamp |-> Len(integrationAuditLog)
|
|
])
|
|
/\ UNCHANGED <<userLevels, userTenants, webhookConfigs, webhookQueue,
|
|
webhookDeliveries, oauthTokens, apiKeys, apiCallCounts,
|
|
eventSubscriptions>>
|
|
|
|
-----------------------------------------------------------------------------
|
|
(* API Key Management *)
|
|
|
|
\* User creates API key
|
|
CreateAPIKey(user, keyId, name, scopes, expiresAt) ==
|
|
/\ CanManageAPIKeys(user)
|
|
/\ keyId \in APIKeys
|
|
/\ keyId \notin {k.id : k \in apiKeys}
|
|
/\ CountKeysForUser(user) < MaxKeysPerUser
|
|
/\ LET newKey == [
|
|
id |-> keyId,
|
|
userId |-> user,
|
|
tenantId |-> userTenants[user],
|
|
name |-> name,
|
|
key |-> "key_" \o keyId,
|
|
status |-> "active",
|
|
scopes |-> scopes,
|
|
expiresAt |-> expiresAt,
|
|
createdAt |-> Len(integrationAuditLog)
|
|
] IN
|
|
/\ apiKeys' = apiKeys \cup {newKey}
|
|
/\ integrationAuditLog' = Append(integrationAuditLog, [
|
|
user |-> user,
|
|
action |-> "create_api_key",
|
|
targetId |-> keyId,
|
|
tenant |-> userTenants[user],
|
|
timestamp |-> Len(integrationAuditLog)
|
|
])
|
|
/\ UNCHANGED <<userLevels, userTenants, webhookConfigs, webhookQueue,
|
|
webhookDeliveries, oauthApps, oauthTokens, apiCallCounts,
|
|
eventSubscriptions>>
|
|
|
|
\* User revokes API key
|
|
RevokeAPIKey(user, keyId) ==
|
|
/\ \E key \in apiKeys :
|
|
/\ key.id = keyId
|
|
/\ key.userId = user
|
|
/\ key.status = "active"
|
|
/\ apiKeys' = (apiKeys \ {key}) \cup
|
|
{[key EXCEPT !.status = "revoked"]}
|
|
/\ integrationAuditLog' = Append(integrationAuditLog, [
|
|
user |-> user,
|
|
action |-> "revoke_api_key",
|
|
targetId |-> keyId,
|
|
tenant |-> userTenants[user],
|
|
timestamp |-> Len(integrationAuditLog)
|
|
])
|
|
/\ UNCHANGED <<userLevels, userTenants, webhookConfigs, webhookQueue,
|
|
webhookDeliveries, oauthApps, oauthTokens, apiCallCounts,
|
|
eventSubscriptions>>
|
|
|
|
\* System expires old API keys
|
|
ExpireAPIKey(keyId) ==
|
|
/\ \E key \in apiKeys :
|
|
/\ key.id = keyId
|
|
/\ key.status = "active"
|
|
/\ Len(integrationAuditLog) >= key.expiresAt
|
|
/\ apiKeys' = (apiKeys \ {key}) \cup
|
|
{[key EXCEPT !.status = "expired"]}
|
|
/\ UNCHANGED <<userLevels, userTenants, webhookConfigs, webhookQueue,
|
|
webhookDeliveries, oauthApps, oauthTokens, apiCallCounts,
|
|
eventSubscriptions, integrationAuditLog>>
|
|
|
|
-----------------------------------------------------------------------------
|
|
(* Rate Limiting *)
|
|
|
|
\* Record API call
|
|
RecordAPICall(identity, hour) ==
|
|
/\ ~RateLimitExceeded(identity, hour)
|
|
/\ apiCallCounts' = [apiCallCounts EXCEPT
|
|
![<<identity, hour>>] = @ + 1]
|
|
/\ UNCHANGED <<userLevels, userTenants, webhookConfigs, webhookQueue,
|
|
webhookDeliveries, oauthApps, oauthTokens, apiKeys,
|
|
eventSubscriptions, integrationAuditLog>>
|
|
|
|
-----------------------------------------------------------------------------
|
|
(* Event Subscriptions *)
|
|
|
|
\* Create event subscription
|
|
SubscribeToEvent(user, subId, eventType, filters) ==
|
|
/\ CanManageIntegrations(user, userTenants[user])
|
|
/\ subId \notin {s.id : s \in eventSubscriptions}
|
|
/\ eventType \in EventTypes
|
|
/\ LET newSub == [
|
|
id |-> subId,
|
|
subscriberId |-> user,
|
|
tenantId |-> userTenants[user],
|
|
eventType |-> eventType,
|
|
filters |-> filters,
|
|
active |-> TRUE
|
|
] IN
|
|
/\ eventSubscriptions' = eventSubscriptions \cup {newSub}
|
|
/\ integrationAuditLog' = Append(integrationAuditLog, [
|
|
user |-> user,
|
|
action |-> "subscribe_event",
|
|
targetId |-> subId,
|
|
tenant |-> userTenants[user],
|
|
timestamp |-> Len(integrationAuditLog)
|
|
])
|
|
/\ UNCHANGED <<userLevels, userTenants, webhookConfigs, webhookQueue,
|
|
webhookDeliveries, oauthApps, oauthTokens, apiKeys,
|
|
apiCallCounts>>
|
|
|
|
\* Unsubscribe from event
|
|
UnsubscribeFromEvent(user, subId) ==
|
|
/\ \E sub \in eventSubscriptions :
|
|
/\ sub.id = subId
|
|
/\ sub.subscriberId = user
|
|
/\ CanManageIntegrations(user, sub.tenantId)
|
|
/\ eventSubscriptions' = (eventSubscriptions \ {sub}) \cup
|
|
{[sub EXCEPT !.active = FALSE]}
|
|
/\ integrationAuditLog' = Append(integrationAuditLog, [
|
|
user |-> user,
|
|
action |-> "unsubscribe_event",
|
|
targetId |-> subId,
|
|
tenant |-> sub.tenantId,
|
|
timestamp |-> Len(integrationAuditLog)
|
|
])
|
|
/\ UNCHANGED <<userLevels, userTenants, webhookConfigs, webhookQueue,
|
|
webhookDeliveries, oauthApps, oauthTokens, apiKeys,
|
|
apiCallCounts>>
|
|
|
|
-----------------------------------------------------------------------------
|
|
(* Next State Relation *)
|
|
|
|
Next ==
|
|
\/ \E u \in Users, wid \in Webhooks, url \in STRING,
|
|
events \in SUBSET EventTypes, secret \in STRING:
|
|
CreateWebhook(u, wid, url, events, secret)
|
|
\/ \E u \in Users, wid \in Webhooks, status \in WebhookStatus:
|
|
UpdateWebhookStatus(u, wid, status)
|
|
\/ \E wid \in Webhooks, et \in EventTypes, payload \in STRING, did \in Nat:
|
|
EnqueueWebhook(wid, et, payload, did)
|
|
\/ \E did \in Nat: AttemptDelivery(did)
|
|
\/ \E did \in Nat: FailDelivery(did)
|
|
\/ \E did \in Nat: PermanentFailDelivery(did)
|
|
\/ \E u \in Users, aid \in OAuthApps, name \in STRING,
|
|
scopes \in SUBSET STRING, uri \in STRING:
|
|
CreateOAuthApp(u, aid, name, scopes, uri)
|
|
\/ \E u \in Users, aid \in OAuthApps, tid \in Nat, scopes \in SUBSET STRING:
|
|
AuthorizeOAuthApp(u, aid, tid, scopes)
|
|
\/ \E u \in Users, aid \in OAuthApps: RevokeOAuthApp(u, aid)
|
|
\/ \E u \in Users, kid \in APIKeys, name \in STRING,
|
|
scopes \in SUBSET STRING, exp \in Nat:
|
|
CreateAPIKey(u, kid, name, scopes, exp)
|
|
\/ \E u \in Users, kid \in APIKeys: RevokeAPIKey(u, kid)
|
|
\/ \E kid \in APIKeys: ExpireAPIKey(kid)
|
|
\/ \E identity \in (Users \cup OAuthApps), hour \in Nat:
|
|
RecordAPICall(identity, hour)
|
|
\/ \E u \in Users, sid \in Nat, et \in EventTypes, f \in STRING:
|
|
SubscribeToEvent(u, sid, et, f)
|
|
\/ \E u \in Users, sid \in Nat: UnsubscribeFromEvent(u, sid)
|
|
|
|
-----------------------------------------------------------------------------
|
|
(* Safety Properties *)
|
|
|
|
\* Admin-only integration management
|
|
AdminOnlyIntegrationManagement ==
|
|
\A event \in 1..Len(integrationAuditLog):
|
|
LET action == integrationAuditLog[event].action IN
|
|
action \in {"create_webhook", "update_webhook_status",
|
|
"create_oauth_app", "revoke_oauth_app",
|
|
"subscribe_event", "unsubscribe_event"} =>
|
|
userLevels[integrationAuditLog[event].user] >= 4
|
|
|
|
\* Webhooks don't exceed tenant limit
|
|
WebhookTenantLimit ==
|
|
\A t \in Tenants:
|
|
CountWebhooksForTenant(t) <= MaxWebhooksPerTenant
|
|
|
|
\* API keys don't exceed user limit
|
|
APIKeyUserLimit ==
|
|
\A u \in Users:
|
|
CountKeysForUser(u) <= MaxKeysPerUser
|
|
|
|
\* Rate limits are enforced
|
|
RateLimitEnforcement ==
|
|
\A identity \in (Users \cup OAuthApps), hour \in Nat:
|
|
GetCallCount(identity, hour) <= RateLimitPerHour
|
|
|
|
\* Tenant isolation for webhooks
|
|
WebhookTenantIsolation ==
|
|
\A w \in webhookConfigs:
|
|
userTenants[w.ownerId] = w.tenantId
|
|
|
|
\* Tenant isolation for OAuth apps
|
|
OAuthAppTenantIsolation ==
|
|
\A app \in oauthApps:
|
|
userTenants[app.ownerId] = app.tenantId
|
|
|
|
\* Tenant isolation for API keys
|
|
APIKeyTenantIsolation ==
|
|
\A key \in apiKeys:
|
|
userTenants[key.userId] = key.tenantId
|
|
|
|
\* OAuth tokens match app tenants
|
|
TokenTenantConsistency ==
|
|
\A token \in oauthTokens:
|
|
\E app \in oauthApps:
|
|
app.id = token.appId /\ app.tenantId = token.tenantId
|
|
|
|
\* Active deliveries are in queue
|
|
ActiveDeliveriesQueued ==
|
|
\A d \in webhookDeliveries:
|
|
d.status = "pending" =>
|
|
\E i \in 1..Len(webhookQueue) : webhookQueue[i].id = d.id
|
|
|
|
-----------------------------------------------------------------------------
|
|
(* Liveness Properties *)
|
|
|
|
\* Webhook deliveries eventually complete or fail
|
|
EventualDeliveryCompletion ==
|
|
\A did \in Nat:
|
|
\E d \in webhookDeliveries :
|
|
d.id = did /\ d.status = "pending" ~>
|
|
d.status \in {"success", "failed"}
|
|
|
|
\* Failed deliveries eventually retry or permanently fail
|
|
EventualRetryOrFail ==
|
|
\A did \in Nat:
|
|
\E d \in webhookDeliveries :
|
|
d.id = did /\ d.status = "retrying" ~>
|
|
d.status \in {"success", "failed"}
|
|
|
|
\* Expired keys eventually get marked as expired
|
|
EventualExpiration ==
|
|
\A kid \in APIKeys:
|
|
\E key \in apiKeys :
|
|
key.id = kid /\ key.status = "active" /\
|
|
Len(integrationAuditLog) >= key.expiresAt ~>
|
|
key.status = "expired"
|
|
|
|
-----------------------------------------------------------------------------
|
|
(* System Specification *)
|
|
|
|
Spec ==
|
|
/\ Init
|
|
/\ [][Next]_vars
|
|
/\ \A did \in Nat: WF_vars(AttemptDelivery(did))
|
|
/\ \A kid \in APIKeys: WF_vars(ExpireAPIKey(kid))
|
|
|
|
-----------------------------------------------------------------------------
|
|
(* Invariants *)
|
|
|
|
Invariants ==
|
|
/\ TypeOK
|
|
/\ AdminOnlyIntegrationManagement
|
|
/\ WebhookTenantLimit
|
|
/\ APIKeyUserLimit
|
|
/\ RateLimitEnforcement
|
|
/\ WebhookTenantIsolation
|
|
/\ OAuthAppTenantIsolation
|
|
/\ APIKeyTenantIsolation
|
|
/\ TokenTenantConsistency
|
|
/\ ActiveDeliveriesQueued
|
|
|
|
=============================================================================
|