Skip to content

Fix soundness gaps for dyn-typed values in truncated containers #1279

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
copybara-service wants to merge 1 commit into
base: main
Choose a base branch
from
Open

Fix soundness gaps for dyn-typed values in truncated containers #1279

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
107 changes: 93 additions & 14 deletions verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -87,6 +87,7 @@ final class CelAstToZ3Translator {
private final CelZ3OperatorTranslator operatorTranslator;
private final Map<String, TranslatedValue> symbolTable;
private final Set<BoolExpr> typeConstraints;
private final Map<Expr<?>, CelType> inputVariableTypes;
private final ImmutableSet<String> unknownIdentifiers;
private final int comprehensionUnrollLimit;
private final CelTypeProvider typeProvider;
Expand Down Expand Up @@ -251,6 +252,7 @@ private TranslatedValue translateIdent(CelExpr celExpr, CelAbstractSyntaxTree as
name,
n -> {
Expr<?> v = ctx.mkConst(n, typeSystem.celValueSort());
inputVariableTypes.put(v, type);

// Variables at rest can never be pre-cooked Errors
// Basically prevents error being a counterexample of var == var
Expand Down Expand Up @@ -286,6 +288,7 @@ private TranslatedValue translateList(CelExpr celExpr, CelAbstractSyntaxTree ast
// check to a trivial identity check (e.g., `list_ref_0 == list_ref_0`).
if (listRef == null) {
SeqExpr seq = ctx.mkEmptySeq(ctx.mkSeqSort(typeSystem.celValueSort()));
List<Expr<?>> values = new ArrayList<>();
ImmutableList<Integer> optionalIndices = createList.optionalIndices();
ImmutableList<CelExpr> elements = createList.elements();
for (int i = 0; i < elements.size(); i++) {
Expand All @@ -299,19 +302,23 @@ private TranslatedValue translateList(CelExpr celExpr, CelAbstractSyntaxTree ast
elem = TranslatedValue.create(checkedValue, element, typeSystem, elem.isApproximate());

Expr<?> optRef = typeSystem.getOptionalRef(elem.z3Expr());
Expr<?> value = typeSystem.getOptionalValue(optRef);
seq =
(SeqExpr)
ctx.mkITE(
typeSystem.optHasValue(optRef),
typeSystem.mkConcatSafe(seq, ctx.mkUnit(typeSystem.getOptionalValue(optRef))),
typeSystem.mkConcatSafe(seq, ctx.mkUnit(value)),
seq);
values.add(value);
} else {
seq = typeSystem.mkConcatSafe(seq, ctx.mkUnit(elem.z3Expr()));
values.add(elem.z3Expr());
}
elementsTv.add(elem);
}
listRef = typeSystem.mkListRefConst(LIST_REF_PREFIX);
typeConstraints.add(ctx.mkEq(typeSystem.getSeq(listRef), seq));
propagateTruncatedTypeConstraint(typeSystem.wrapList(listRef), values);
Expr<?> finalListRef = listRef;
cacheKey.ifPresent(key -> listLiteralCache.put(key, finalListRef));
}
Expand All @@ -329,6 +336,7 @@ private TranslatedValue translateMap(CelExpr celExpr, CelAbstractSyntaxTree ast)
Expr<?> keysSeq = ctx.mkEmptySeq(ctx.mkSeqSort(typeSystem.celValueSort()));

List<TranslatedValue> elementsTv = new ArrayList<>();
List<Expr<?>> values = new ArrayList<>();

for (CelExpr.CelMap.Entry entryAst : createMap.entries()) {
TranslatedValue keyTv = translateExpr(entryAst.key(), ast);
Expand All @@ -350,6 +358,7 @@ private TranslatedValue translateMap(CelExpr celExpr, CelAbstractSyntaxTree ast)
finalValue = typeSystem.getOptionalValue(optRef);
}
elementsTv.add(valueTv);
values.add(finalValue);

BoolExpr keyAlreadyPresent = (BoolExpr) ctx.mkSelect(mapPresence, key);
BoolExpr shouldInsertKey = ctx.mkAnd(ctx.mkNot(keyAlreadyPresent), finalPresence);
Expand All @@ -368,9 +377,25 @@ private TranslatedValue translateMap(CelExpr celExpr, CelAbstractSyntaxTree ast)
typeConstraints.add(ctx.mkEq(typeSystem.getMapKeys(mapRef), keysSeq));

Expr<?> result = typeSystem.wrapMap(mapRef);
propagateTruncatedTypeConstraint(result, values);
return TranslatedValue.propagateStrict(ctx, typeSystem, result, celExpr, elementsTv);
}

/**
* Marks {@code container} as having a truncated type constraint if any of {@code elements} has
* one, unless it is an error or unknown: those are shared terms that hold no elements.
*/
private void propagateTruncatedTypeConstraint(Expr<?> container, Iterable<Expr<?>> elements) {
BoolExpr hasTruncated =
ctx.mkOr(
typeSystem.isErrorOrUnknown(container),
typeSystem.hasTruncatedTypeConstraint(container));
for (Expr<?> element : elements) {
typeConstraints.add(
ctx.mkImplies(typeSystem.hasTruncatedTypeConstraint(element), hasTruncated));
}
}

private TranslatedValue translateStruct(CelExpr celExpr, CelAbstractSyntaxTree ast) {
CelExpr.CelStruct createStruct = celExpr.struct();
if (isJsonWkt(createStruct.messageName())) {
Expand Down Expand Up @@ -673,8 +698,13 @@ private TranslatedValue translateSelect(CelExpr celExpr, CelAbstractSyntaxTree a

typeConstraints.add(createTypeConstraint(fieldAccess, exprId, ast));

return TranslatedValue.propagateStrict(
ctx, typeSystem, fieldAccess, celExpr, ImmutableList.of(operandTv));
TranslatedValue result =
TranslatedValue.propagateStrict(
ctx, typeSystem, fieldAccess, celExpr, ImmutableList.of(operandTv));
// Map presence is only linked to the keys up to the unroll limit.
return operandType.kind() == CelKind.STRUCT
? result
: result.withApproximation(operatorTranslator.isTruncatedMap(operand));
}

private TranslatedValue translateBlock(
Expand Down Expand Up @@ -710,7 +740,14 @@ private TranslatedValue translateCall(CelExpr expr, CelAbstractSyntaxTree ast) {

return operatorTranslator
.translateFunctionCall(functionName, args, exprId, ast)
.map(tv -> TranslatedValue.create(tv.z3Expr(), expr, typeSystem, tv.isApproximate()))
.map(
tv -> {
if (mayEmbedArgs(functionName, ast.getTypeOrThrow(exprId))) {
propagateTruncatedTypeConstraint(
tv.z3Expr(), Iterables.transform(args, TranslatedValue::z3Expr));
}
return TranslatedValue.create(tv.z3Expr(), expr, typeSystem, tv.isApproximate());
})
.orElseGet(
() -> {
// Uninterpreted function
Expand All @@ -732,6 +769,19 @@ private TranslatedValue translateCall(CelExpr expr, CelAbstractSyntaxTree ast) {
});
}

/**
* Whether a call may construct a container that embeds its args (e.g. list concatenation, map
* insertion or optional.of). Indexing and conditionals return existing values instead, so
* propagating to them would needlessly taint e.g. an element whenever its container has a
* truncated type constraint.
*/
private static boolean mayEmbedArgs(String functionName, CelType resultType) {
return (!CelZ3OperatorTranslator.isStaticallyKnown(resultType)
|| !resultType.parameters().isEmpty())
&& !functionName.equals(Operator.INDEX.getFunction())
&& !functionName.equals(Operator.CONDITIONAL.getFunction());
}

private <T> T withScope(String varName, TranslatedValue value, Supplier<T> action) {
TranslatedValue prev = symbolTable.put(varName, value);
try {
Expand Down Expand Up @@ -856,7 +906,8 @@ private TranslatedValue translateDynamicComprehension(
if (!isList && !isMap) {
BoolExpr isRuntimeListOrMap =
ctx.mkOr(typeSystem.isList(iterRange), typeSystem.isMap(iterRange));
Expr<?> result = ctx.mkITE(isRuntimeListOrMap, typeSystem.mkUnknown(), typeSystem.mkError());
Expr<?> result =
ctx.mkITE(isRuntimeListOrMap, mkParameterizedUnknown(celExpr, ast), typeSystem.mkError());
return TranslatedValue.create(result, celExpr, typeSystem, isRuntimeListOrMap);
}

Expand Down Expand Up @@ -1063,22 +1114,26 @@ private TranslatedValue unrollMapAndFilter(
Expr<?> iterRangeExpr = iterRangeTv.z3Expr();
BoolExpr rangeIsError = typeSystem.isError(iterRangeExpr);
BoolExpr rangeIsUnknown = typeSystem.isUnknown(iterRangeExpr);
BoolExpr isNotError = ctx.mkNot(typeSystem.isError(resultTv.z3Expr()));
BoolExpr shouldYieldUnknown = ctx.mkAnd(isTruncated, isNotError);

// TODO: Model the loop condition for custom macros; until then, abstract the
// result of any non-true condition, since the unrolled value ignores early exits.
BoolExpr isConditionUnmodeled = ctx.mkBool(!isLiteralTrue(comp.loopCondition()));
BoolExpr isAbstracted =
CelZ3TypeSystem.mkOrFlattened(ctx, rangeIsUnknown, isTruncated, isConditionUnmodeled);
// An error is not final when truncated: an unknown from a later iteration overrides it.
Expr<?> finalResult =
CelZ3TypeSystem.SwitchBuilder.newBuilder(ctx)
.addCase(rangeIsError, typeSystem.mkError())
.addCase(
ctx.mkOr(rangeIsUnknown, shouldYieldUnknown), mkParameterizedUnknown(celExpr, ast))
.addCase(isAbstracted, mkParameterizedUnknown(celExpr, ast))
.build(resultTv.z3Expr());

BoolExpr finalTaint =
(BoolExpr)
ctx.mkITE(
ctx.mkOr(rangeIsError, rangeIsUnknown),
iterRangeTv.isApproximate(),
CelZ3TypeSystem.mkOrFlattened(ctx, resultTv.isApproximate(), shouldYieldUnknown));
CelZ3TypeSystem.mkOrFlattened(
ctx, resultTv.isApproximate(), isTruncated, isConditionUnmodeled));

return TranslatedValue.create(finalResult, celExpr, typeSystem, finalTaint);
}
Expand Down Expand Up @@ -1200,6 +1255,11 @@ private static boolean isBooleanAccuInit(CelComprehension comp, boolean expected
&& comp.accuInit().constant().booleanValue() == expectedValue;
}

private static boolean isLiteralTrue(CelExpr expr) {
CelConstant constant = expr.constantOrDefault();
return constant.getKind() == CelConstant.Kind.BOOLEAN_VALUE && constant.booleanValue();
}

private static boolean isNotStrictlyFalseLoopCondition(CelComprehension comp, boolean expectNot) {
CelExpr.CelCall call = comp.loopCondition().callOrDefault();
if (!call.function().equals(Operator.NOT_STRICTLY_FALSE.getFunction())
Expand Down Expand Up @@ -1280,7 +1340,7 @@ private BoolExpr createTypeConstraintForType(Expr<?> val, CelType type) {
// Constrain list elements using bounded unrolling up to comprehensionUnrollLimit rather
// than Z3 forall quantifiers to prevent MBQI quantifier instantiation loops.
// Assert: isList(val) ∧ for all unrolled 0 <= i < length: ¬isError(seq[i]) ∧
// typeConstraint(seq[i])
// typeConstraint(seq[i]).
BoolExpr isList = typeSystem.isList(val);
CelType elemType = ((ListType) type).elemType();

Expand All @@ -1290,6 +1350,13 @@ private BoolExpr createTypeConstraintForType(Expr<?> val, CelType type) {

List<BoolExpr> boundsAndTypes = new ArrayList<>();
boundsAndTypes.add(isList);
// Elements beyond the limit are unconstrained, which only matters if elemType is known.
if (CelZ3OperatorTranslator.isStaticallyKnown(elemType)) {
boundsAndTypes.add(
ctx.mkImplies(
ctx.mkGt(length, ctx.mkInt(comprehensionUnrollLimit)),
typeSystem.hasTruncatedTypeConstraint(val)));
}
for (int i = 0; i < comprehensionUnrollLimit; i++) {
IntExpr idx = ctx.mkInt(i);
Expr elem = ctx.mkNth(seq, idx);
Expand Down Expand Up @@ -1323,6 +1390,14 @@ private BoolExpr createTypeConstraintForType(Expr<?> val, CelType type) {
List<BoolExpr> boundsAndTypes = new ArrayList<>();
boundsAndTypes.add(isMap);
boundsAndTypes.add(getBoundedMapBijection(mapPresence, seq, (ArithExpr) length));
// Entries beyond the limit are unconstrained, which matters if keyType or valType is known.
if (CelZ3OperatorTranslator.isStaticallyKnown(keyType)
|| CelZ3OperatorTranslator.isStaticallyKnown(valType)) {
boundsAndTypes.add(
ctx.mkImplies(
ctx.mkGt(length, ctx.mkInt(comprehensionUnrollLimit)),
typeSystem.hasTruncatedTypeConstraint(val)));
}

for (int i = 0; i < comprehensionUnrollLimit; i++) {
IntExpr idx = ctx.mkInt(i);
Expand Down Expand Up @@ -1400,25 +1475,29 @@ private Expr<?> mkParameterizedUnknown(CelExpr expr, CelAbstractSyntaxTree ast)
smtArgs.add(translateExpr(freeVar, ast).z3Expr());
}

return typeSystem.mkParameterizedUnknown(sig.staticHash(), smtArgs.build());
return typeSystem.mkParameterizedUnknown(
"!trunc_" + Long.toHexString(sig.staticHash()), smtArgs.build());
}

CelAstToZ3Translator(
Context ctx,
int comprehensionUnrollLimit,
ImmutableSet<String> unknownIdentifiers,
CelZ3FunctionRegistry functionRegistry,
CelTypeProvider typeProvider) {
CelTypeProvider typeProvider,
boolean parameterizeUnknowns) {
this.ctx = ctx;
this.comprehensionUnrollLimit = comprehensionUnrollLimit;
this.typeSystem = new CelZ3TypeSystem(ctx);
this.typeSystem = new CelZ3TypeSystem(ctx, parameterizeUnknowns);
this.typeConstraints = new LinkedHashSet<>();
this.inputVariableTypes = new HashMap<>();
this.operatorTranslator =
new CelZ3OperatorTranslator(
ctx,
typeSystem,
this.typeConstraints::add,
this::createTypeConstraintForType,
val -> inputVariableTypes.getOrDefault(val, SimpleType.DYN),
functionRegistry,
comprehensionUnrollLimit);
this.symbolTable = new HashMap<>();
Expand Down
33 changes: 22 additions & 11 deletions verifier/src/main/java/dev/cel/verifier/CelVerifierZ3Impl.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -192,16 +192,21 @@ public CelVerificationResult verifyEquivalence(
// Fall back to original ASTs if canonicalization or re-typechecking fails
}
try (Context ctx = new Context(ImmutableMap.of("model", "true"))) {
CelAstToZ3Translator translator =
new CelAstToZ3Translator(
ctx, comprehensionUnrollLimit, unknownIdentifiers, functionRegistry, typeProvider);
translator.getTypeSystem().enableParameterizedUnknownPropagation();
CelAstToZ3Translator translator = newTranslator(ctx, /* parameterizeUnknowns= */ true);

TranslatedValue tvA = translator.translate(astA);
TranslatedValue tvB = translator.translate(astB);

BoolExpr divergenceCondition = ctx.mkNot(ctx.mkEq(tvA.z3Expr(), tvB.z3Expr()));
BoolExpr combinedTaint = ctx.mkOr(tvA.isApproximate(), tvB.isApproximate());
// Parameterized unknowns are keyed on the operation producing them, whereas CEL identifies
// an unknown only by its attributes (e.g. `a && true` and `a` both yield unknown {a}). Two
// distinct unknowns may thus still be equivalent.
BoolExpr combinedTaint =
CelZ3TypeSystem.mkOrFlattened(
ctx,
tvA.isApproximate(),
tvB.isApproximate(),
ctx.mkAnd(tvA.isZ3Unknown(), tvB.isZ3Unknown()));

Solver solver = newSolver(ctx);
for (BoolExpr constraint : translator.getTypeConstraints()) {
Expand Down Expand Up @@ -273,9 +278,7 @@ CelVerificationResult verifyImplication(
}

try (Context ctx = new Context(ImmutableMap.of("model", "true"))) {
CelAstToZ3Translator translator =
new CelAstToZ3Translator(
ctx, comprehensionUnrollLimit, unknownIdentifiers, functionRegistry, typeProvider);
CelAstToZ3Translator translator = newTranslator(ctx, /* parameterizeUnknowns= */ false);

for (Map.Entry<String, CelAbstractSyntaxTree> entry : boundSymbols.entrySet()) {
TranslatedValue tv = translator.translate(entry.getValue());
Expand Down Expand Up @@ -350,9 +353,7 @@ CelVerificationResult verifyImplication(
private CelVerificationResult checkSatisfiability(
CelAbstractSyntaxTree ast, boolean searchForCounterexample) throws CelVerificationException {
try (Context ctx = new Context(ImmutableMap.of("model", "true"))) {
CelAstToZ3Translator translator =
new CelAstToZ3Translator(
ctx, comprehensionUnrollLimit, unknownIdentifiers, functionRegistry, typeProvider);
CelAstToZ3Translator translator = newTranslator(ctx, /* parameterizeUnknowns= */ false);

TranslatedValue tv = translator.translate(ast);
BoolExpr condition = translator.isTrue(tv.z3Expr());
Expand Down Expand Up @@ -502,6 +503,16 @@ private Solver newSolver(Context ctx) {
return solver;
}

private CelAstToZ3Translator newTranslator(Context ctx, boolean parameterizeUnknowns) {
return new CelAstToZ3Translator(
ctx,
comprehensionUnrollLimit,
unknownIdentifiers,
functionRegistry,
typeProvider,
parameterizeUnknowns);
}

private static String getCounterexampleString(
Context ctx,
CelZ3TypeSystem typeSystem,
Expand Down
Loading
Loading