Skip to content
Open
Show file tree
Hide file tree
Changes from all commits
Commits
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
3 changes: 3 additions & 0 deletions cedar-policy-cli/CHANGELOG.md
Original file line number Diff line number Diff line change
Expand Up @@ -5,6 +5,9 @@ Changes to the Cedar language, which are likely to affect users of the CLI, are

## Unreleased

### Added
- `symcc` subcommand support for template-linked policies with the `--template-linked` option.

## 4.10.0

### Added
Expand Down
31 changes: 26 additions & 5 deletions cedar-policy-cli/src/command/symcc.rs
Original file line number Diff line number Diff line change
Expand Up @@ -21,7 +21,7 @@ use miette::{miette, Result};
use std::path::PathBuf;

use crate::CedarExitCode;
use crate::{read_cedar_policy_set, read_json_policy_set, PoliciesArgs};
use crate::{add_template_links_to_set, read_cedar_policy_set, read_json_policy_set, PoliciesArgs};
use crate::{PolicyFormat, SchemaArgs};

#[derive(Args, Debug)]
Expand Down Expand Up @@ -96,15 +96,22 @@ pub struct SymccPoliciesArgs {
/// Format of policies in the `--policies` file
#[arg(long = "policy-format", default_value_t, value_enum)]
pub policy_format: PolicyFormat,
/// File containing template-linked policies
#[arg(short = 'k', long = "template-linked", value_name = "FILE")]
pub template_linked_file: Option<String>,

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Do we need a separate SymccPoliciesArg now that it accepts templates links? I think I remember @katherine-hough duplicated in order to not accept templates here.

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

John is correct see: afae911

Copy link
Copy Markdown
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks, I should have remembered too.

}

impl SymccPoliciesArgs {
/// Turn this `SymccPoliciesArgs` into the appropriate `PolicySet` object
fn get_policy_set(&self) -> Result<PolicySet> {
match self.policy_format {
let mut pset = match self.policy_format {
PolicyFormat::Cedar => read_cedar_policy_set(self.policies_file.as_ref()),
PolicyFormat::Json => read_json_policy_set(self.policies_file.as_ref()),
}?;
if let Some(links_filename) = self.template_linked_file.as_ref() {
add_template_links_to_set(links_filename, &mut pset)?;
}
Ok(pset)
}
}

Expand All @@ -117,20 +124,26 @@ pub struct TwoPolicyArgs {
/// Format of the first policy file
#[arg(long = "policy1-format", default_value_t, value_enum)]
pub policy1_format: PolicyFormat,
/// File containing template-linked policies for the first policy
#[arg(long = "template-linked1", value_name = "FILE")]
pub template_linked1_file: Option<String>,
/// File containing the second Cedar policy
#[arg(long = "policy2", value_name = "FILE")]
pub policy2_file: Option<String>,
/// Format of the second policy file
#[arg(long = "policy2-format", default_value_t, value_enum)]
pub policy2_format: PolicyFormat,
/// File containing template-linked policies for the second policy
#[arg(long = "template-linked2", value_name = "FILE")]
pub template_linked2_file: Option<String>,
}

impl TwoPolicyArgs {
fn get_policy_set_1(&self) -> Result<PolicySet> {
let pargs = PoliciesArgs {
policies_file: self.policy1_file.clone(),
policy_format: self.policy1_format,
template_linked_file: None,
template_linked_file: self.template_linked1_file.clone(),
};
pargs.get_policy_set()
}
Expand All @@ -139,13 +152,13 @@ impl TwoPolicyArgs {
let pargs = PoliciesArgs {
policies_file: self.policy2_file.clone(),
policy_format: self.policy2_format,
template_linked_file: None,
template_linked_file: self.template_linked2_file.clone(),
};
pargs.get_policy_set()
}
}

/// Two policy-set comparison: policy set inputs without linked policies.
/// Two policy-set comparison: policy set inputs.
#[derive(Args, Debug)]
pub struct SymccTwoPoliciesArgs {
/// File containing the first policy set
Expand All @@ -154,19 +167,26 @@ pub struct SymccTwoPoliciesArgs {
/// Format of the first policy set file
#[arg(long = "policies1-format", default_value_t, value_enum)]
pub policies1_format: PolicyFormat,
/// File containing template-linked policies for the first policy set
#[arg(long = "template-linked1", value_name = "FILE")]
pub template_linked1_file: Option<String>,
/// File containing the second policy set
#[arg(long = "policies2", value_name = "FILE")]
pub policies2_file: Option<String>,
/// Format of the second policy set file
#[arg(long = "policies2-format", default_value_t, value_enum)]
pub policies2_format: PolicyFormat,
/// File containing template-linked policies for the second policy set
#[arg(long = "template-linked2", value_name = "FILE")]
pub template_linked2_file: Option<String>,
}

impl SymccTwoPoliciesArgs {
fn get_policy_set_1(&self) -> Result<PolicySet> {
let pargs = SymccPoliciesArgs {
policies_file: self.policies1_file.clone(),
policy_format: self.policies1_format,
template_linked_file: self.template_linked1_file.clone(),
};
pargs.get_policy_set()
}
Expand All @@ -175,6 +195,7 @@ impl SymccTwoPoliciesArgs {
let pargs = SymccPoliciesArgs {
policies_file: self.policies2_file.clone(),
policy_format: self.policies2_format,
template_linked_file: self.template_linked2_file.clone(),
};
pargs.get_policy_set()
}
Expand Down
108 changes: 108 additions & 0 deletions cedar-policy-cli/tests/symcc.rs
Original file line number Diff line number Diff line change
Expand Up @@ -1098,3 +1098,111 @@ fn test_equivalent_does_not_hold_no_counterexample() {
.stdout(predicates::str::contains("DOES NOT HOLD"))
.stdout(predicates::str::contains("Counterexample found").not());
}

// ---- Template-linked policy tests ----

#[test]
fn test_never_errors_with_template_linked_policy() {
let schema = write_temp(SAMPLE_SCHEMA);
let policy = write_temp(r#"permit(principal == ?principal, action, resource);"#);
let links = write_temp(
r#"[{"template_id": "policy0", "link_id": "link0", "args": {"?principal": "Identity::\"alice\""}}]"#,
);

cargo::cargo_bin_cmd!("cedar")
.arg("symcc")
.arg("--principal-type")
.arg("Identity")
.arg("--action")
.arg(r#"Action::"view""#)
.arg("--resource-type")
.arg("Thing")
.arg("--schema")
.arg(schema.path())
.arg("--schema-format")
.arg("cedar")
.arg("never-errors")
.arg("--policies")
.arg(policy.path())
.arg("--template-linked")
.arg(links.path())
.assert()
.success()
.stdout(predicates::str::contains("VERIFIED"));
}

#[test]
fn test_always_denies_with_template_linked_forbid() {
let schema = write_temp(SAMPLE_SCHEMA);
// A permit-all plus a linked forbid: should NOT always allow
let policy = write_temp(
r#"
permit(principal, action, resource);
forbid(principal == ?principal, action, resource);
"#,
);
let links = write_temp(
r#"[{"template_id": "policy1", "link_id": "link0", "args": {"?principal": "Identity::\"alice\""}}]"#,
);

cargo::cargo_bin_cmd!("cedar")
.arg("symcc")
.arg("--principal-type")
.arg("Identity")
.arg("--action")
.arg(r#"Action::"view""#)
.arg("--resource-type")
.arg("Thing")
.arg("--schema")
.arg(schema.path())
.arg("--schema-format")
.arg("cedar")
.arg("always-allows")
.arg("--policies")
.arg(policy.path())
.arg("--template-linked")
.arg(links.path())
.assert()
.success()
.stdout(predicates::str::contains("DOES NOT HOLD"));
}

#[test]
fn test_multiple_template_links() {
let schema = write_temp(SAMPLE_SCHEMA);
// One template linked twice with different principals.
// permit-all + two linked forbids: should NOT always allow.
let policy = write_temp(
r#"
permit(principal, action, resource);
forbid(principal == ?principal, action, resource);
"#,
);
let links = write_temp(
r#"[
{"template_id": "policy1", "link_id": "link0", "args": {"?principal": "Identity::\"alice\""}},
{"template_id": "policy1", "link_id": "link1", "args": {"?principal": "Identity::\"bob\""}}
]"#,
);

cargo::cargo_bin_cmd!("cedar")
.arg("symcc")
.arg("--principal-type")
.arg("Identity")
.arg("--action")
.arg(r#"Action::"view""#)
.arg("--resource-type")
.arg("Thing")
.arg("--schema")
.arg(schema.path())
.arg("--schema-format")
.arg("cedar")
.arg("always-allows")
.arg("--policies")
.arg(policy.path())
.arg("--template-linked")
.arg(links.path())
.assert()
.success()
.stdout(predicates::str::contains("DOES NOT HOLD"));
}
6 changes: 6 additions & 0 deletions cedar-policy-symcc/CHANGELOG.md
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,12 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
## [Unreleased]
Cedar Language Version: TBD

### Added

- Support for template-linked policies. `CompiledPolicy::compile` and
`CompiledPolicySet::compile` now resolve linked policies by inlining slot bindings
before typechecking and symbolic compilation.

## [0.4.0] - 2026-04-23
Cedar Language Version: 4.5

Expand Down
49 changes: 36 additions & 13 deletions cedar-policy-symcc/src/symcc.rs
Original file line number Diff line number Diff line change
Expand Up @@ -46,7 +46,7 @@ pub mod type_abbrevs;
pub mod verifier;

use cedar_policy::Schema;
use cedar_policy_core::ast::{Expr, ExprBuilder, Policy, PolicySet};
use cedar_policy_core::ast::{Expr, ExprBuilder, Policy, PolicySet, Template};
use cedar_policy_core::validator::{
typecheck::Typechecker, types::RequestEnv, ValidationMode, Validator,
};
Expand Down Expand Up @@ -645,8 +645,11 @@ pub fn well_typed_policy(
env: &cedar_policy::RequestEnv,
schema: &Schema,
) -> Result<Policy> {
let env = to_validator_request_env(env, schema.as_ref())
let mut env = to_validator_request_env(env, schema.as_ref())
.ok_or_else(|| Error::ActionNotInSchema(env.action().to_string()))?;
if !policy.is_static() {
env = env.link_slot_env(policy.env());
}
well_typed_policy_inner(policy, &env, schema)
}

Expand All @@ -655,16 +658,35 @@ fn well_typed_policy_inner(
env: &RequestEnv<'_>,
schema: &Schema,
) -> Result<Policy> {
// For linked policies, create a static equivalent by resolving slots in the

@john-h-kastner-aws john-h-kastner-aws May 6, 2026

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Could we change the model to match this? IIRC, the lean FFI layer currently does this, but it could make sense to handle this is the corresponding lean function

here, I think:

https://github.com/cedar-policy/cedar-spec/blob/92de50d691a8f59bc7bdfce37dd070e6d50a0b58/cedar-lean/Cedar/SymCC.lean#L58

might be a larger update than i'm thinking though

Copy link
Copy Markdown
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes the Lean FFI layer is currently doing the slot replacement.
I attempted changing that function in Lean, but it would be a large update. We can decide that it's necessary though.

Another difference between the Rust and Lean is that the Lean env doesn't get the extra information that the linked env in Rust passes. However, trying to integrate that alone in Lean doesn't seem trivial either.

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

If you have a decent idea of what would be needed, can you type up an issue on cedar-spec?

// scope constraints. This ensures the typechecked expression has no slots.
let template_for_tc;
let template_ref = if policy.is_static() {
policy.template()
} else {
template_for_tc = Template::new_shared(
policy.id().clone(),
policy.loc().cloned(),
policy.template().annotations_arc().clone(),
policy.effect(),
policy.principal_constraint(),
policy.template().action_constraint().clone(),
policy.resource_constraint(),
policy.non_scope_constraints_arc().cloned(),
);
&template_for_tc
};

let validator_schema = schema.as_ref();
// We need to perform these three checks like what the validator does here: https://github.com/cedar-policy/cedar/blob/82784864c01b5096cb73885dd2df5643074355ed/cedar-policy-core/src/validator.rs#L178-L185
// We don't need `validate_template_action_application` because existence of `env` already serves as evidence
let errs: Vec<_> =
Validator::validate_entity_types_and_literals(schema.as_ref(), policy.template()).collect();
Validator::validate_entity_types_and_literals(schema.as_ref(), template_ref).collect();
if !errs.is_empty() {
return Err(Error::PolicyNotWellTyped { errs });
}
let type_checker = Typechecker::new(validator_schema, ValidationMode::Strict);
let policy_check = type_checker.typecheck_by_single_request_env(policy.template(), env);
let policy_check = type_checker.typecheck_by_single_request_env(template_ref, env);

use cedar_policy_core::validator::typecheck::PolicyCheck::*;
match policy_check {
Expand Down Expand Up @@ -711,17 +733,18 @@ pub fn well_typed_policies(
env: &cedar_policy::RequestEnv,
schema: &Schema,
) -> Result<PolicySet> {
if policies.policies().any(|p| !p.is_static()) {
return Err(CompileError::UnsupportedFeature(
"template-linked policies are not supported".to_string(),
)
.into());
}
let env = to_validator_request_env(env, schema.as_ref())
let base_env = to_validator_request_env(env, schema.as_ref())
.ok_or_else(|| Error::ActionNotInSchema(env.action().to_string()))?;
let typed_policies: Result<Vec<Policy>> = policies
.static_policies()
.map(|p| well_typed_policy_inner(p, &env, schema))
.policies()
.map(|p| {
let linked_env = if p.is_static() {
base_env.clone()
} else {
base_env.clone().link_slot_env(p.env())
};
well_typed_policy_inner(p, &linked_env, schema)
})
.collect();
match typed_policies {
Ok(ps) => {
Expand Down
4 changes: 2 additions & 2 deletions cedar-policy-symcc/src/symcc/env.rs
Original file line number Diff line number Diff line change
Expand Up @@ -587,8 +587,8 @@ pub fn to_validator_request_env<'a>(
action,
resource,
context,
principal_slot: None,
resource_slot: None,
principal_slot: env.principal_slot().map(|s| s.as_ref().clone()),
resource_slot: env.resource_slot().map(|s| s.as_ref().clone()),
},
)
}
Loading
Loading