diff --git a/src/analysis/souffle/operations.dl b/src/analysis/souffle/operations.dl index 37e493041..6345ccb77 100644 --- a/src/analysis/souffle/operations.dl +++ b/src/analysis/souffle/operations.dl @@ -29,7 +29,7 @@ .type OperandList = [ operand: AccessPath, next: OperandList ] // An Operation. -.type Operation = [owner: Principal, operator: Operator, result: AccessPath, +.type Operation = [actor: Principal, operator: Operator, result: AccessPath, operandList: OperandList, attributes: AttributeList] // Operation universe. @@ -45,28 +45,28 @@ .decl isAttributeList(attributeList: AttributeList) // Fill the appropriate universes with the pieces of the operation. -isPrincipal(owner), isOperator(operator), isAccessPath(result), +isPrincipal(actor), isOperator(operator), isAccessPath(result), isOperandList(operandList), isAttributeList(attributeList) :- -isOperation([owner, operator, result, operandList, attributeList]). +isOperation([actor, operator, result, operandList, attributeList]). // Declare mappings from an operation to its fields. .decl operationHasResult(operation: Operation, result: AccessPath) -.decl operationHasOwner(operation: Operation, owner: Principal) +.decl operationHasActor(operation: Operation, actor: Principal) .decl operationHasOperator(operation: Operation, operator: Operator) .decl operationHasOperandList(operation: Operation, operandList: OperandList) .decl operationHasAttributeList(operation: Operation, attributeList: AttributeList) // Populate field association relations. -operationHasResult(operation, result), operationHasOwner(operation, owner), +operationHasResult(operation, result), operationHasActor(operation, actor), operationHasOperator(operation, operator), operationHasOperandList(operation, operands), operationHasAttributeList(operation, attributes) :- - isPrincipal(owner), isOperator(operator), isAccessPath(result), isOperandList(operands), + isPrincipal(actor), isOperator(operator), isAccessPath(result), isOperandList(operands), isAttributeList(attributes), isOperation(operation), - operation = [owner, operator, result, operands, attributes]. + operation = [actor, operator, result, operands, attributes]. // BINARY_OPERATION is a convenience macro for the very-common-case of binary operations. -#define BINARY_OPERATION(owner, operator, result, attrs, input1, input2) \ -isOperation([owner, operator, result, [input1, [input2, nil]], attrs]) +#define BINARY_OPERATION(actor, operator, result, attrs, input1, input2) \ +isOperation([actor, operator, result, [input1, [input2, nil]], attrs]) // Explode the operand lists so that we can extract the heads of each sublist // to get a mapping from operations to their operands. diff --git a/src/analysis/souffle/tag_transforms.dl b/src/analysis/souffle/tag_transforms.dl index 0341a0c0b..f1d20152b 100644 --- a/src/analysis/souffle/tag_transforms.dl +++ b/src/analysis/souffle/tag_transforms.dl @@ -21,7 +21,7 @@ // Note: this will need to change when we integrate auth logic into the SQL // verifier. -#define DEFAULT_SQL_OWNER as("sql", Principal) +#define DEFAULT_SQL_ACTOR as("sql", Principal) #define TAG_TRANSFORM_OPERATOR as("sql.tag_transform", Operator) #define MERGE_OPERATOR as("sql.merge", Operator) #define TAG_TRANSFORM_RULE_NAME_ATTR "rule_name" @@ -98,14 +98,14 @@ isIntegrityTag(tag) :- sqlPolicyRuleNameHasResult(_, $AddIntegrityTag(tag)). .decl isTagTransformOperation(tagTransform: Operation) isTagTransformOperation( - [DEFAULT_SQL_OWNER, TAG_TRANSFORM_OPERATOR, result, operandList, attributes]) :- - isOperation([DEFAULT_SQL_OWNER, TAG_TRANSFORM_OPERATOR, result, operandList, attributes]). + [DEFAULT_SQL_ACTOR, TAG_TRANSFORM_OPERATOR, result, operandList, attributes]) :- + isOperation([DEFAULT_SQL_ACTOR, TAG_TRANSFORM_OPERATOR, result, operandList, attributes]). // A TagTransform operator propagates confidentiality tags and integrity tags // only from its direct input (its 0th input) to its output. It faithfully // propagates all integrity tags. This can be expressed by drawing a single // edge from the input to the output. -resolvedEdge(DEFAULT_SQL_OWNER, xformedInput, xformedOutput) :- +resolvedEdge(DEFAULT_SQL_ACTOR, xformedInput, xformedOutput) :- isTagTransformOperation(operation), operationHasOperandAtIndex(operation, xformedInput, 0), operationHasResult(operation, xformedOutput). @@ -138,7 +138,7 @@ allTagTransformPreconditionsLessThanIndexMet(op, 0) :- isTagTransformOperation(o allTagTransformPreconditionsLessThanIndexMet(op, idx + 1) :- isTagTransformOperation(op), tagTransformHasIndexedTagPrecondition(op, idx, [preconditionPath, requiredITag]), - mustHaveIntegrityTag(preconditionPath, DEFAULT_SQL_OWNER, requiredITag), + mustHaveIntegrityTag(preconditionPath, DEFAULT_SQL_ACTOR, requiredITag), allTagTransformPreconditionsLessThanIndexMet(op, idx). .decl allTagTransformPreconditionsMet(tagTransform: Operation) @@ -150,21 +150,21 @@ allTagTransformPreconditionsMet(tagTransform) :- policyRulePreconditionListLength(preconditionList, preconditionListLength), allTagTransformPreconditionsLessThanIndexMet(tagTransform, preconditionListLength). -removeTag(result, DEFAULT_SQL_OWNER, tag) :- +removeTag(result, DEFAULT_SQL_ACTOR, tag) :- isTagTransformOperation(op), operationHasResult(op, result), tagTransformHasRuleName(op, ruleName), allTagTransformPreconditionsMet(op), sqlPolicyRuleNameHasResult(ruleName, $RemoveConfidentialityTag(tag)). -hasTag(result, DEFAULT_SQL_OWNER, tag) :- +hasTag(result, DEFAULT_SQL_ACTOR, tag) :- isTagTransformOperation(op), operationHasResult(op, result), tagTransformHasRuleName(op, ruleName), allTagTransformPreconditionsMet(op), sqlPolicyRuleNameHasResult(ruleName, $AddConfidentialityTag(tag)). -mustHaveIntegrityTag(result, DEFAULT_SQL_OWNER, iTag) :- +mustHaveIntegrityTag(result, DEFAULT_SQL_ACTOR, iTag) :- isTagTransformOperation(op), operationHasResult(op, result), tagTransformHasRuleName(op, ruleName), @@ -212,11 +212,11 @@ isMergeOperationDirectInput(mergeOp, inputPath) :- // For the union rule, any itag on a direct input should propagate to the // output. -mustHaveIntegrityTag(result, DEFAULT_SQL_OWNER, iTag) :- +mustHaveIntegrityTag(result, DEFAULT_SQL_ACTOR, iTag) :- isModifiedPropagationMergeOp(mergeOp, RAKSHA_INTERNAL_UNION_ITAG_RULE_NAME), operationHasResult(mergeOp, result), isMergeOperationDirectInput(mergeOp, operand), - mustHaveIntegrityTag(operand, DEFAULT_SQL_OWNER, iTag). + mustHaveIntegrityTag(operand, DEFAULT_SQL_ACTOR, iTag). // For intersection, an integrity tag must be present on all direct inputs to be // placed upon the output. Use induction to check that it is present on all @@ -229,8 +229,8 @@ mergeOperationHasIntegrityTagOnDirectOperandsUpToIndex(mergeOp, integrityTag, 0) isMergeOp(mergeOp), isIntegrityTag(integrityTag), operationHasOperandAtIndex(mergeOp, operand, 0), isMergeOperationDirectInput(mergeOp, operand), - operationHasOwner(mergeOp, owner), - mustHaveIntegrityTag(operand, owner, integrityTag). + operationHasActor(mergeOp, actor), + mustHaveIntegrityTag(operand, actor, integrityTag). // Inductive case. mergeOperationHasIntegrityTagOnDirectOperandsUpToIndex(mergeOp, integrityTag, idx + 1) :- @@ -238,18 +238,18 @@ mergeOperationHasIntegrityTagOnDirectOperandsUpToIndex(mergeOp, integrityTag, id mergeOperationHasIntegrityTagOnDirectOperandsUpToIndex(mergeOp, integrityTag, idx), operationHasOperandAtIndex(mergeOp, operand, idx + 1), isMergeOperationDirectInput(mergeOp, operand), - operationHasOwner(mergeOp, owner), mustHaveIntegrityTag(operand, owner, integrityTag). + operationHasActor(mergeOp, actor), mustHaveIntegrityTag(operand, actor, integrityTag). // Propagate the integrity tag if the operation has INTERSECTION propagation // behavior and the integrity tag is present on all operands at indices up to // just under the control start index. -mustHaveIntegrityTag(result, owner, integTag) :- +mustHaveIntegrityTag(result, actor, integTag) :- isModifiedPropagationMergeOp(mergeOp, RAKSHA_INTERNAL_INTERSECT_ITAG_RULE_NAME), - isPrincipal(owner), isIntegrityTag(integTag), operationHasResult(mergeOp, result), + isPrincipal(actor), isIntegrityTag(integTag), operationHasResult(mergeOp, result), mergeOperationHasIntegrityTagOnDirectOperandsUpToIndex(mergeOp, integTag, idx), mergeOperationHasControlInputStartIndex(mergeOp, idx + 1). -#undef DEFAULT_SQL_OWNER +#undef DEFAULT_SQL_ACTOR #undef TAG_TRANSFORM_OPERATOR #undef TAG_TRANSFORM_RULE_NAME_ATTR diff --git a/src/analysis/souffle/tests/arcs_fact_tests/operation_field_unit_test.dl b/src/analysis/souffle/tests/arcs_fact_tests/operation_field_unit_test.dl index 871019e8f..a7391cd43 100644 --- a/src/analysis/souffle/tests/arcs_fact_tests/operation_field_unit_test.dl +++ b/src/analysis/souffle/tests/arcs_fact_tests/operation_field_unit_test.dl @@ -21,16 +21,16 @@ TEST_CASE(cat(test_name, cat("_", #relation))) :- \ count : { relation(operation, _) } = 1, relation(operation, expected) -#define CREATE_AND_TEST_OPERATOR_INNER(test_name, operation, owner, operator, result, operandList, attrList) \ +#define CREATE_AND_TEST_OPERATOR_INNER(test_name, operation, actor, operator, result, operandList, attrList) \ isOperation(operation). \ - TEST_SINGLE_RESULT_FOR_OPERATION(test_name, (operation), operationHasOwner, owner). \ + TEST_SINGLE_RESULT_FOR_OPERATION(test_name, (operation), operationHasActor, actor). \ TEST_SINGLE_RESULT_FOR_OPERATION(test_name, (operation), operationHasOperator, operator). \ TEST_SINGLE_RESULT_FOR_OPERATION(test_name, (operation), operationHasResult, result). \ TEST_SINGLE_RESULT_FOR_OPERATION(test_name, (operation), operationHasOperandList, (operandList)). \ TEST_SINGLE_RESULT_FOR_OPERATION(test_name, (operation), operationHasAttributeList, (attrList)) -#define CREATE_AND_TEST_OPERATION(test_name, owner, operator, result, operandList, attrList) \ - CREATE_AND_TEST_OPERATOR_INNER(test_name, ([owner, operator, result, (operandList), (attrList)]), owner, operator, result, (operandList), (attrList)) +#define CREATE_AND_TEST_OPERATION(test_name, actor, operator, result, operandList, attrList) \ + CREATE_AND_TEST_OPERATOR_INNER(test_name, ([actor, operator, result, (operandList), (attrList)]), actor, operator, result, (operandList), (attrList)) #define OPERAND_LIST1 ["operand1", nil] #define ATTR_LIST1 [["attr1", $NumberAttributePayload(1)], nil] @@ -42,4 +42,4 @@ CREATE_AND_TEST_OPERATION("test1", "somePrincipal", "someOperator", "ap1", (OPER CREATE_AND_TEST_OPERATION("test2", "prin", "op", "ap2", nil, (ATTR_LIST2)). #define OPERAND_LIST2 ["input1", ["input2", nil]] -CREATE_AND_TEST_OPERATION("test3", "owner", "op2", "ap3", (OPERAND_LIST2), nil). +CREATE_AND_TEST_OPERATION("test3", "actor", "op2", "ap3", (OPERAND_LIST2), nil).