Formal verification for policy module: 2 bugs fixed, 44 Z3 proofs, 100% MC/DC

[buger]

Summary

This PR applies ReqProof formal verification to Tyk's policy engine (internal/policy/). ReqProof bridges natural-language requirements and mathematical proof: requirements are written in structured YAML with FRETish temporal logic formulas, then verified through a 6-layer chain -- Kind2 realizability, Z3 SMT proofs, MC/DC coverage, FLIP test fixtures, human-written tests, and bidirectional traceability.

The verification found and fixed 2 real bugs. Everything else is additive -- no behavioral changes to existing code beyond the nil guards.

Bugs Fixed

1. Nil store panic in Apply()

• What: Apply() dereferences the policy store without a nil check. If the store is nil (e.g., during gateway startup or after a failed initialization), this panics and crashes the gateway process.
• Fix: Added nil guard at the top of Apply() returning ErrNilPolicyStore sentinel error.
• Requirement: SYS-REQ-042 (store availability precondition)

2. Nil store panic in ClearSession()

• What: Same nil store dereference pattern in ClearSession().
• Fix: Added matching nil guard returning ErrNilPolicyStore.
• Requirement: SYS-REQ-042

Both bugs were discovered by writing requirements from intent (what the policy engine should guarantee) rather than from code (what it currently does). The spec-from-intent approach forces you to consider preconditions that the code silently assumes.

Formal Verification Coverage

Layer	Count	Details
Requirements	60	7 stakeholder (STK-REQ) + 53 system (SYS-REQ)
Z3 SMT proofs	44	23 data constraints + 19 merge algebra + 2 behavioral
MC/DC witness rows	111	0 uncovered across 29 formalized requirements
FLIP test fixtures	116	Propositional logic witnesses proving formula structure
Kind2 realizability	PASS	All 53 guarantees realizable
Kind2 consistency	PASS	0 conflicts across 630 requirement pairs
Kind2 vacuity	PASS	0/46 requirements vacuous
Obligation classes	7	nominal, error_handling, malformed_input, boundary, access_denied, policy_merge, rate_limit_boundary

What the Z3 proofs cover

• Merge algebra: highest-rate-wins for rate limits, quotas, complexity; set-union for tags; key-merge for metadata and access rights; special -1 (unlimited) sentinel handling
• Data constraints: boundary values (zero, negative, int64 max), empty rate guards, overlapping vs disjoint key sets
• Behavioral: error-success mutual exclusion, idle safety

Scoping

The verification_scope in proof.yaml restricts all analysis to internal/policy/**. This means the linter, traceability, and MC/DC checks operate only on the ~50 functions in the policy module -- not on the 8,000+ functions in the rest of the Tyk codebase. Zero noise.

Obligation Classes

Each stakeholder requirement declares an obligation checklist -- the behavioral cases that must be covered by child system requirements:

STK-REQ	Concern	Obligation Classes
STK-REQ-001	Policy application	nominal, error_handling, malformed_input, boundary, access_denied, policy_merge
STK-REQ-002	Session clearing	nominal, error_handling
STK-REQ-003	Rate limiting	nominal, rate_limit_boundary, error_handling, policy_merge
STK-REQ-004	Endpoint limits	nominal, rate_limit_boundary, policy_merge
STK-REQ-005	Error atomicity	nominal, error_handling, access_denied, malformed_input
STK-REQ-006	Idle safety	nominal, error_handling
STK-REQ-007	Performance	nominal

The obligation_completeness audit check verifies that every class in each checklist is covered by at least one child SYS-REQ with a matching obligation_class.

CI Integration

A GitHub Actions workflow (.github/workflows/reqproof.yml) runs proof audit on every PR touching the policy module, using probelabs/proof-action@v1. This prevents regressions in verification coverage.

Audit Result

```
Errors: 0 Warnings: 0
Assurance: 1 components (L3: 1)
```

All 60 requirements pass all quality gates across specification, implementation, verification, and documentation stages.

---

Generated with ReqProof formal verification toolchain.

[probelabs]

This pull request introduces a formal verification framework for the internal/policy module using the ReqProof toolchain. This is a significant, primarily additive change that defines stakeholder and system-level requirements in a verifiable format, backed by Z3 SMT proofs and an extensive new test suite designed to achieve 100% Modified Condition/Decision Coverage (MC/DC).

The verification process uncovered and fixed two critical nil-panic bugs in the policy engine that could crash the gateway. A new CI workflow is also added to continuously audit the policy module against its formal specification, preventing future regressions.

Bugs Fixed

1. Nil Store Panic in Apply(): A nil guard has been added to internal/policy/apply.go to prevent a panic when the policy store is unavailable, returning a new ErrNilPolicyStore error instead.
2. Nil Store Panic in ClearSession(): A similar nil guard was added to ClearSession() to handle cases where the policy store is nil.

Files Changed Analysis

• Total Changes: 30 files were changed, with 10,395 additions and 49 deletions. The vast majority of these changes are additive, introducing the formal verification framework, requirement specifications, and extensive tests.
• Production Code: The core logic changes are minimal and confined to internal/policy/apply.go, where nil guards were added to fix the two discovered bugs. Other minor changes include adding requirement trace comments (SYS-REQ-...) and small refactors.
• Formal Specification: A new specs/ directory contains stakeholder and system requirements in YAML format. These are governed by the new proof.yaml configuration file.
• Testing: Several large test files have been added (spec_test.go, mcdc_test.go, mcdc_closure_test.go, z3_spec_test.go), contributing thousands of lines of new test code. These tests are designed to provide evidence for the formal requirements and achieve 100% MC/DC for the policy module.
• CI/CD: A new GitHub Actions workflow (.github/workflows/reqproof.yml) is introduced to automate the formal verification audit on every pull request that modifies the policy module.

Architecture & Impact Assessment

• What this PR accomplishes: It significantly hardens the internal/policy module by applying formal verification methods. This not only fixes two critical stability bugs but also establishes a rigorous, verifiable specification for the policy engine's behavior, reducing the risk of future regressions in this security-critical component.

• Key technical changes introduced:

  1. Formal Verification Framework: Integrates the ReqProof toolchain, including formal requirement specifications (specs/), Z3 SMT proofs, and MC/DC analysis.
  2. Bug Fixes: Adds nil-pointer checks in Apply() and ClearSession() to prevent gateway crashes when the policy store is unavailable.
  3. Comprehensive Testing: Introduces property-based tests, MC/DC closure tests, and specification-driven tests, dramatically increasing test coverage and confidence in the policy engine's correctness.
  4. CI Automation: A new workflow ensures that the formal specification and the implementation do not diverge over time.

• Affected system components: The primary component is the internal/policy engine. However, the bug fixes have a system-wide impact on stability. A panic in the policy engine could crash the entire Tyk gateway process, so these fixes improve the resilience of the gateway's data plane.

Formal Verification Flow

graph TD
    A[Formal Requirements<br>specs/**/*.req.yaml] -->|ReqProof Toolchain| B(Verified Spec & Test Fixtures)
    C[Policy Engine Code<br>internal/policy/*.go] -->|Executed by| D{New Go Tests}
    B -->|Consumed by| D
    D -->|Verifies| C
    D -->|Produces| E[Test Results & 100% MC/DC]

Loading

Scope Discovery & Context Expansion

• Broader Impact: While the code changes are scoped to internal/policy, the impact is global for the gateway. The policy engine is on the critical path for every authenticated API request. The bug fixes in apply.go prevent the gateway from crashing if its policy store (e.g., Redis) is unavailable during startup or becomes unavailable during operation, thus improving the overall stability and resilience of the data plane.

• Context from Related Files:

  • internal/policy/apply.go: The addition of ErrNilPolicyStore and the corresponding nil checks in Apply() and ClearSession() are the core fixes. The rest of the changes are comments and minor refactors to improve traceability to the new formal requirements.
  • internal/policy/*_test.go: The new test files are a comprehensive verification suite. mcdc_closure_test.go and mcdc_test.go are particularly important as they contain hundreds of targeted tests to satisfy every condition of every decision point in the policy engine's logic, achieving an exceptionally high level of test coverage.
  • specs/ & proof.yaml: These files represent the new "source of truth" for the policy engine's behavior. They formally document invariants and expected outcomes (e.g., merge algebra, error atomicity), which are then proven against the code.
  • .github/workflows/reqproof.yml: This file demonstrates the commitment to maintaining this high level of quality by integrating the verification process directly into the development lifecycle for any future changes to the policy module.

Metadata

• Review Effort: 5 / 5
• Primary Label: enhancement

---

Powered by Visor from Probelabs

Last updated: 2026-04-20T16:50:59.230Z | Triggered by: pr_updated | Commit: 8f0002f

💡 TIP: You can chat with Visor using /visor ask <your question>

[github-actions]

API Changes

--- prev.txt	2026-04-20 16:49:29.962209010 +0000
+++ current.txt	2026-04-20 16:49:22.431179715 +0000
@@ -7422,11 +7422,6 @@
 
 	// Controls which algorthm to use as a fallback when your distributed rate limiter can't be used.
 	DRLEnableSentinelRateLimiter bool `json:"drl_enable_sentinel_rate_limiter"`
-
-	// RateLimitResponseHeaders specifies the data source for rate limit headers in HTTP responses.
-	// This controls whether rate limit headers (X-RateLimit-Limit, X-RateLimit-Remaining, etc.)
-	// are populated from quota data or rate limit data. Valid values: "quotas", "rate_limits".
-	RateLimitResponseHeaders RateLimitSource `json:"rate_limit_response_headers"`
 }
     RateLimit contains flags and configuration for controlling rate limiting
     behaviour. It is embedded in the main config structure.
@@ -7434,12 +7429,6 @@
 func (r *RateLimit) String() string
     String returns a readable setting for the rate limiter in effect.
 
-type RateLimitSource string
-
-const (
-	SourceQuotas     RateLimitSource = "quotas"
-	SourceRateLimits RateLimitSource = "rate_limits"
-)
 type Reporter struct {
 	// URL connection url to the zipkin server
 	URL        string `json:"url"`
@@ -10209,8 +10198,6 @@
 	TimeStamp     int64
 }
 
-type CtxData = map[string]any
-
 type CustomMiddlewareResponseHook struct {
 	BaseTykResponseHandler
 	// Has unexported fields.
@@ -11752,8 +11739,7 @@
 	path string,
 	IP string,
 	r *http.Request,
-	session *user.SessionState,
-)
+	session *user.SessionState)
 
 func (k *OrganizationMonitor) EnabledForSpec() bool
 
@@ -11761,17 +11747,11 @@
 
 func (k *OrganizationMonitor) ProcessRequest(w http.ResponseWriter, r *http.Request, _ interface{}) (error, int)
 
-func (k *OrganizationMonitor) ProcessRequestLive(
-	r *http.Request,
-	orgSession *user.SessionState,
-) (error, int)
+func (k *OrganizationMonitor) ProcessRequestLive(r *http.Request, orgSession *user.SessionState) (error, int)
     ProcessRequest will run any checks on the request on the way through the
     system, return an error to have the chain fail
 
-func (k *OrganizationMonitor) ProcessRequestOffThread(
-	r *http.Request,
-	orgSession *user.SessionState,
-) (error, int)
+func (k *OrganizationMonitor) ProcessRequestOffThread(r *http.Request, orgSession *user.SessionState) (error, int)
 
 func (k *OrganizationMonitor) SetOrgSentinel(orgChan chan bool, orgId string)
 
@@ -12033,7 +12013,7 @@
 
 func (k *RateLimitForAPI) Name() string
 
-func (k *RateLimitForAPI) ProcessRequest(rw http.ResponseWriter, r *http.Request, _ interface{}) (error, int)
+func (k *RateLimitForAPI) ProcessRequest(_ http.ResponseWriter, r *http.Request, _ interface{}) (error, int)
     ProcessRequest will run any checks on the request on the way through the
     system, return an error to have the chain fail
 
@@ -12594,12 +12574,7 @@
     SessionLimiter is the rate limiter for the API, use ForwardMessage() to
     check if a message should pass through or not
 
-func NewSessionLimiter(
-	ctx context.Context,
-	conf *config.Config,
-	drlManager *drl.DRL,
-	externalServicesConfig *config.ExternalServiceConfig,
-) SessionLimiter
+func NewSessionLimiter(ctx context.Context, conf *config.Config, drlManager *drl.DRL, externalServicesConfig *config.ExternalServiceConfig) SessionLimiter
     NewSessionLimiter initializes the session limiter.
 
     The session limiter initializes the storage required for rate limiters.
@@ -12615,10 +12590,10 @@
 	session *user.SessionState,
 	rateLimitKey string,
 	quotaKey string,
+	store storage.Handler,
 	enableRL, enableQ bool,
 	api *APISpec,
 	dryRun bool,
-	headerSender rate.HeaderSender,
 ) sessionFailReason
     ForwardMessage will enforce rate limiting, returning a non-zero
     sessionFailReason if session limits have been exceeded. Key values to manage
@@ -12626,14 +12601,7 @@
 
 func (l *SessionLimiter) RateLimitInfo(r *http.Request, api *APISpec, endpoints user.Endpoints) (*user.EndpointRateLimitInfo, bool)
 
-func (l *SessionLimiter) RedisQuotaExceeded(
-	r *http.Request,
-	session *user.SessionState,
-	quotaKey, scope string,
-	limit *user.APILimit,
-	hashKeys bool,
-	enableCtxVars bool,
-) bool
+func (l *SessionLimiter) RedisQuotaExceeded(r *http.Request, session *user.SessionState, quotaKey, scope string, limit *user.APILimit, store storage.Handler, hashKeys bool) bool
     RedisQuotaExceeded returns true if the request should be blocked as over
     quota.
 
@@ -13330,14 +13298,9 @@
     upgrade and websocket
 
 const (
-	// XRateLimitLimit The maximum number of requests that the client is allowed to make in a given time period
-	XRateLimitLimit = "X-RateLimit-Limit"
-
-	// XRateLimitRemaining The number of requests remaining in the current rate limit window.
+	XRateLimitLimit     = "X-RateLimit-Limit"
 	XRateLimitRemaining = "X-RateLimit-Remaining"
-
-	// XRateLimitReset The number of seconds until the rate limit resets.
-	XRateLimitReset = "X-RateLimit-Reset"
+	XRateLimitReset     = "X-RateLimit-Reset"
 )
     Gateway's custom response headers
 

[probelabs]

Security Issues (1)

Severity	Location	Issue
🟡 Warning	.claude/settings.local.json:1-52	A highly permissive configuration file for a development tool has been added to the repository. This file grants broad shell access, including commands like `rm:*`, `bash:*`, and `curl:*`. Committing such a file is risky as it could be misused by a compromised developer account or if the tool is used in a shared or CI environment. Local configuration files should typically not be version-controlled. 💡 Suggestion The file `.claude/settings.local.json` should be removed from the repository and added to `.gitignore`. If a template is needed for developers, it should be provided with secure defaults and clear instructions not to commit personal or overly permissive versions.

Security Issues (1)

Severity	Location	Issue
🟡 Warning	.claude/settings.local.json:1-52	A highly permissive configuration file for a development tool has been added to the repository. This file grants broad shell access, including commands like `rm:*`, `bash:*`, and `curl:*`. Committing such a file is risky as it could be misused by a compromised developer account or if the tool is used in a shared or CI environment. Local configuration files should typically not be version-controlled. 💡 Suggestion The file `.claude/settings.local.json` should be removed from the repository and added to `.gitignore`. If a template is needed for developers, it should be provided with secure defaults and clear instructions not to commit personal or overly permissive versions.

\n\n ### Architecture Issues (1)

Severity	Location	Issue
🟠 Error	internal/policy/apply.go:98-102	The `Apply` function treats an error from `ClearSession` as a non-fatal warning and continues execution. A failure in `ClearSession` (e.g., due to the newly handled `ErrNilPolicyStore`) means that stale rate limit, quota, or complexity values may remain in the session. This can lead to incorrect policy enforcement, as a new, more restrictive policy might not be applied because the pre-existing, less restrictive values were not cleared. This violates the atomicity of the policy application process. 💡 Suggestion To ensure policy correctness, the `Apply` function should fail fast. If `ClearSession` returns an error, `Apply` should propagate that error immediately instead of just logging it. This would prevent the application of policies to a potentially inconsistent session state.

Performance Issues (1)

Severity	Location	Issue
🟡 Warning	internal/policy/apply.go:422-435	The logic for merging `RestrictedTypes` within the `applyPartitions` function uses a nested loop, resulting in O(N*M) time complexity, where N is the number of types in the session-so-far and M is the number of types in the policy being applied. This can be inefficient if an API has a large number of GraphQL types defined in its access rights across multiple policies. A similar inefficient loop exists for merging `AllowedTypes` starting at line 449. 💡 Suggestion To optimize the merge operation, convert the slice of types into a map before the loop for O(1) lookups. This would reduce the overall complexity from O(N*M) to O(N+M). Example for RestrictedTypes: // Before line 422 restrictedTypesMap := make(map[string]*graphql.Type, len(r.RestrictedTypes)) for i := range r.RestrictedTypes { restrictedTypesMap[r.RestrictedTypes[i].Name] = &r.RestrictedTypes[i] } for _, rt := range v.RestrictedTypes { if existing, ok := restrictedTypesMap[rt.Name]; ok { existing.Fields = appendIfMissing(existing.Fields, rt.Fields...) } else { newType := rt r.RestrictedTypes = append(r.RestrictedTypes, newType) restrictedTypesMap[newType.Name] = &r.RestrictedTypes[len(r.RestrictedTypes)-1] } }

Quality Issues (1)

Severity	Location	Issue
🟡 Warning	internal/policy/spec_test.go:720-803	Several property-based tests like `TestProperty_Quota_HighestWins`, `TestProperty_Metadata_CombineByKey` (line 957), and `TestProperty_ClearSession_PartitionBehavior` (line 1123) contain significant boilerplate repetition across their sub-tests (`t.Run`). Each sub-test re-initializes similar policy and session objects, making the tests verbose and harder to maintain or extend with new cases. 💡 Suggestion Refactor these tests to use a table-driven approach. A slice of structs can define the test cases (inputs and expected outputs), and a single loop can iterate over them, running each as a sub-test. This will centralize the setup logic, reduce code duplication, and make it easier to add new test cases. For example, `TestProperty_Quota_HighestWins` could be refactored to iterate over a slice of test cases, each defining the quotas for two policies and the expected merged quota.

---

Powered by Visor from Probelabs

Last updated: 2026-04-20T16:49:37.530Z | Triggered by: pr_updated | Commit: 8f0002f

💡 TIP: You can chat with Visor using /visor ask <your question>

[github-actions]

🚨 Jira Linter Failed

Commit: 8f0002f
Failed at: 2026-04-20 16:48:24 UTC

The Jira linter failed to validate your PR. Please check the error details below:

🔍 Click to view error details

failed to validate branch and PR title rules: branch name 'experiment/formal-requirements-policy' must contain a valid Jira ticket ID (e.g., ABC-123)

Next Steps

• Ensure your branch name contains a valid Jira ticket ID (e.g., ABC-123)
• Verify your PR title matches the branch's Jira ticket ID
• Check that the Jira ticket exists and is accessible

---

This comment will be automatically deleted once the linter passes.

[sonarqubecloud]

Quality Gate failed

Failed conditions
1 Security Hotspot
75.8% Coverage on New Code (required ≥ 80%)
C Reliability Rating on New Code (required ≥ A)

See analysis details on SonarQube Cloud

Catch issues before they fail your Quality Gate with our IDE extension SonarQube for IDE