Skip to content

Commit

Permalink
Rename owner to actor in the Operation Record Type.
Browse files Browse the repository at this point in the history
PiperOrigin-RevId: 479127693
  • Loading branch information
bgogul authored and arcs-c3po committed Oct 5, 2022
1 parent d4f2a41 commit 06d813e
Show file tree
Hide file tree
Showing 3 changed files with 30 additions and 30 deletions.
18 changes: 9 additions & 9 deletions src/analysis/souffle/operations.dl
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand All @@ -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.
Expand Down
32 changes: 16 additions & 16 deletions src/analysis/souffle/tag_transforms.dl
Original file line number Diff line number Diff line change
Expand Up @@ -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"
Expand Down Expand Up @@ -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).

Expand Down Expand Up @@ -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)
Expand All @@ -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),
Expand Down Expand Up @@ -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
Expand All @@ -229,27 +229,27 @@ 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) :-
isMergeOp(mergeOp), isIntegrityTag(integrityTag),
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

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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]
Expand All @@ -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).

0 comments on commit 06d813e

Please sign in to comment.