feat(policyimport): OPA Rego + Cedar → CEL translation layer (closes #282) - #284
Merged
Conversation
…282) Positions symkernel as a Z3-proof backend for teams already using OPA or Cedar: keep your existing Rego/Cedar policies, gain formal verification — no migration to a new policy language. New package internal/policyimport: - TranslateRego(src, ruleName) — parses a Rego module (opa/v1/ast, Rego v1 syntax), combines `allow` rules as a disjunction of conjoined body expressions, handles the default-deny idiom, emits CEL over `input`. - TranslateCedar(src) — parses a Cedar policy (cedar-go), walks the x/exp/ast node tree (scope constraints + when/unless conditions), emits CEL over principal/action/resource/context, carries permit/forbid Effect. - Both emit into the existing internal/cel substrate. Fail-closed by design: any construct not explicitly supported yields an *UnsupportedError with a precise Construct slug, never a best-effort guess — a silent mistranslation would let symkernel "prove" a property about a policy that does not match the source. Rejected: Rego user/unknown builtins, with, some/every, else, partial sets, non-input roots, default-true; Cedar like, extension calls, tags, isEmpty, is-in-condition, multi-policy docs. Tests prove semantic equivalence by evaluating the emitted CEL on symkernel's own cel.Evaluate across input matrices, plus fail-closed rejections. The worked example (worked_example_test.go) carries a Rego and a Cedar policy through CEL to a Z3-verified safety invariant (guard ∧ ¬invariant = unsat), skipping when z3 is absent. Docs: docs/opa-cedar-compat.md frames the position, the supported subset, the fail-closed boundary, and the Rego/Cedar → CEL → Z3 worked example. Verified: go build ./... , go vet, go test ./internal/policyimport/, golangci-lint (0 issues), staticcheck (clean), gofmt clean.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Positions symkernel as a Z3-proof backend for teams already using OPA or Cedar — keep your existing Rego/Cedar policies, gain formal verification, no migration to a new policy language.
What
New
internal/policyimportpackage with two entry points:TranslateRego(src, ruleName)— parses Rego (opa/v1/ast, Rego v1 syntax), combinesallowrules as a disjunction of conjoined body expressions, handles thedefault allow := falsedeny-by-default idiom, emits CEL overinput.TranslateCedar(src)— parses Cedar (cedar-go), walks thex/exp/astnode tree (scope constraints + when/unless), emits CEL overprincipal/action/resource/context, carries the permit/forbidEffect.Both emit into the existing
internal/celsubstrate — no new evaluation path, and coordinated with the criterion IR (no duplication ofinternal/cel/constraint work).Fail-closed by design
A silent mistranslation is worse than no translation: it would let symkernel prove a property about a policy that does not match the source. So every construct the translator does not explicitly understand yields an
*UnsupportedErrorwith a preciseConstructslug (e.g.rego.builtin:count,cedar.node:like) — never a best-effort guess. Seedocs/opa-cedar-compat.mdfor the full supported-subset / rejected-construct matrix.Provable — the point of the PR
worked_example_test.gocarries a Rego and a Cedar policy through CEL to a Z3-verified safety invariant: encode the policy guard + the negation of the invariant and checkunsat(no input both satisfies the policy and violates the property). e.g.allow if { input.age >= 18 }is proven to never admit an under-18 principal. Skips automatically when thez3binary is absent.Verification
go build ./...,go vet,go test ./internal/policyimport/(equivalence on the realcel.Evaluate+ fail-closed rejections + Z3 worked examples),golangci-lint(0 issues),staticcheck(clean),gofmtclean.Closes #282.