Skip to content

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

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
buger wants to merge 19 commits into
base: master
Choose a base branch
from
Open

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

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
19 commits
Select commit Hold shift + click to select a range
da0b4a7
experiment: formal requirements specification for internal/policy pac…
buger Mar 28, 2026
2cbc874
Add Z3 boundary test fixtures and refactor test suite
buger Mar 29, 2026
a35dd7f
Remove generated docs from PR
buger Mar 29, 2026
ab8e990
Polish test suite: remove redundancy, wire property fixtures, documen…
buger Mar 29, 2026
aeebbb5
Rename reqforge to reqproof across all spec files
buger Mar 29, 2026
8a9d851
Remove unused fixtures, add requirement traceability annotations
buger Mar 29, 2026
22b01c2
Remove meta-test TestZ3_FixturesExist
buger Mar 29, 2026
f281684
Complete formal verification: obligations, Z3, MC/DC, verification_scope
buger Apr 19, 2026
09e4eec
Push to L3 assurance: 99.5% coverage, 89.2%/91.3% MC/DC, all checks c…
buger Apr 19, 2026
b68c125
Remove generated artifacts from repo, add to .gitignore
buger Apr 19, 2026
5581e9c
Achieve L3 assurance with strict MC/DC: 100% code MC/DC, MCDC witness…
buger Apr 20, 2026
19f23df
L5 assurance: 100% MC/DC, 100% coverage, obligation checklists complete
buger Apr 20, 2026
dd1bebe
Add MCDC row witness annotations to all test files with Verifies links
buger Apr 20, 2026
05fdb3e
Enable test_mcdc_annotations check for strict MCDC enforcement
buger Apr 20, 2026
9984564
Remove fixture_evidence.components — fixtures not committed to repo
buger Apr 20, 2026
6dcd149
Adapt test helpers to PolicyID interface change from master
buger Apr 20, 2026
34e63d5
Update trace link reviews after rebase on master
buger Apr 20, 2026
5c6044f
Annotate and cover new MCP/policy code from main rebase
buger Apr 20, 2026
8f0002f
Remove Z3 fixtures from repo — generated artifacts
buger Apr 20, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
52 changes: 52 additions & 0 deletions .claude/settings.local.json
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,52 @@
{

Check warning on line 1 in .claude/settings.local.json

View check run for this annotation

probelabs / Visor: quality

undefined Issue 

This file appears to be a user-specific or tool-specific local configuration file (`settings.local.json`) that may not be intended for version control. Such files can introduce noise and potential conflicts if different developers have different local settings.
Raw output 
Consider adding `.claude/settings.local.json` to the root `.gitignore` file if it's not meant to be shared across all development environments. If it is intended to be shared, consider renaming it to remove the `.local` suffix to avoid confusion.
"permissions": {
"allow": [
"Bash(gh pr view:*)",
"Bash(chmod:*)",
"Bash(redis-cli:*)",
"Bash(./monitor-recovery-logs.sh:*)",
"Bash(timeout:*)",
"Bash(bash:*)",
"Bash(./continuous-load-test.sh:*)",
"Bash(curl:*)",
"Bash(pkill:*)",
"Bash(./run-all-tests.sh:*)",
"Bash(./test-network-failures.sh:*)",
"Bash(./test-nonce-recovery.sh:*)",
"Bash(rm:*)",
"Bash(brew list:*)",
"Bash(brew install:*)",
"Bash(go build:*)",
"Bash(./test-nonce-issue-demo.sh:*)",
"Bash(grep:*)",
"Bash(find:*)",
"Bash(go test:*)",
"Bash(git checkout:*)",
"Bash(git add:*)",
"Bash(git push:*)",
"Bash(gh pr checks:*)",
"Bash(gh run list:*)",
"WebFetch(domain:github.com)",
"Bash(git fetch:*)",
"Bash(gh api:*)",
"Bash(gh run view:*)",
"Bash(gh run view:*)",
"Bash(golangci-lint run:*)",
"Bash(git commit:*)",
"Bash(sed:*)",
"Bash(golangci-lint run:*)",
"Bash(go run:*)",
"Bash(git commit:*)",
"Bash(git pull:*)",
"Bash(git rebase:*)",
"Bash(gofmt:*)",
"Bash(git rm:*)",
"Bash(git stash:*)"
],
"deny": []
},
"enableAllProjectMcpServers": true,
"enabledMcpjsonServers": [
"big-brain"
]
}

Check warning on line 52 in .claude/settings.local.json

View check run for this annotation

probelabs / Visor: security

security Issue 

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.
Raw output 
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.
48 changes: 48 additions & 0 deletions .github/workflows/reqproof.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,48 @@
name: ReqProof Audit
on:
push:
branches: [main, experiment/formal-requirements-policy]
pull_request:
paths:
- 'internal/policy/**'
- 'specs/**'
- 'proof.yaml'

jobs:
audit:
runs-on: ubuntu-24.04
steps:
- uses: actions/checkout@v4
with:
fetch-depth: 0

- name: Set up Go
uses: actions/setup-go@v5
with:
go-version: '1.21'

- name: Install Z3 solver
run: sudo apt-get update -qq && sudo apt-get install -y -qq z3

- name: Cache ReqProof solvers
uses: actions/cache@v4
with:
path: ~/.proof/solvers
key: proof-solvers-${{ runner.os }}

- name: Cache ReqProof index
uses: actions/cache@v4
with:
path: |
.proof/index.db
.proof/index.db-shm
.proof/index.db-wal
key: proof-index-${{ runner.os }}-${{ hashFiles('specs/**/*.req.yaml') }}
restore-keys: |
proof-index-${{ runner.os }}-

- uses: probelabs/proof-action@v1
with:
fail-level: warn
scope: full
format: markdown
7 changes: 7 additions & 0 deletions .gitignore
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -92,3 +92,10 @@ ci/tests/specs/policies
# unknown json files
/gateway/test.json
/gateway/child-v1.json

# ReqProof generated artifacts
.proof/
tests/policy/properties/
tests/policy/tc-*.json
tests/policy/z3-*.json
tests/policy/z3-fixtures/
3 changes: 3 additions & 0 deletions .reqproof/.gitignore
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
cache/
index.db
jobs/
74 changes: 51 additions & 23 deletions internal/policy/apply.go
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -14,6 +14,9 @@
var (
// ErrMixedPartitionAndPerAPIPolicies is the error to return when a mix of per api and partitioned policies are to be applied in a session.
ErrMixedPartitionAndPerAPIPolicies = errors.New("cannot apply multiple policies when some have per_api set and some are partitioned")

// ErrNilPolicyStore is returned when Apply or ClearSession is called with a nil policy store.
ErrNilPolicyStore = errors.New("policy store is nil")
)

// Service represents the implementation for apply policies logic.
Expand All @@ -25,6 +28,7 @@
orgID *string
}

// SYS-REQ-008, SYS-REQ-042
func New(orgID *string, storage model.PolicyProvider, logger *logrus.Logger) *Service {
return &Service{
orgID: orgID,
Expand All @@ -33,9 +37,13 @@
}
}

// SYS-REQ-019, SYS-REQ-020, SYS-REQ-049
// ClearSession clears the quota, rate limit and complexity values so that partitioned policies can apply their values.
// Otherwise, if the session has already a higher value, an applied policy will not win, and its values will be ignored.
func (t *Service) ClearSession(session *user.SessionState) error {
if t.storage == nil {
return ErrNilPolicyStore
}

for _, polID := range t.policyIds(session) {
policy, ok := t.storage.PolicyByID(polID)
Expand Down Expand Up @@ -76,6 +84,9 @@
didPartition bool
}

// SYS-REQ-008, SYS-REQ-010, SYS-REQ-011, SYS-REQ-012, SYS-REQ-013, SYS-REQ-014, SYS-REQ-015, SYS-REQ-016, SYS-REQ-017, SYS-REQ-018
// SYS-REQ-024, SYS-REQ-025, SYS-REQ-026, SYS-REQ-027, SYS-REQ-028, SYS-REQ-029, SYS-REQ-030, SYS-REQ-031, SYS-REQ-032, SYS-REQ-033
// SYS-REQ-040, SYS-REQ-042, SYS-REQ-043, SYS-REQ-044, SYS-REQ-050, SYS-REQ-052, SYS-REQ-053, SYS-REQ-054
// Apply will check if any policies are loaded. If any are, it
// will overwrite the session state to use the policy values.
func (t *Service) Apply(session *user.SessionState) error {
Expand All @@ -84,9 +95,11 @@
if session.MetaData == nil {
session.MetaData = make(map[string]interface{})
}

if err := t.ClearSession(session); err != nil {
t.logger.WithError(err).Warn("error clearing session")
if t.logger != nil {
t.logger.WithError(err).Warn("error clearing session")
}

Check failure on line 102 in internal/policy/apply.go

View check run for this annotation

probelabs / Visor: architecture

architecture Issue 

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.
Raw output 
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.
}

applyState := applyStatus{
Expand All @@ -105,6 +118,10 @@
storage = NewStore(customPolicies)
policyIDs = storage.PolicyIDs()
} else {
// No custom policies; storage must be available.
if t.storage == nil {
return ErrNilPolicyStore
}
policyIDs = t.policyIds(session)
}

Expand Down Expand Up @@ -230,9 +247,11 @@
v.Limit.QuotaRenews = session.QuotaRenews
}

// If multime ACL
// If multiple ACLs from different policies, set AllowanceScope from SetBy.
// SetBy is always non-empty here: every API that passes the didAcl
// check above had SetBy assigned during partition/perAPI processing.
if len(distinctACL) > 1 {
if v.AllowanceScope == "" && v.Limit.SetBy != "" {
if v.AllowanceScope == "" {
v.AllowanceScope = v.Limit.SetBy
}
}
Expand All @@ -257,11 +276,13 @@
return nil
}

// SYS-REQ-008
// Logger implements a typical logger signature with service context.
func (t *Service) Logger() *logrus.Entry {
return logrus.NewEntry(t.logger)
}

// SYS-REQ-021, SYS-REQ-022, SYS-REQ-041, SYS-REQ-051
// ApplyRateLimits will write policy limits to session and apiLimits.
// The limits get written if either are empty.
// The limits get written if filled and policyLimits allows a higher request rate.
Expand Down Expand Up @@ -299,10 +320,12 @@
}
}

// SYS-REQ-021
func (t *Service) emptyRateLimit(m user.APILimit) bool {
return m.Rate == 0 || m.Per == 0
}

// SYS-REQ-013, SYS-REQ-014, SYS-REQ-015
func (t *Service) applyPerAPI(policy user.Policy, session *user.SessionState, rights map[string]user.AccessDefinition,
applyState *applyStatus) error {

Expand Down Expand Up @@ -355,6 +378,7 @@
return nil
}

// SYS-REQ-008, SYS-REQ-033
func (t *Service) policyIds(session *user.SessionState) []model.PolicyID {
ids := session.PolicyIDs()

Expand All @@ -373,6 +397,7 @@
}
}

// SYS-REQ-030, SYS-REQ-031, SYS-REQ-032
func (t *Service) applyPartitions(policy user.Policy, session *user.SessionState, rights map[string]user.AccessDefinition,
applyState *applyStatus) error {

Expand All @@ -394,17 +419,20 @@

for k, v := range policy.AccessRights {
// Use rights[k], which holds previously seen/merged policy access rights.
ar := rights[k]

if !usePartitions || policy.Partitions.Acl {
applyState.didAcl[k] = true

// Merge ACLs for the same API
if r, ok := rights[k]; ok {
// Merge ACLs for the same API.
// rights[k] is guaranteed to exist: the pre-fill loop above (lines 382-387)
// ensures every key in policy.AccessRights is present in rights.
{
r := rights[k]
// If GQL introspection is disabled, keep that configuration.
if v.DisableIntrospection {
r.DisableIntrospection = v.DisableIntrospection
}

Check warning on line 435 in internal/policy/apply.go

View check run for this annotation

probelabs / Visor: performance

performance Issue 

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.
Raw output 
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`:

```go
// 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]
	}
}
```
r.Versions = appendIfMissing(rights[k].Versions, v.Versions...)

r.AllowedURLs = MergeAllowedURLs(r.AllowedURLs, v.AllowedURLs)
Expand Down Expand Up @@ -522,11 +550,11 @@

t.ApplyRateLimits(session, policy, &ar.Limit)

if rightsAR, ok := rights[k]; ok {
ar.Endpoints = t.ApplyEndpointLevelLimits(v.Endpoints, rightsAR.Endpoints)
ar.JSONRPCMethods = t.ApplyJSONRPCMethodLimits(v.JSONRPCMethods, rightsAR.JSONRPCMethods)
ar.MCPPrimitives = t.ApplyMCPPrimitiveLimits(v.MCPPrimitives, rightsAR.MCPPrimitives)
}
// rights[k] is guaranteed to exist (pre-filled above).
rightsAR := rights[k]
ar.Endpoints = t.ApplyEndpointLevelLimits(v.Endpoints, rightsAR.Endpoints)
ar.JSONRPCMethods = t.ApplyJSONRPCMethodLimits(v.JSONRPCMethods, rightsAR.JSONRPCMethods)
ar.MCPPrimitives = t.ApplyMCPPrimitiveLimits(v.MCPPrimitives, rightsAR.MCPPrimitives)

if policy.ThrottleRetryLimit > ar.Limit.ThrottleRetryLimit {
ar.Limit.ThrottleRetryLimit = policy.ThrottleRetryLimit
Expand Down Expand Up @@ -595,28 +623,24 @@
return nil
}

// SYS-REQ-024, SYS-REQ-025
func (t *Service) updateSessionRootVars(session *user.SessionState, rights map[string]user.AccessDefinition, applyState applyStatus) {
if len(applyState.didQuota) == 1 && len(applyState.didRateLimit) == 1 && len(applyState.didComplexity) == 1 {
for _, v := range rights {
if len(applyState.didRateLimit) == 1 {
session.Rate = v.Limit.Rate
session.Per = v.Limit.Per
session.Smoothing = v.Limit.Smoothing
}
session.Rate = v.Limit.Rate
session.Per = v.Limit.Per
session.Smoothing = v.Limit.Smoothing

if len(applyState.didQuota) == 1 {
session.QuotaMax = v.Limit.QuotaMax
session.QuotaRenews = v.Limit.QuotaRenews
session.QuotaRenewalRate = v.Limit.QuotaRenewalRate
}
session.QuotaMax = v.Limit.QuotaMax
session.QuotaRenews = v.Limit.QuotaRenews
session.QuotaRenewalRate = v.Limit.QuotaRenewalRate

if len(applyState.didComplexity) == 1 {
session.MaxQueryDepth = v.Limit.MaxQueryDepth
}
session.MaxQueryDepth = v.Limit.MaxQueryDepth
}
}
}

// SYS-REQ-023
func (t *Service) applyAPILevelLimits(policyAD user.AccessDefinition, currAD user.AccessDefinition) user.AccessDefinition {
var updated bool
if policyAD.Limit.Duration() > currAD.Limit.Duration() {
Expand Down Expand Up @@ -651,6 +675,7 @@
return policyAD
}

// SYS-REQ-023
// ApplyEndpointLevelLimits combines policyEndpoints and currEndpoints and returns the combined value.
// The returned endpoints would have the highest request rate from policyEndpoints and currEndpoints.
func (t *Service) ApplyEndpointLevelLimits(policyEndpoints user.Endpoints, currEndpoints user.Endpoints) user.Endpoints {
Expand Down Expand Up @@ -689,6 +714,7 @@
return result.Endpoints()
}

// SYS-REQ-023
// mergeACLRules merges two AccessControlRules using union semantics, consistent
// with how AllowedURLs are merged across policies: both Allowed and Blocked lists
// are unioned. If src is empty (not configured), dst is returned unchanged.
Expand All @@ -705,6 +731,7 @@
}
}

// SYS-REQ-023
// ApplyJSONRPCMethodLimits merges per-method rate limits: higher rate (lower duration) wins,
// matching the semantics of ApplyEndpointLevelLimits.
func (t *Service) ApplyJSONRPCMethodLimits(policy, current []user.JSONRPCMethodLimit) []user.JSONRPCMethodLimit {
Expand Down Expand Up @@ -737,6 +764,7 @@
return out
}

// SYS-REQ-023
// ApplyMCPPrimitiveLimits merges per-primitive rate limits keyed on type+name:
// higher rate (lower duration) wins, matching ApplyEndpointLevelLimits semantics.
func (t *Service) ApplyMCPPrimitiveLimits(policy, current []user.MCPPrimitiveLimit) []user.MCPPrimitiveLimit {
Expand Down
Loading
Loading