From b7043cfc2998bcdc6223da19f223e1f5c11fc946 Mon Sep 17 00:00:00 2001 From: Florian Wendland Date: Mon, 15 Apr 2024 11:45:43 +0200 Subject: [PATCH] Implement initial PoC for checking return values (#846) Co-authored-by: Selina Lin Co-authored-by: Robert Haimerl --- .../backends/cpg/coko/CokoCpgBackend.kt | 17 +- .../backends/cpg/coko/dsl/DataItemCpgDsl.kt | 77 +++ .../cpg/coko/dsl/ImplementationDsl.kt | 45 +- .../coko/evaluators/CpgWheneverEvaluator.kt | 461 ++++++++++++++++++ .../cpg/coko/modelling/CpgBackendDataItem.kt | 38 ++ .../coko/core/CokoBackend.kt | 10 + .../coko/core/WheneverEvaluator.kt | 71 +++ .../coko/core/dsl/Condition.kt | 148 ++++++ .../coko/core/dsl/Op.kt | 47 +- .../coko/core/dsl/TransformationResult.kt | 66 +++ .../coko/core/modelling/BackendDataItem.kt | 27 + .../core/modelling/ConditionComponents.kt | 93 ++++ .../coko/core/modelling/DataItem.kt | 104 ++++ .../coko/dsl/CokoScript.kt | 34 +- .../coko/dsl/cli/Validation.kt | 4 +- .../coko/dsl/host/CokoExecutor.kt | 60 ++- .../coko/dsl/host/ConceptTranslator.kt | 188 +++++++ .../coko-dsl/src/main/resources/concept.g4 | 69 +++ .../coko/dsl/ConceptTranslationTest.kt | 167 +++++++ .../coko/dsl/WheneverEvaluatorTest.kt | 86 ++++ .../resources/concept/CipherTestFile.java | 39 ++ .../resources/concept/bsi-tr-rules.codyze.kts | 56 +++ .../test/resources/concept/bsi-tr.concepts | 66 +++ .../resources/concept/followedBy.concepts | 11 + .../followedByImplementations.codyze.kts | 33 ++ .../concept/followedByRule.codyze.kts | 6 + .../resources/concept/jca-cipher.codyze.kts | 103 ++++ .../src/test/resources/concept/rpc.concepts | 14 + .../src/test/resources/concept/some.concepts | 25 + 29 files changed, 2109 insertions(+), 56 deletions(-) create mode 100644 codyze-backends/cpg/src/main/kotlin/de/fraunhofer/aisec/codyze/backends/cpg/coko/dsl/DataItemCpgDsl.kt create mode 100644 codyze-backends/cpg/src/main/kotlin/de/fraunhofer/aisec/codyze/backends/cpg/coko/evaluators/CpgWheneverEvaluator.kt create mode 100644 codyze-backends/cpg/src/main/kotlin/de/fraunhofer/aisec/codyze/backends/cpg/coko/modelling/CpgBackendDataItem.kt create mode 100644 codyze-specification-languages/coko/coko-core/src/main/kotlin/de/fraunhofer/aisec/codyze/specificationLanguages/coko/core/WheneverEvaluator.kt create mode 100644 codyze-specification-languages/coko/coko-core/src/main/kotlin/de/fraunhofer/aisec/codyze/specificationLanguages/coko/core/dsl/Condition.kt create mode 100644 codyze-specification-languages/coko/coko-core/src/main/kotlin/de/fraunhofer/aisec/codyze/specificationLanguages/coko/core/dsl/TransformationResult.kt create mode 100644 codyze-specification-languages/coko/coko-core/src/main/kotlin/de/fraunhofer/aisec/codyze/specificationLanguages/coko/core/modelling/BackendDataItem.kt create mode 100644 codyze-specification-languages/coko/coko-core/src/main/kotlin/de/fraunhofer/aisec/codyze/specificationLanguages/coko/core/modelling/ConditionComponents.kt create mode 100644 codyze-specification-languages/coko/coko-core/src/main/kotlin/de/fraunhofer/aisec/codyze/specificationLanguages/coko/core/modelling/DataItem.kt create mode 100644 codyze-specification-languages/coko/coko-dsl/src/main/kotlin/de/fraunhofer/aisec/codyze/specificationLanguages/coko/dsl/host/ConceptTranslator.kt create mode 100644 codyze-specification-languages/coko/coko-dsl/src/main/resources/concept.g4 create mode 100644 codyze-specification-languages/coko/coko-dsl/src/test/kotlin/de/fraunhofer/aisec/codyze/specificationLanguages/coko/dsl/ConceptTranslationTest.kt create mode 100644 codyze-specification-languages/coko/coko-dsl/src/test/kotlin/de/fraunhofer/aisec/codyze/specificationLanguages/coko/dsl/WheneverEvaluatorTest.kt create mode 100644 codyze-specification-languages/coko/coko-dsl/src/test/resources/concept/CipherTestFile.java create mode 100644 codyze-specification-languages/coko/coko-dsl/src/test/resources/concept/bsi-tr-rules.codyze.kts create mode 100644 codyze-specification-languages/coko/coko-dsl/src/test/resources/concept/bsi-tr.concepts create mode 100644 codyze-specification-languages/coko/coko-dsl/src/test/resources/concept/followedBy.concepts create mode 100644 codyze-specification-languages/coko/coko-dsl/src/test/resources/concept/followedByImplementations.codyze.kts create mode 100644 codyze-specification-languages/coko/coko-dsl/src/test/resources/concept/followedByRule.codyze.kts create mode 100644 codyze-specification-languages/coko/coko-dsl/src/test/resources/concept/jca-cipher.codyze.kts create mode 100644 codyze-specification-languages/coko/coko-dsl/src/test/resources/concept/rpc.concepts create mode 100644 codyze-specification-languages/coko/coko-dsl/src/test/resources/concept/some.concepts diff --git a/codyze-backends/cpg/src/main/kotlin/de/fraunhofer/aisec/codyze/backends/cpg/coko/CokoCpgBackend.kt b/codyze-backends/cpg/src/main/kotlin/de/fraunhofer/aisec/codyze/backends/cpg/coko/CokoCpgBackend.kt index a49fb370b..a9533e0a8 100644 --- a/codyze-backends/cpg/src/main/kotlin/de/fraunhofer/aisec/codyze/backends/cpg/coko/CokoCpgBackend.kt +++ b/codyze-backends/cpg/src/main/kotlin/de/fraunhofer/aisec/codyze/backends/cpg/coko/CokoCpgBackend.kt @@ -18,15 +18,15 @@ package de.fraunhofer.aisec.codyze.backends.cpg.coko import de.fraunhofer.aisec.codyze.backends.cpg.CPGBackend import de.fraunhofer.aisec.codyze.backends.cpg.CPGConfiguration import de.fraunhofer.aisec.codyze.backends.cpg.coko.dsl.* -import de.fraunhofer.aisec.codyze.backends.cpg.coko.evaluators.FollowsEvaluator -import de.fraunhofer.aisec.codyze.backends.cpg.coko.evaluators.NeverEvaluator -import de.fraunhofer.aisec.codyze.backends.cpg.coko.evaluators.OnlyEvaluator -import de.fraunhofer.aisec.codyze.backends.cpg.coko.evaluators.OrderEvaluator +import de.fraunhofer.aisec.codyze.backends.cpg.coko.evaluators.* import de.fraunhofer.aisec.codyze.core.VersionProvider import de.fraunhofer.aisec.codyze.core.backend.BackendConfiguration import de.fraunhofer.aisec.codyze.specificationLanguages.coko.core.CokoBackend +import de.fraunhofer.aisec.codyze.specificationLanguages.coko.core.WheneverEvaluator +import de.fraunhofer.aisec.codyze.specificationLanguages.coko.core.dsl.Condition import de.fraunhofer.aisec.codyze.specificationLanguages.coko.core.dsl.Op import de.fraunhofer.aisec.codyze.specificationLanguages.coko.core.dsl.Order +import de.fraunhofer.aisec.codyze.specificationLanguages.coko.core.modelling.ConditionComponent import de.fraunhofer.aisec.codyze.specificationLanguages.coko.core.ordering.OrderToken import de.fraunhofer.aisec.codyze.specificationLanguages.coko.core.ordering.getOp import de.fraunhofer.aisec.cpg.graph.Node @@ -86,4 +86,13 @@ class CokoCpgBackend(config: BackendConfiguration) : */ override fun only(vararg ops: Op): OnlyEvaluator = OnlyEvaluator(ops.toList()) override fun never(vararg ops: Op): NeverEvaluator = NeverEvaluator(ops.toList()) + override fun whenever( + premise: Condition.() -> ConditionComponent, + assertionBlock: WheneverEvaluator.() -> Unit + ): WheneverEvaluator = CpgWheneverEvaluator(Condition().premise()).apply(assertionBlock) + + override fun whenever( + premise: ConditionComponent, + assertionBlock: WheneverEvaluator.() -> Unit + ): WheneverEvaluator = CpgWheneverEvaluator(premise).apply(assertionBlock) } diff --git a/codyze-backends/cpg/src/main/kotlin/de/fraunhofer/aisec/codyze/backends/cpg/coko/dsl/DataItemCpgDsl.kt b/codyze-backends/cpg/src/main/kotlin/de/fraunhofer/aisec/codyze/backends/cpg/coko/dsl/DataItemCpgDsl.kt new file mode 100644 index 000000000..287ca5986 --- /dev/null +++ b/codyze-backends/cpg/src/main/kotlin/de/fraunhofer/aisec/codyze/backends/cpg/coko/dsl/DataItemCpgDsl.kt @@ -0,0 +1,77 @@ +/* + * Copyright (c) 2022, Fraunhofer AISEC. All rights reserved. + * + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ +package de.fraunhofer.aisec.codyze.backends.cpg.coko.dsl + +import de.fraunhofer.aisec.codyze.backends.cpg.coko.Nodes +import de.fraunhofer.aisec.codyze.specificationLanguages.coko.core.CokoBackend +import de.fraunhofer.aisec.codyze.specificationLanguages.coko.core.modelling.ArgumentItem +import de.fraunhofer.aisec.codyze.specificationLanguages.coko.core.modelling.DataItem +import de.fraunhofer.aisec.codyze.specificationLanguages.coko.core.modelling.ReturnValueItem +import de.fraunhofer.aisec.codyze.specificationLanguages.coko.core.modelling.Value +import de.fraunhofer.aisec.cpg.graph.* +import de.fraunhofer.aisec.cpg.graph.declarations.VariableDeclaration +import de.fraunhofer.aisec.cpg.graph.statements.expressions.Reference + +/** + * Get all [Nodes] that are associated with this [DataItem]. + */ +context(CokoBackend) +fun DataItem<*>.cpgGetAllNodes(): Nodes = + when (this@DataItem) { + is ReturnValueItem -> op.cpgGetAllNodes().flatMap { it.getVariableInNextDFGOrThis() } + is Value -> this@DataItem.getNodes() + is ArgumentItem -> op.cpgGetAllNodes().map { it.arguments[index] } // TODO: Do we count starting at 0 or 1? + } + +/** + * Get all [Nodes] that are associated with this [DataItem]. + */ +context(CokoBackend) +fun DataItem<*>.cpgGetNodes(): Nodes { + return when (this@DataItem) { + is ReturnValueItem -> op.cpgGetNodes().flatMap { it.getVariableInNextDFGOrThis() } + is Value -> this@DataItem.getNodes() + is ArgumentItem -> op.cpgGetNodes().map { it.arguments[index] } // TODO: Do we count starting at 0 or 1? + } +} + +/** + * Get all [Nodes] that evaluate to the same value as [Value.value]. + */ +context(CokoBackend) +private fun Value<*>.getNodes(): Nodes { + val value = this.value + return if (value is Node) { + listOf(value) + } else { + cpg.literals.filter { node -> + node.value == value + } + cpg.variables.filter { node -> + node.evaluate() == value + } + } +} + +/** + * Returns all [VariableDeclaration]s and [DeclaredReferenceExpression]s that have a DFG edge from [this]. + * If there are none, returns [this]. + */ +private fun Node.getVariableInNextDFGOrThis(): Nodes = + this.nextDFG + .filter { + next -> + next is Reference || next is VariableDeclaration + }.ifEmpty { listOf(this) } diff --git a/codyze-backends/cpg/src/main/kotlin/de/fraunhofer/aisec/codyze/backends/cpg/coko/dsl/ImplementationDsl.kt b/codyze-backends/cpg/src/main/kotlin/de/fraunhofer/aisec/codyze/backends/cpg/coko/dsl/ImplementationDsl.kt index 8423a9758..9de960be9 100644 --- a/codyze-backends/cpg/src/main/kotlin/de/fraunhofer/aisec/codyze/backends/cpg/coko/dsl/ImplementationDsl.kt +++ b/codyze-backends/cpg/src/main/kotlin/de/fraunhofer/aisec/codyze/backends/cpg/coko/dsl/ImplementationDsl.kt @@ -21,17 +21,13 @@ import de.fraunhofer.aisec.codyze.backends.cpg.coko.Nodes import de.fraunhofer.aisec.codyze.specificationLanguages.coko.core.CokoBackend import de.fraunhofer.aisec.codyze.specificationLanguages.coko.core.CokoMarker import de.fraunhofer.aisec.codyze.specificationLanguages.coko.core.dsl.* -import de.fraunhofer.aisec.codyze.specificationLanguages.coko.core.modelling.Definition -import de.fraunhofer.aisec.codyze.specificationLanguages.coko.core.modelling.ParameterGroup -import de.fraunhofer.aisec.codyze.specificationLanguages.coko.core.modelling.Signature +import de.fraunhofer.aisec.codyze.specificationLanguages.coko.core.modelling.* import de.fraunhofer.aisec.cpg.TranslationResult import de.fraunhofer.aisec.cpg.graph.* import de.fraunhofer.aisec.cpg.graph.declarations.ValueDeclaration -import de.fraunhofer.aisec.cpg.graph.statements.expressions.CallExpression -import de.fraunhofer.aisec.cpg.graph.statements.expressions.ConstructExpression -import de.fraunhofer.aisec.cpg.graph.statements.expressions.Expression -import de.fraunhofer.aisec.cpg.graph.statements.expressions.MemberExpression +import de.fraunhofer.aisec.cpg.graph.statements.expressions.* import de.fraunhofer.aisec.cpg.query.dataFlow +import de.fraunhofer.aisec.cpg.query.executionPath // // all functions/properties defined here must use CokoBackend @@ -42,11 +38,21 @@ val CokoBackend.cpg: TranslationResult /** Get all [Nodes] that are associated with this [Op]. */ context(CokoBackend) -fun Op.cpgGetAllNodes(): Nodes = +fun Op.cpgGetAllNodes(): Collection = when (this@Op) { is FunctionOp -> this@Op.definitions.flatMap { def -> this@CokoBackend.cpgCallFqn(def.fqn) } is ConstructorOp -> this@CokoBackend.cpgConstructor(this.classFqn) + is GroupingOp -> this@Op.ops.flatMap { it.cpgGetAllNodes() } + is ConditionalOp -> { + val resultNodes = resultOp.cpgGetAllNodes() + val conditionNodes = conditionOp.cpgGetAllNodes() + resultNodes.filter { resultNode -> + conditionNodes.any { conditionNode -> + dataFlow(conditionNode, resultNode).value + } + } + } } /** @@ -54,7 +60,7 @@ fun Op.cpgGetAllNodes(): Nodes = * [Definition]s. */ context(CokoBackend) -fun Op.cpgGetNodes(): Nodes = +fun Op.cpgGetNodes(): Collection = when (this@Op) { is FunctionOp -> this@Op.definitions @@ -74,6 +80,18 @@ fun Op.cpgGetNodes(): Nodes = sig.unorderedParameters.all { it?.cpgFlowsTo(arguments) ?: false } } } + is GroupingOp -> this@Op.ops.flatMap { it.cpgGetNodes() } + is ConditionalOp -> { + val resultNodes = resultOp.cpgGetNodes() + val conditionNodes = conditionOp.cpgGetNodes() + resultNodes.filter { resultNode -> + conditionNodes.any { conditionNode -> + // TODO: Is it correct to use the EOG relationship here? + val result = executionPath(conditionNode, resultNode) + result.value + } + } + } } /** Returns a list of [ValueDeclaration]s with the matching name. */ @@ -146,7 +164,10 @@ infix fun Any.cpgFlowsTo(that: Collection): Boolean = true } else { when (this) { - is String -> that.any { Regex(this).matches((it as? Expression)?.evaluate()?.toString().orEmpty()) } + is String -> that.any { + val regex = Regex(this) + regex.matches((it as? Expression)?.evaluate()?.toString().orEmpty()) || regex.matches(it.code.orEmpty()) + } is Iterable<*> -> this.any { it?.cpgFlowsTo(that) ?: false } is Array<*> -> this.any { it?.cpgFlowsTo(that) ?: false } is Node -> that.any { dataFlow(this, it).value } @@ -189,8 +210,10 @@ fun CallExpression.cpgSignature(vararg parameters: Any?, hasVarargs: Boolean = f parameter.param cpgFlowsTo arguments[i] // checks if the type of the argument is the same is Type -> cpgCheckType(parameter, i) - // check if any of the Nodes from the Op flow to the argument + // check if any of the Nodes of the Op flow to the argument is Op -> parameter.cpgGetNodes() cpgFlowsTo arguments[i] + // check if any of the Nodes of the DataItem flow to the argument + is DataItem<*> -> parameter.cpgGetNodes() cpgFlowsTo arguments[i] // checks if there is dataflow from the parameter to the argument in the same position else -> parameter cpgFlowsTo arguments[i] } diff --git a/codyze-backends/cpg/src/main/kotlin/de/fraunhofer/aisec/codyze/backends/cpg/coko/evaluators/CpgWheneverEvaluator.kt b/codyze-backends/cpg/src/main/kotlin/de/fraunhofer/aisec/codyze/backends/cpg/coko/evaluators/CpgWheneverEvaluator.kt new file mode 100644 index 000000000..c6595faa0 --- /dev/null +++ b/codyze-backends/cpg/src/main/kotlin/de/fraunhofer/aisec/codyze/backends/cpg/coko/evaluators/CpgWheneverEvaluator.kt @@ -0,0 +1,461 @@ +/* + * Copyright (c) 2023, Fraunhofer AISEC. All rights reserved. + * + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ +package de.fraunhofer.aisec.codyze.backends.cpg.coko.evaluators + +import de.fraunhofer.aisec.codyze.backends.cpg.coko.CpgFinding +import de.fraunhofer.aisec.codyze.backends.cpg.coko.Nodes +import de.fraunhofer.aisec.codyze.backends.cpg.coko.dsl.cpgGetNodes +import de.fraunhofer.aisec.codyze.backends.cpg.coko.modelling.toBackendDataItem +import de.fraunhofer.aisec.codyze.specificationLanguages.coko.core.* +import de.fraunhofer.aisec.codyze.specificationLanguages.coko.core.dsl.Rule +import de.fraunhofer.aisec.codyze.specificationLanguages.coko.core.dsl.TransformationResult +import de.fraunhofer.aisec.codyze.specificationLanguages.coko.core.modelling.* +import de.fraunhofer.aisec.cpg.graph.Node +import de.fraunhofer.aisec.cpg.query.executionPath +import kotlin.reflect.full.findAnnotation + +context(de.fraunhofer.aisec.codyze.backends.cpg.coko.CokoCpgBackend) +@Suppress("complexity.TooManyFunctions") +class CpgWheneverEvaluator(premise: ConditionComponent) : WheneverEvaluator(premise) { + + private val defaultFailMessage: String = "" + + private val defaultPassMessage: String = "" + override fun evaluate(context: EvaluationContext): Collection { + val ruleAnnotation = context.rule.findAnnotation() + val failMessage = ruleAnnotation?.failMessage?.takeIf { it.isNotEmpty() } ?: defaultFailMessage + val passMessage = ruleAnnotation?.passMessage?.takeIf { it.isNotEmpty() } ?: defaultPassMessage + + val findings = mutableListOf() + + // First find the nodes corresponding to the premise + val (premiseNodes, _, premiseProblems) = evaluateConditionComponentToCpgNodes(premise) + + // If there are no premiseNodes, we cannot evaluate further + if (premiseNodes.isEmpty()) { + if (premiseProblems.isNotEmpty()) { + // If there were problems resolving the premise, we cannot be sure that the rule was followed + findings.add( + CpgFinding( + message = "$premise could not be resolved correctly. $premiseProblems", + kind = Finding.Kind.Open, + ) + ) + } else { + // Since there were no problems in resolving the premise, the rule must not be applicable + findings.add( + CpgFinding( + message = "$premise was not found in code.", + kind = Finding.Kind.NotApplicable, + ) + ) + } + } else { + // check for each premiseNode if the ensures and callAssertions are fulfilled + for (premiseNode in premiseNodes) { + // find nodes that fulfill the ensures conditions + val ensuresToNodes = ensures.associateWith { ensure -> + evaluateConditionComponentToCpgNodes( + ensure, + premiseNode + ).removeDummyNodes() + } + // find nodes that fulfill the call conditions + val callAssertionsToNodes = callAssertions.associateWith { callAssertion -> + val nodes = callAssertion.op.cpgGetNodes() + val location = callAssertion.location + if (location != null) { + when (location.scope) { + Scope.Function -> { + when (location.direction) { + Direction.Afterwards -> TODO() + Direction.Before -> TODO() + Direction.Somewhere -> TODO() + } + } + Scope.Block -> TODO() + } + } + TODO() + // EvaluationResult(nodes, emptyList(), Problems()) + } + findings.addAll( + generateFindings(premiseNode, ensuresToNodes + callAssertionsToNodes, passMessage, failMessage) + ) + } + } + + return findings + } + + /** Generates the findings based on what nodes were found for each condition in [conditionToNodes]. */ + private fun generateFindings( + premiseNode: Node, + conditionToNodes: Map, + passMessage: String, + failMessage: String + ): Collection { + val findings = mutableListOf() + + val unfulfilledConditions = conditionToNodes.filterValues { (fulfilled, _, _) -> fulfilled.isEmpty() } + + // If there is a condition that was not fulfilled, the rule was not followed + if (unfulfilledConditions.isNotEmpty()) { + for ((condition, nodesToProblems) in unfulfilledConditions) { + val (_, unfulfilled, problems) = nodesToProblems + if (problems.isNotEmpty()) { + // If there were problems resolving the condition, we cannot be sure that the rule was broken or not + findings.add( + CpgFinding( + message = "There were problems in resolving $condition. $problems", + kind = Finding.Kind.Open, + node = premiseNode, + relatedNodes = problems.getNodes() + ) + ) + } else { + // Since there were no problems, this means that the condition was definitely not fulfilled and + // the rule was broken + findings.add( + CpgFinding( + // TODO: Better message + message = "No $condition found around $premise. $failMessage", + kind = Finding.Kind.Fail, + node = premiseNode, + relatedNodes = unfulfilled + ) + ) + } + } + } else { + // Since there are no unfulfilled conditions, the rule was followed for this premiseNode + findings.add( + CpgFinding( + message = passMessage, + kind = Finding.Kind.Pass, + node = premiseNode, + relatedNodes = conditionToNodes.values.flatMap { it.fulfillingNodes } + ) + ) + + // document any problems that occurred when resolving the condition + val conditionToProblems = conditionToNodes.mapValues { (_, result) -> result.problems } + for ((condition, problems) in conditionToProblems) { + if (problems.isNotEmpty()) { + CpgFinding( + message = "There were problems in resolving $condition. $problems", + kind = Finding.Kind.Informational, + node = premiseNode, + relatedNodes = problems.getNodes() + ) + } + } + } + + return findings + } + + /** + * Finds the nodes that are represented by the [conditionNode]. + * If [premiseNode] is given, only nodes that are in its vicinity are considered. + */ + private fun evaluateConditionNodeToCpgNodes( + conditionNode: ConditionNode, + premiseNode: Node? = null + ): EvaluationResult { + return when (conditionNode) { + is ConditionComponent -> evaluateConditionComponentToCpgNodes(conditionNode, premiseNode) + is ArgumentItem<*> -> evaluateArgumentItemToCpgNodes(conditionNode, premiseNode) + is ReturnValueItem<*> -> evaluateReturnValueItemToCpgNodes(conditionNode, premiseNode) + is Value<*> -> evaluateValueToCpgNodes(conditionNode, premiseNode) + } + } + + /** + * Finds the nodes that are represented by [value]. + */ + @Suppress("style.UnusedParameter") + private fun evaluateValueToCpgNodes(value: Value<*>, premiseNode: Node? = null): EvaluationResult { + // We return a [DummyNode] here because Value objects don't use the information from the backend + // for their transformation. + return EvaluationResult(listOf(DummyNode()), emptyList(), Problems()) + } + + /** + * Finds the nodes that are represented by [argumentItem]. + * If [premiseNode] is given, only nodes that are in its vicinity are considered. + */ + private fun evaluateArgumentItemToCpgNodes( + argumentItem: ArgumentItem<*>, + premiseNode: Node? = null + ): EvaluationResult { + val nodes = argumentItem.cpgGetNodes().filterWithDistanceToPremise(premiseNode) + return EvaluationResult(nodes, emptyList(), Problems()) + } + + /** + * Finds the nodes that are represented by [returnValueItem]. + * If [premiseNode] is given, only nodes that are in its vicinity are considered. + */ + private fun evaluateReturnValueItemToCpgNodes( + returnValueItem: ReturnValueItem<*>, + premiseNode: Node? = null + ): EvaluationResult { + val nodes = returnValueItem.cpgGetNodes().filterWithDistanceToPremise(premiseNode) + return EvaluationResult(nodes, emptyList(), Problems()) + } + + /** + * Finds the nodes that fulfill and don't fulfill the [conditionComponent]. + * If [premiseNode] is given, only nodes that are in its vicinity are considered. + */ + private fun evaluateConditionComponentToCpgNodes( + conditionComponent: ConditionComponent, + premiseNode: Node? = null + ): EvaluationResult { + return when (conditionComponent) { + is BinaryLogicalConditionComponent -> + evaluateBinaryLogicalConditionComponent(conditionComponent, premiseNode) + is ComparisonConditionComponent -> evaluateComparisonConditionComponent(conditionComponent, premiseNode) + is UnaryConditionComponent -> TODO() + is CallConditionComponent -> evaluateCallConditionComponent(conditionComponent, premiseNode) + is ContainsConditionComponent<*, *> -> evaluateContainsConditionComponent(conditionComponent, premiseNode) + } + } + + /** + * Combines the nodes of the right and left side of the [binaryLogicalConditionComponent]. + * If [premiseNode] is given, only nodes that are in its vicinity are considered. + */ + private fun evaluateBinaryLogicalConditionComponent( + binaryLogicalConditionComponent: BinaryLogicalConditionComponent, + premiseNode: Node? = null + ): EvaluationResult { + val (leftFulfillingNodes, leftUnfulfillingNodes, leftProblems) = + evaluateConditionComponentToCpgNodes(binaryLogicalConditionComponent.left, premiseNode) + val (rightFulfillingNodes, rightUnfulfillingNodes, rightProblems) = + evaluateConditionComponentToCpgNodes(binaryLogicalConditionComponent.right, premiseNode) + return when (binaryLogicalConditionComponent.operator) { + BinaryLogicalOperatorName.AND -> + EvaluationResult( + leftFulfillingNodes intersect rightFulfillingNodes.toSet(), + // we return the union of the unfulfilled nodes since we want to collect them all + leftUnfulfillingNodes union rightUnfulfillingNodes, + leftProblems + rightProblems + ) + BinaryLogicalOperatorName.OR -> + EvaluationResult( + leftFulfillingNodes union rightFulfillingNodes, + leftUnfulfillingNodes union rightUnfulfillingNodes, + leftProblems + rightProblems + ) + } + } + + /** + * Finds the nodes that fulfill and don't fulfill the [comparisonConditionComponent]. + * If [premiseNode] is given, only nodes that are in its vicinity are considered. + */ + private fun evaluateComparisonConditionComponent( + comparisonConditionComponent: ComparisonConditionComponent, + premiseNode: Node? = null + ): EvaluationResult { + val (leftFulfillingNodes, leftUnfulfillingNodes, leftProblems) = + evaluateConditionNodeToCpgNodes(comparisonConditionComponent.left, premiseNode) + val (rightFulfillingNodes, rightUnfulfillingNodes, rightProblems) = + evaluateConditionNodeToCpgNodes(comparisonConditionComponent.right, premiseNode) + + val newProblems = Problems() + val newFulfillingNodes = mutableSetOf() + val newUnfulfillingNodes = mutableSetOf() + + // These are the nodes where the transformation produced a value which can hopefully compared to one another + val leftNodesToValues = + leftFulfillingNodes.toNodesToValues(newProblems, comparisonConditionComponent.left.transformation) + val rightNodesToValues = + rightFulfillingNodes.toNodesToValues(newProblems, comparisonConditionComponent.right.transformation) + + for ((leftNode, leftValue) in leftNodesToValues) { + // we partition the rightNodes into ones that fulfill and + // the ones that do not fulfill this condition when compared to the leftNode + val (fulfilling, unfulfilling) = when (comparisonConditionComponent.operator) { + ComparisonOperatorName.GEQ -> TODO() + ComparisonOperatorName.GT -> TODO() + ComparisonOperatorName.LEQ -> TODO() + ComparisonOperatorName.LT -> TODO("How do we ensure that both values have an order?") + ComparisonOperatorName.EQ -> + rightNodesToValues.toList().partition { (_, rightValue) -> leftValue == rightValue } + ComparisonOperatorName.NEQ -> + rightNodesToValues.toList().partition { (_, rightValue) -> leftValue != rightValue } + } + newFulfillingNodes.addAll(fulfilling.map { it.first }) + newUnfulfillingNodes.addAll(unfulfilling.map { it.first }) + if (fulfilling.isEmpty()) { + // there was no rightNode where the comparison to this leftNode returned true, + // so it does not fulfill this condition + newUnfulfillingNodes.add( + leftNode + ) + } else { + // there was a rightNode where the comparison to this leftNode returned true, + // so it fulfills this condition + newFulfillingNodes.add(leftNode) + } + } + + return EvaluationResult( + newFulfillingNodes, + leftUnfulfillingNodes + rightUnfulfillingNodes + newUnfulfillingNodes, + leftProblems + rightProblems + newProblems + ) + } + + /** + * Finds the nodes of the [Op] of [callConditionComponent]. + * If [premiseNode] is given, only nodes that are in its vicinity are considered. + */ + private fun evaluateCallConditionComponent( + callConditionComponent: CallConditionComponent, + premiseNode: Node? = null + ): EvaluationResult { + val callNodes = callConditionComponent.op.cpgGetNodes().filterWithDistanceToPremise(premiseNode) + return EvaluationResult(callNodes, emptyList(), Problems()) + } + + /** + * Finds the nodes of the [DataItem] of [containsConditionComponent] for which + * its transformed value is contained in [ContainsConditionComponent.collection]. + * If [premiseNode] is given, only nodes that are in its vicinity are considered. + */ + private fun evaluateContainsConditionComponent( + containsConditionComponent: ContainsConditionComponent<*, *>, + premiseNode: Node? + ): EvaluationResult { + val problems = Problems() + val nodes = containsConditionComponent.item.cpgGetNodes().filterWithDistanceToPremise(premiseNode) + val (fulfilling, unfulfilling) = nodes.partition { node -> + val backendDataItem = node.toBackendDataItem() + val transformationResult = containsConditionComponent.item.transformation(backendDataItem) + if (transformationResult.isFailure) { + problems.add( + transformationResult.getFailureReasonOrNull() ?: "Transformation of $backendDataItem failed", + node + ) + false + } else { + val value = transformationResult.getValueOrNull() + containsConditionComponent.collection.contains(value) + } + } + + return EvaluationResult(fulfilling, unfulfilling, problems) + } + + /** + * Maps the nodes in [Nodes] to their transformed values based on [transformation]. + * If the transformation was unsuccessful, the failure reason is added to [problems]. + */ + private fun Nodes.toNodesToValues( + problems: Problems, + transformation: (BackendDataItem) -> TransformationResult + ): Map { + val result = mutableMapOf() + + for (node in this) { + val backendDataItem = node.toBackendDataItem() + val transformationResult = transformation(backendDataItem) + val value = transformationResult.getValueOrNull() + if (value == null) { + problems.add(transformationResult.getFailureReasonOrNull() ?: "Value was null", node) + } else { + result[node] = value + } + } + + return result + } + + /** + * Filters out all nodes that are not in the vicinity of [premiseNode]. + */ + // TODO: Is this filter ok? Do we have to limit how far the nodes can be apart? + private fun Nodes.filterWithDistanceToPremise(premiseNode: Node?): Nodes { + return if (premiseNode != null) { + this.filter { executionPath(it, premiseNode).value } + } else { + this + } + } + + /** + * A class to collect the problems that are encountered in an evaluation. + */ + class Problems { + private val map: MutableMap = mutableMapOf() + + fun add(reason: String, value: Node) { + map[value] = reason + } + + fun getNodes(): Nodes = map.keys + + fun isNotEmpty(): Boolean { + return map.isNotEmpty() + } + + operator fun plus(other: Problems): Problems { + map.putAll(other.map) + return this + } + + override fun toString(): String { + return map.mapKeys { (node, _) -> node.toBackendDataItem() }.toString() + } + } + + /** + * A class to collect the results of the evaluation of a [ConditionNode]. + * [fulfillingNodes] contains all nodes that fulfill the [ConditionNode], + * [unfulfillingNodes] contains all nodes that do not fulfill the [ConditionNode], + * [problems] are the problems encountered in the evaluation. + */ + data class EvaluationResult( + val fulfillingNodes: MutableList = mutableListOf(), + val unfulfillingNodes: MutableList = mutableListOf(), + val problems: Problems = Problems() + ) { + constructor( + fulfillingNodes: Nodes, + unfulfillingNodes: Nodes, + problems: Problems + ) : this(fulfillingNodes.toMutableList(), unfulfillingNodes.toMutableList(), problems) + + operator fun plus(other: EvaluationResult): EvaluationResult { + fulfillingNodes.addAll(other.fulfillingNodes) + unfulfillingNodes.addAll(other.unfulfillingNodes) + problems + other.problems + return this + } + + fun removeDummyNodes(): EvaluationResult { + fulfillingNodes.removeIf { it is DummyNode } + unfulfillingNodes.removeIf { it is DummyNode } + return this + } + } + + class DummyNode : Node() +} diff --git a/codyze-backends/cpg/src/main/kotlin/de/fraunhofer/aisec/codyze/backends/cpg/coko/modelling/CpgBackendDataItem.kt b/codyze-backends/cpg/src/main/kotlin/de/fraunhofer/aisec/codyze/backends/cpg/coko/modelling/CpgBackendDataItem.kt new file mode 100644 index 000000000..b72d0194e --- /dev/null +++ b/codyze-backends/cpg/src/main/kotlin/de/fraunhofer/aisec/codyze/backends/cpg/coko/modelling/CpgBackendDataItem.kt @@ -0,0 +1,38 @@ +/* + * Copyright (c) 2022, Fraunhofer AISEC. All rights reserved. + * + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ +package de.fraunhofer.aisec.codyze.backends.cpg.coko.modelling + +import de.fraunhofer.aisec.codyze.specificationLanguages.coko.core.modelling.BackendDataItem +import de.fraunhofer.aisec.cpg.graph.Node +import de.fraunhofer.aisec.cpg.graph.declarations.Declaration +import de.fraunhofer.aisec.cpg.graph.evaluate +import de.fraunhofer.aisec.cpg.graph.statements.expressions.Expression +import de.fraunhofer.aisec.cpg.graph.types.HasType + +/** Implementation of the [BackendDataItem] interface for the CPG */ +class CpgBackendDataItem( + override val name: String?, + override val value: Any?, + override val type: String? +) : BackendDataItem + +/** Returns the [CpgBackendDataItem] of the given [Node] */ +fun Node.toBackendDataItem(): CpgBackendDataItem { + val value = (this as? Expression)?.evaluate() ?: (this as? Declaration)?.evaluate() + val type = (this as? HasType)?.type?.typeName + + return CpgBackendDataItem(name = name.toString(), value = value, type = type) +} diff --git a/codyze-specification-languages/coko/coko-core/src/main/kotlin/de/fraunhofer/aisec/codyze/specificationLanguages/coko/core/CokoBackend.kt b/codyze-specification-languages/coko/coko-core/src/main/kotlin/de/fraunhofer/aisec/codyze/specificationLanguages/coko/core/CokoBackend.kt index b58623014..09f00d662 100644 --- a/codyze-specification-languages/coko/coko-core/src/main/kotlin/de/fraunhofer/aisec/codyze/specificationLanguages/coko/core/CokoBackend.kt +++ b/codyze-specification-languages/coko/coko-core/src/main/kotlin/de/fraunhofer/aisec/codyze/specificationLanguages/coko/core/CokoBackend.kt @@ -16,8 +16,10 @@ package de.fraunhofer.aisec.codyze.specificationLanguages.coko.core import de.fraunhofer.aisec.codyze.core.backend.Backend +import de.fraunhofer.aisec.codyze.specificationLanguages.coko.core.dsl.Condition import de.fraunhofer.aisec.codyze.specificationLanguages.coko.core.dsl.Op import de.fraunhofer.aisec.codyze.specificationLanguages.coko.core.dsl.Order +import de.fraunhofer.aisec.codyze.specificationLanguages.coko.core.modelling.ConditionComponent import de.fraunhofer.aisec.codyze.specificationLanguages.coko.core.ordering.OrderToken import kotlin.reflect.KFunction @@ -61,4 +63,12 @@ interface CokoBackend : Backend { /** Ensures that there are no calls to the [ops] which have arguments that fit the parameters specified in [ops] */ fun never(vararg ops: Op): Evaluator + + /** Verifies that the [assertionBlock] is ensured when [premise] is found */ + fun whenever( + premise: Condition.() -> ConditionComponent, + assertionBlock: WheneverEvaluator.() -> Unit + ): WheneverEvaluator + + fun whenever(premise: ConditionComponent, assertionBlock: WheneverEvaluator.() -> Unit): WheneverEvaluator } diff --git a/codyze-specification-languages/coko/coko-core/src/main/kotlin/de/fraunhofer/aisec/codyze/specificationLanguages/coko/core/WheneverEvaluator.kt b/codyze-specification-languages/coko/coko-core/src/main/kotlin/de/fraunhofer/aisec/codyze/specificationLanguages/coko/core/WheneverEvaluator.kt new file mode 100644 index 000000000..86ced94a9 --- /dev/null +++ b/codyze-specification-languages/coko/coko-core/src/main/kotlin/de/fraunhofer/aisec/codyze/specificationLanguages/coko/core/WheneverEvaluator.kt @@ -0,0 +1,71 @@ +/* + * Copyright (c) 2022, Fraunhofer AISEC. All rights reserved. + * + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ +package de.fraunhofer.aisec.codyze.specificationLanguages.coko.core + +import de.fraunhofer.aisec.codyze.specificationLanguages.coko.core.dsl.Condition +import de.fraunhofer.aisec.codyze.specificationLanguages.coko.core.dsl.Op +import de.fraunhofer.aisec.codyze.specificationLanguages.coko.core.modelling.CallConditionComponent +import de.fraunhofer.aisec.codyze.specificationLanguages.coko.core.modelling.ConditionComponent + +/** + * An evaluator that describes what should happen around the code that the [premise] represents. + */ +abstract class WheneverEvaluator(protected val premise: ConditionComponent) : Evaluator { + protected val ensures: MutableList = mutableListOf() + protected val callAssertions: MutableList = mutableListOf() + + /** + * Specifies a condition that has to be ensured around the [premise]. + */ + fun ensure(block: Condition.() -> ConditionComponent) { + ensures.add(Condition().run(block)) + } + + /** + * Specifies that [op] has to be called in the given [location] in regard to the [premise]. + */ + fun call(op: Op, location: CallLocationBuilder.() -> CallLocation? = { null }) { + callAssertions.add(CallAssertion(op, CallLocationBuilder().run(location))) + } +} + +class CallLocationBuilder { + infix fun Direction.within(scope: Scope) = CallLocation(this@Direction, scope) +} +data class CallLocation(val direction: Direction, val scope: Scope) + +enum class Direction { + Afterwards, Before, Somewhere +} + +enum class Scope { + Function, Block +} + +class CallAssertion(op: Op, val location: CallLocation? = null) : CallConditionComponent(op) { + override fun toString(): String = + "Call $op ${ + if (location != null) { + "${location.direction} in ${location.scope}." + } else { + "" + } + }" +} + +class ListBuilder { + operator fun get(vararg things: E): List = things.toList() +} diff --git a/codyze-specification-languages/coko/coko-core/src/main/kotlin/de/fraunhofer/aisec/codyze/specificationLanguages/coko/core/dsl/Condition.kt b/codyze-specification-languages/coko/coko-core/src/main/kotlin/de/fraunhofer/aisec/codyze/specificationLanguages/coko/core/dsl/Condition.kt new file mode 100644 index 000000000..79f345bb5 --- /dev/null +++ b/codyze-specification-languages/coko/coko-core/src/main/kotlin/de/fraunhofer/aisec/codyze/specificationLanguages/coko/core/dsl/Condition.kt @@ -0,0 +1,148 @@ +/* + * Copyright (c) 2022, Fraunhofer AISEC. All rights reserved. + * + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ +package de.fraunhofer.aisec.codyze.specificationLanguages.coko.core.dsl + +import de.fraunhofer.aisec.codyze.specificationLanguages.coko.core.ListBuilder +import de.fraunhofer.aisec.codyze.specificationLanguages.coko.core.modelling.* + +fun condition(block: Condition.() -> ConditionComponent) = Condition().run(block) + +/** This class exists to restrict where the functions can be called */ +@Suppress("complexity.TooManyFunctions") +class Condition { + /** Can be used to build a list like `list[x,y,z]` */ + val list by lazy { ListBuilder() } + + /** + * Builds a [ContainsConditionComponent] that specifies that the value of this [DataItem] should be + * contained in [collection]. + */ + infix fun DataItem<*>.within(collection: Collection<*>) = + ContainsConditionComponent(this, collection) + + /** + * Builds a [ComparisonConditionComponent] that specifies that the value of this [DataItem] should be + * greater than the value of [other]. + */ + infix fun DataItem<*>.gt(other: DataItem<*>) = + ComparisonConditionComponent(this, other, ComparisonOperatorName.GT) + + /** + * Builds a [ComparisonConditionComponent] that specifies that the value of this should be + * greater than the value of [other]. + */ + // This function exists so users don't have to wrap the objects as Value themselves + infix fun Any.gt(other: Any) = toValue(this) gt toValue(other) + + /** + * Builds a [ComparisonConditionComponent] that specifies that the value of this [DataItem] should be + * greater or equal to the value of [other]. + */ + infix fun DataItem<*>.geq(other: DataItem<*>) = + ComparisonConditionComponent(this, other, ComparisonOperatorName.GEQ) + + /** + * Builds a [ComparisonConditionComponent] that specifies that the value of this should be + * greater or equal to the value of [other]. + */ + // This function exists so users don't have to wrap the objects as Value themselves + infix fun Any.geq(other: Any) = toValue(this) geq toValue(other) + + /** + * Builds a [ComparisonConditionComponent] that specifies that the value of this [DataItem] should be + * less than the value of [other]. + */ + infix fun DataItem<*>.lt(other: DataItem<*>) = + ComparisonConditionComponent(this, other, ComparisonOperatorName.LT) + + /** + * Builds a [ComparisonConditionComponent] that specifies that the value of this should be + * less than the value of [other]. + */ + // This function exists so users don't have to wrap the objects as Value themselves + infix fun Any.lt(other: Any) = toValue(this) lt toValue(other) + + /** + * Builds a [ComparisonConditionComponent] that specifies that the value of this [DataItem] should be + * less or equal to the value of [other]. + */ + infix fun DataItem<*>.leq(other: DataItem<*>) = + ComparisonConditionComponent(this, other, ComparisonOperatorName.LEQ) + + /** + * Builds a [ComparisonConditionComponent] that specifies that the value of this should be + * less or equal to the value of [other]. + */ + // This function exists so users don't have to wrap the objects as Value themselves + infix fun Any.leq(other: Any) = toValue(this) leq toValue(other) + + /** + * Builds a [ComparisonConditionComponent] that specifies that the value of this [DataItem] should be + * equal to the value of [other]. + */ + infix fun DataItem<*>.eq(other: DataItem<*>) = + ComparisonConditionComponent(this, other, ComparisonOperatorName.EQ) + + /** + * Builds a [ComparisonConditionComponent] that specifies that the value of this should be + * equal to the value of [other]. + */ + // This function exists so users don't have to wrap the objects as Value themselves + infix fun Any.eq(other: Any) = toValue(this) eq toValue(other) + + /** + * Builds a [ComparisonConditionComponent] that specifies that the value of this [DataItem] should not be + * equal to the value of [other]. + */ + infix fun DataItem<*>.neq(other: DataItem<*>) = + ComparisonConditionComponent(this, other, ComparisonOperatorName.NEQ) + + /** + * Builds a [ComparisonConditionComponent] that specifies that the value of this should not be + * equal to the value of [other]. + */ + // This function exists so users don't have to wrap the objects as Value themselves + infix fun Any.neq(other: Any) = toValue(this) neq toValue(other) + + /** + * Builds a [CallConditionComponent] that specifies that [op] should be called. + */ + // TODO: Is this needed? + fun call(op: Op) = CallConditionComponent(op) + + /** + * Connects two [ConditionComponent]s with a logical and. + */ + infix fun ConditionComponent.and(other: ConditionComponent) = + BinaryLogicalConditionComponent(this, other, BinaryLogicalOperatorName.AND) + + /** + * Connects two [ConditionComponent]s with a logical or. + */ + infix fun ConditionComponent.or(other: ConditionComponent) = + BinaryLogicalConditionComponent(this, other, BinaryLogicalOperatorName.OR) + + /** + * Negates a [ConditionComponent] + */ + fun not(conditionComponent: ConditionComponent) = UnaryConditionComponent(conditionComponent, UnaryOperatorName.NOT) + + private fun toValue(value: Any): DataItem<*> = + when (value) { + is DataItem<*> -> value + else -> Value(value) + } +} diff --git a/codyze-specification-languages/coko/coko-core/src/main/kotlin/de/fraunhofer/aisec/codyze/specificationLanguages/coko/core/dsl/Op.kt b/codyze-specification-languages/coko/coko-core/src/main/kotlin/de/fraunhofer/aisec/codyze/specificationLanguages/coko/core/dsl/Op.kt index 8be75c30f..e8b707603 100644 --- a/codyze-specification-languages/coko/coko-core/src/main/kotlin/de/fraunhofer/aisec/codyze/specificationLanguages/coko/core/dsl/Op.kt +++ b/codyze-specification-languages/coko/coko-core/src/main/kotlin/de/fraunhofer/aisec/codyze/specificationLanguages/coko/core/dsl/Op.kt @@ -13,25 +13,37 @@ * See the License for the specific language governing permissions and * limitations under the License. */ +@file:Suppress("TooManyFunctions") + package de.fraunhofer.aisec.codyze.specificationLanguages.coko.core.dsl import de.fraunhofer.aisec.codyze.specificationLanguages.coko.core.CokoMarker -import de.fraunhofer.aisec.codyze.specificationLanguages.coko.core.modelling.Definition -import de.fraunhofer.aisec.codyze.specificationLanguages.coko.core.modelling.Parameter -import de.fraunhofer.aisec.codyze.specificationLanguages.coko.core.modelling.ParameterGroup -import de.fraunhofer.aisec.codyze.specificationLanguages.coko.core.modelling.Signature +import de.fraunhofer.aisec.codyze.specificationLanguages.coko.core.modelling.* import de.fraunhofer.aisec.codyze.specificationLanguages.coko.core.ordering.OrderFragment import de.fraunhofer.aisec.codyze.specificationLanguages.coko.core.ordering.TerminalOrderNode @CokoMarker sealed interface Op : OrderFragment { val ownerClassFqn: String + val returnValue: ReturnValueItem + get() = ReturnValueItem(this) + + val arguments: Arguments + get() = Arguments(this) + override fun toNode(): TerminalOrderNode = TerminalOrderNode( baseName = ownerClassFqn, opName = hashCode().toString() ) } +/** + * A helper class that makes it possible to construct an [ArgumentItem] with an indexed access (e.g. op.argument[1]) + */ +class Arguments(val op: Op) { + operator fun get(index: Int): ArgumentItem = ArgumentItem(op, index) +} + /** * Represents a group of functions that serve the same purpose in the API. * @@ -110,6 +122,23 @@ class ConstructorOp internal constructor( } } +/** An [Op] that contains other [Op]s */ +data class GroupingOp(val ops: Set, override val ownerClassFqn: String = "") : Op { + override fun toString(): String { + return ops.joinToString() + } +} + +/** + * An [Op] that describes that the function calls found with [resultOp] depend on the function calls found with the [conditionOp] + */ +// TODO: Clearly define the dependency we are describing here -> is it data flow, control flow, or something else? +data class ConditionalOp(val resultOp: Op, val conditionOp: Op, override val ownerClassFqn: String = "") : Op { + override fun toString(): String { + return "$resultOp with $conditionOp" + } +} + context(Any) // This is needed to have access to the owner of this function // -> in which class is the function defined that created this [OP] /** @@ -159,6 +188,16 @@ fun constructor(classFqn: String, block: ConstructorOp.() -> Unit): ConstructorO return ConstructorOp(classFqn, this@Any::class.java.name).apply(block) } +/** Create a [GroupingOp] containing the given [ops]. */ +context(Any) +fun opGroup(vararg ops: Op): GroupingOp = GroupingOp(ops.toSet(), this@Any::class.java.name) + +/** + * Create a [ConditionalOp] with [this] as the [ConditionalOp.resultOp] and [conditionOp] as the [ConditionalOp.conditionOp] + */ +context(Any) +infix fun Op.with(conditionOp: Op): ConditionalOp = ConditionalOp(this, conditionOp, this@Any::class.java.name) + /** * Create a [Definition] which can be added to the [FunctionOp]. * diff --git a/codyze-specification-languages/coko/coko-core/src/main/kotlin/de/fraunhofer/aisec/codyze/specificationLanguages/coko/core/dsl/TransformationResult.kt b/codyze-specification-languages/coko/coko-core/src/main/kotlin/de/fraunhofer/aisec/codyze/specificationLanguages/coko/core/dsl/TransformationResult.kt new file mode 100644 index 000000000..552262745 --- /dev/null +++ b/codyze-specification-languages/coko/coko-core/src/main/kotlin/de/fraunhofer/aisec/codyze/specificationLanguages/coko/core/dsl/TransformationResult.kt @@ -0,0 +1,66 @@ +/* + * Copyright (c) 2022, Fraunhofer AISEC. All rights reserved. + * + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ +package de.fraunhofer.aisec.codyze.specificationLanguages.coko.core.dsl + +/** + * This class works similar to the [Result] class in the Kotlin standard library. + * The difference is that the [TransformationFailure] can store information other than [Throwable]s to be able to + * describe the reasons for failure in more detail. + */ +sealed interface TransformationResult { + val isFailure: Boolean + val isSuccess: Boolean + + fun getValueOrNull(): E? + fun getFailureReasonOrNull(): T? + override fun toString(): String + + companion object { + /** Creates a [TransformationFailure] object with the given [reason]. */ + fun failure(reason: T): TransformationResult = TransformationFailure(reason) + + /** Creates a [TransformationSuccess] object with the given [value]. */ + fun success(value: E): TransformationResult = TransformationSuccess(value) + } +} + +/** + * This class indicates that the operation was a success and the result is stored in [value]. + */ +private data class TransformationSuccess(val value: E) : TransformationResult { + override val isFailure: Boolean + get() = false + override val isSuccess: Boolean + get() = true + + override fun getValueOrNull(): E? = value + + override fun getFailureReasonOrNull(): T? = null +} + +/** + * This class indicates that the operation was not successful and the reasons are stored in [reason]. + */ +private data class TransformationFailure(val reason: T) : TransformationResult { + override val isFailure: Boolean + get() = true + override val isSuccess: Boolean + get() = false + + override fun getValueOrNull(): E? = null + + override fun getFailureReasonOrNull(): T = reason +} diff --git a/codyze-specification-languages/coko/coko-core/src/main/kotlin/de/fraunhofer/aisec/codyze/specificationLanguages/coko/core/modelling/BackendDataItem.kt b/codyze-specification-languages/coko/coko-core/src/main/kotlin/de/fraunhofer/aisec/codyze/specificationLanguages/coko/core/modelling/BackendDataItem.kt new file mode 100644 index 000000000..07b269fae --- /dev/null +++ b/codyze-specification-languages/coko/coko-core/src/main/kotlin/de/fraunhofer/aisec/codyze/specificationLanguages/coko/core/modelling/BackendDataItem.kt @@ -0,0 +1,27 @@ +/* + * Copyright (c) 2022, Fraunhofer AISEC. All rights reserved. + * + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ +package de.fraunhofer.aisec.codyze.specificationLanguages.coko.core.modelling + +import de.fraunhofer.aisec.codyze.specificationLanguages.coko.core.CokoBackend + +/** + * Interface for accessing info about a DataItem from the [CokoBackend] + */ +interface BackendDataItem { + val name: String? + val value: Any? + val type: String? +} diff --git a/codyze-specification-languages/coko/coko-core/src/main/kotlin/de/fraunhofer/aisec/codyze/specificationLanguages/coko/core/modelling/ConditionComponents.kt b/codyze-specification-languages/coko/coko-core/src/main/kotlin/de/fraunhofer/aisec/codyze/specificationLanguages/coko/core/modelling/ConditionComponents.kt new file mode 100644 index 000000000..aea42f0c2 --- /dev/null +++ b/codyze-specification-languages/coko/coko-core/src/main/kotlin/de/fraunhofer/aisec/codyze/specificationLanguages/coko/core/modelling/ConditionComponents.kt @@ -0,0 +1,93 @@ +/* + * Copyright (c) 2022, Fraunhofer AISEC. All rights reserved. + * + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ +package de.fraunhofer.aisec.codyze.specificationLanguages.coko.core.modelling + +import de.fraunhofer.aisec.codyze.specificationLanguages.coko.core.dsl.Op + +sealed interface ConditionNode { + override fun toString(): String +} + +/** [ConditionNode] that can have children */ +sealed interface ConditionComponent : ConditionNode + +/** [ConditionNode] that does not have children */ +sealed interface ConditionLeaf : ConditionNode + +/** A [ConditionComponent] that has two children and a [operator] */ +sealed interface BinaryConditionComponent : ConditionComponent { + val left: ConditionNode + val right: ConditionNode + val operator: BinaryOperatorName +} + +/** A [BinaryConditionComponent] that compares [left] and [right] based on [operator] (e.g. equality or less than) */ +class ComparisonConditionComponent( + override val left: DataItem<*>, + override val right: DataItem<*>, + override val operator: ComparisonOperatorName +) : BinaryConditionComponent { + override fun toString(): String = "$left ${operator.name} $right" +} + +/** A [BinaryConditionComponent] that logically combines [left] and [right] based on [operator] (e.g. logical and) */ +class BinaryLogicalConditionComponent( + override val left: ConditionComponent, + override val right: ConditionComponent, + override val operator: BinaryLogicalOperatorName +) : BinaryConditionComponent { + override fun toString(): String = "$left ${operator.name} $right" +} + +/** A [ConditionComponent] that has one child, [conditionNode], and a [operator] (e.g. negation) */ +class UnaryConditionComponent( + val conditionNode: ConditionNode, + val operator: UnaryOperatorName +) : ConditionComponent { + override fun toString(): String = "${operator.name} $conditionNode" +} + +/** A [ConditionComponent] that represents a function call */ +// TODO: Is this necessary? And should it be a ConditionLeaf? +open class CallConditionComponent(val op: Op) : ConditionComponent { + override fun toString(): String = op.toString() +} + +/** A [ConditionComponent] that represents the condition that the value of [item] should be in [collection] */ +class ContainsConditionComponent(val item: DataItem, val collection: Collection) : ConditionComponent { + override fun toString(): String = "$item within $collection" +} + +sealed interface BinaryOperatorName { + val operatorCodes: List +} + +enum class BinaryLogicalOperatorName(override val operatorCodes: List) : BinaryOperatorName { + AND(listOf("&&", "and")), + OR(listOf("||", "or")) +} +enum class ComparisonOperatorName(override val operatorCodes: List) : BinaryOperatorName { + GEQ(listOf(">=")), + GT(listOf(">")), + LEQ(listOf("<=")), + LT(listOf("<")), + EQ(listOf("==")), // TODO: python `==` vs `is` + NEQ(listOf("!=")), +} + +enum class UnaryOperatorName(val operatorCodes: List) { + NOT(listOf("!", "not")) +} diff --git a/codyze-specification-languages/coko/coko-core/src/main/kotlin/de/fraunhofer/aisec/codyze/specificationLanguages/coko/core/modelling/DataItem.kt b/codyze-specification-languages/coko/coko-core/src/main/kotlin/de/fraunhofer/aisec/codyze/specificationLanguages/coko/core/modelling/DataItem.kt new file mode 100644 index 000000000..f23e99ace --- /dev/null +++ b/codyze-specification-languages/coko/coko-core/src/main/kotlin/de/fraunhofer/aisec/codyze/specificationLanguages/coko/core/modelling/DataItem.kt @@ -0,0 +1,104 @@ +/* + * Copyright (c) 2022, Fraunhofer AISEC. All rights reserved. + * + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ +package de.fraunhofer.aisec.codyze.specificationLanguages.coko.core.modelling + +import de.fraunhofer.aisec.codyze.specificationLanguages.coko.core.dsl.Op +import de.fraunhofer.aisec.codyze.specificationLanguages.coko.core.dsl.TransformationResult + +/** + * Represents a data item such as a variable or literal. + * + * [transformation] is a function that transforms data from the [CokoBackend] into an object with type [E] + */ +sealed interface DataItem : ConditionLeaf { + val transformation: (BackendDataItem) -> TransformationResult +} + +/** + * Adds an infix function [withTransformation] to a [DataItem]. + */ +sealed interface CanChangeTransformation : DataItem { + /** + * Changes the [transformation] of this [DataItem] into the given [newTransformation]. + */ + infix fun withTransformation( + newTransformation: (BackendDataItem) -> TransformationResult + ): DataItem +} + +/** + * Represents the data item that a function call represented by [op] returns. + */ +data class ReturnValueItem( + val op: Op, + override val transformation: (BackendDataItem) -> TransformationResult = { + TransformationResult.failure("No transformation given from user") + } +) : CanChangeTransformation { + override fun toString(): String = "Return value of $op" + + override infix fun withTransformation( + newTransformation: (BackendDataItem) -> TransformationResult + ): ReturnValueItem = + ReturnValueItem(op = op, transformation = newTransformation) +} + +/** + * Represents the argument at [index] given to the function call represented by [op]. + * + * The [index] starts counting from 0. + */ +data class ArgumentItem( + val op: Op, + val index: Int, + override val transformation: (BackendDataItem) -> TransformationResult = { + TransformationResult.failure("No transformation given from user") + } +) : CanChangeTransformation { + init { + // TODO: Do we count starting at 0 or 1? + require(index >= 0) { "The number of the argument cannot be negative" } + } + + override fun withTransformation( + newTransformation: (BackendDataItem) -> TransformationResult + ): ArgumentItem = + ArgumentItem(op = op, index = index, transformation = newTransformation) + + override fun toString(): String = "${(index + 1).ordinal()} argument of $op" + + @Suppress("MagicNumber") + fun Int.ordinal(): String { + return "$this" + when { + (this % 100 in 11..13) -> "th" + (this % 10) == 1 -> "st" + (this % 10) == 2 -> "nd" + (this % 10) == 3 -> "rd" + else -> "th" + } + } +} + +/** + * A wrapper class for [value] to make it a [DataItem]. + */ +data class Value internal constructor(val value: E) : DataItem { + override val transformation: (BackendDataItem) -> TransformationResult + get() = { TransformationResult.success(value) } +} + +fun value(value: DataItem): DataItem = value +fun value(value: E): DataItem = Value(value) diff --git a/codyze-specification-languages/coko/coko-dsl/src/main/kotlin/de/fraunhofer/aisec/codyze/specificationLanguages/coko/dsl/CokoScript.kt b/codyze-specification-languages/coko/coko-dsl/src/main/kotlin/de/fraunhofer/aisec/codyze/specificationLanguages/coko/dsl/CokoScript.kt index 6827a0f76..f3e268e05 100644 --- a/codyze-specification-languages/coko/coko-dsl/src/main/kotlin/de/fraunhofer/aisec/codyze/specificationLanguages/coko/dsl/CokoScript.kt +++ b/codyze-specification-languages/coko/coko-dsl/src/main/kotlin/de/fraunhofer/aisec/codyze/specificationLanguages/coko/dsl/CokoScript.kt @@ -16,13 +16,10 @@ package de.fraunhofer.aisec.codyze.specificationLanguages.coko.dsl import de.fraunhofer.aisec.codyze.specificationLanguages.coko.core.CokoBackend -import de.fraunhofer.aisec.codyze.specificationLanguages.coko.core.dsl.Import import io.github.oshai.kotlinlogging.KotlinLogging import java.io.File import kotlin.script.experimental.annotations.KotlinScript import kotlin.script.experimental.api.* -import kotlin.script.experimental.host.FileBasedScriptSource -import kotlin.script.experimental.host.FileScriptSource import kotlin.script.experimental.jvm.* import kotlin.script.experimental.jvm.util.scriptCompilationClasspathFromContext @@ -61,6 +58,7 @@ interface PluginDependenciesSpec { internal object ProjectScriptCompilationConfiguration : ScriptCompilationConfiguration({ + baseClass(CokoScript::class) jvm { dependenciesFromClassContext( // extract dependencies from the host environment @@ -109,12 +107,6 @@ internal object ProjectScriptCompilationConfiguration : context.compilationConfiguration.asSuccess() } } - - // the callback called than any of the listed file-level annotations are encountered in - // the compiled script - // the processing is defined by the `handler`, that may return refined configuration - // depending on the annotations - onAnnotations(Import::class, handler = ::configureImportDepsOnAnnotations) } ide { acceptedLocations(ScriptAcceptedLocation.Everywhere) } @@ -146,30 +138,6 @@ private fun resolveClasspathAndGenerateExtensionsFor(pluginsBlock: String?): Lis ) } -// The handler that is called during script compilation in order to reconfigure compilation on the -// fly -fun configureImportDepsOnAnnotations( - context: ScriptConfigurationRefinementContext -): ResultWithDiagnostics { - val annotations = - // If no action is performed, the original configuration should be returned - context.collectedData?.get(ScriptCollectedData.foundAnnotations)?.takeIf { it.isNotEmpty() } - ?: return context.compilationConfiguration.asSuccess() - - val scriptBaseDir = (context.script as? FileBasedScriptSource)?.file?.parentFile - val importedSources = - annotations.flatMap { - (it as? Import)?.paths?.map { sourceName -> - FileScriptSource(scriptBaseDir?.resolve(sourceName) ?: File(sourceName)) - }.orEmpty() - } - - return ScriptCompilationConfiguration(context.compilationConfiguration) { - if (importedSources.isNotEmpty()) importScripts.append(importedSources) - } - .asSuccess() -} - object ProjectScriptEvaluationConfiguration : ScriptEvaluationConfiguration({ // if a script is imported multiple times in the import hierarchy, use a single copy diff --git a/codyze-specification-languages/coko/coko-dsl/src/main/kotlin/de/fraunhofer/aisec/codyze/specificationLanguages/coko/dsl/cli/Validation.kt b/codyze-specification-languages/coko/coko-dsl/src/main/kotlin/de/fraunhofer/aisec/codyze/specificationLanguages/coko/dsl/cli/Validation.kt index df27d81bd..1654c725d 100644 --- a/codyze-specification-languages/coko/coko-dsl/src/main/kotlin/de/fraunhofer/aisec/codyze/specificationLanguages/coko/dsl/cli/Validation.kt +++ b/codyze-specification-languages/coko/coko-dsl/src/main/kotlin/de/fraunhofer/aisec/codyze/specificationLanguages/coko/dsl/cli/Validation.kt @@ -23,8 +23,8 @@ val Path.fileNameString: String fun validateSpec(spec: List): List { require(spec.all { it.isRegularFile() }) { "All given spec paths must be files." } - require(spec.all { it.fileNameString.endsWith(".codyze.kts") }) { - "All given specification files must be coko specification files (*.codyze.kts)." + require(spec.all { it.fileNameString.endsWith(".codyze.kts") || it.fileNameString.endsWith(".concepts") }) { + "All given specification files must be coko specification files (*.codyze.kts) or concept files (*.concepts)." } return spec } diff --git a/codyze-specification-languages/coko/coko-dsl/src/main/kotlin/de/fraunhofer/aisec/codyze/specificationLanguages/coko/dsl/host/CokoExecutor.kt b/codyze-specification-languages/coko/coko-dsl/src/main/kotlin/de/fraunhofer/aisec/codyze/specificationLanguages/coko/dsl/host/CokoExecutor.kt index 4be8c3db2..54313962b 100644 --- a/codyze-specification-languages/coko/coko-dsl/src/main/kotlin/de/fraunhofer/aisec/codyze/specificationLanguages/coko/dsl/host/CokoExecutor.kt +++ b/codyze-specification-languages/coko/coko-dsl/src/main/kotlin/de/fraunhofer/aisec/codyze/specificationLanguages/coko/dsl/host/CokoExecutor.kt @@ -19,14 +19,18 @@ import de.fraunhofer.aisec.codyze.core.executor.Executor import de.fraunhofer.aisec.codyze.core.timed import de.fraunhofer.aisec.codyze.specificationLanguages.coko.core.CokoBackend import de.fraunhofer.aisec.codyze.specificationLanguages.coko.core.Finding +import de.fraunhofer.aisec.codyze.specificationLanguages.coko.core.dsl.Import import de.fraunhofer.aisec.codyze.specificationLanguages.coko.dsl.CokoConfiguration import de.fraunhofer.aisec.codyze.specificationLanguages.coko.dsl.CokoSarifBuilder import de.fraunhofer.aisec.codyze.specificationLanguages.coko.dsl.CokoScript import io.github.detekt.sarif4k.Run import io.github.oshai.kotlinlogging.KotlinLogging +import java.io.File import java.nio.file.Path +import kotlin.io.path.extension import kotlin.script.experimental.api.* import kotlin.script.experimental.api.SourceCode +import kotlin.script.experimental.host.FileBasedScriptSource import kotlin.script.experimental.host.FileScriptSource import kotlin.script.experimental.host.toScriptSource import kotlin.script.experimental.jvm.baseClassLoader @@ -78,6 +82,8 @@ class CokoExecutor(private val configuration: CokoConfiguration, private val bac /** Contains the class loaders of all evaluated scripts */ private val classLoaders = mutableSetOf() + private val conceptTranslator = ConceptTranslator() + /** Evaluates the given project script [sourceCode] against the given [backend]. */ fun eval( sourceCode: String, @@ -93,7 +99,15 @@ class CokoExecutor(private val configuration: CokoConfiguration, private val bac baseClassLoader: ClassLoader? = null ): ResultWithDiagnostics { val compilationConfiguration = - createJvmCompilationConfigurationFromTemplate() + createJvmCompilationConfigurationFromTemplate { + refineConfiguration { + // the callback called if any of the listed file-level annotations are encountered in + // the compiled script + // the processing is defined by the `handler`, that may return refined configuration + // depending on the annotations + onAnnotations(Import::class, handler = ::configureImportDepsOnAnnotations) + } + } val evaluationConfiguration = createJvmEvaluationConfigurationFromTemplate { implicitReceivers(backend) @@ -121,6 +135,7 @@ class CokoExecutor(private val configuration: CokoConfiguration, private val bac * @return A [SpecEvaluator] object containing the extracted information from all * [specFiles] */ + @Suppress("complexity.CyclomaticComplexMethod") fun compileScriptsIntoSpecEvaluator( backend: CokoBackend, specFiles: List @@ -128,10 +143,16 @@ class CokoExecutor(private val configuration: CokoConfiguration, private val bac var baseClassLoader: ClassLoader? = null val specEvaluator = SpecEvaluator() for (specFile in specFiles) { + val scriptSource = if (specFile.extension == "concepts") { + conceptTranslator.transformConceptFile(specFile) + } else { + FileScriptSource(specFile.toFile()) + } + // compile the script val result = eval( - FileScriptSource(specFile.toFile()), + scriptSource, backend = backend, baseClassLoader = baseClassLoader ) @@ -185,5 +206,40 @@ class CokoExecutor(private val configuration: CokoConfiguration, private val bac } return specEvaluator } + + // The handler that is called during script compilation in order to reconfigure compilation on the + // fly + fun configureImportDepsOnAnnotations( + context: ScriptConfigurationRefinementContext + ): ResultWithDiagnostics { + val annotations = + // If no action is performed, the original configuration should be returned + context.collectedData?.get(ScriptCollectedData.foundAnnotations)?.takeIf { it.isNotEmpty() } + ?: return context.compilationConfiguration.asSuccess() + + val scriptBaseDir = (context.script as? FileBasedScriptSource)?.file?.parentFile + val importedSources = + annotations.flatMap { +// (it as? Import)?.paths?.map { sourceName -> +// FileScriptSource(scriptBaseDir?.resolve(sourceName) ?: File(sourceName)) +// }.orEmpty() + + (it as? Import)?.paths?.mapNotNull { sourceName -> + val file = scriptBaseDir?.resolve(sourceName) ?: File(sourceName).normalize() + if (sourceName.endsWith(".codyze.kts")) { + FileScriptSource(file) + } else if (sourceName.endsWith(".concepts")) { + conceptTranslator.transformConceptFile(file.toPath()) + } else { + null + } + }.orEmpty() + } + + return ScriptCompilationConfiguration(context.compilationConfiguration) { + if (importedSources.isNotEmpty()) importScripts.append(importedSources) + } + .asSuccess() + } } } diff --git a/codyze-specification-languages/coko/coko-dsl/src/main/kotlin/de/fraunhofer/aisec/codyze/specificationLanguages/coko/dsl/host/ConceptTranslator.kt b/codyze-specification-languages/coko/coko-dsl/src/main/kotlin/de/fraunhofer/aisec/codyze/specificationLanguages/coko/dsl/host/ConceptTranslator.kt new file mode 100644 index 000000000..1c4ecca4c --- /dev/null +++ b/codyze-specification-languages/coko/coko-dsl/src/main/kotlin/de/fraunhofer/aisec/codyze/specificationLanguages/coko/dsl/host/ConceptTranslator.kt @@ -0,0 +1,188 @@ +/* + * Copyright (c) 2022, Fraunhofer AISEC. All rights reserved. + * + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ +package de.fraunhofer.aisec.codyze.specificationLanguages.coko.dsl.host + +import de.fraunhofer.aisec.codyze.specificationLanguages.coko.core.dsl.GroupingOp +import java.nio.file.Path +import kotlin.io.path.absolute +import kotlin.io.path.name +import kotlin.script.experimental.host.FileScriptSource +import kotlin.script.experimental.host.StringScriptSource + +class ConceptTranslator { + private val conceptTranslations: MutableMap = mutableMapOf() + + @Suppress("MagicNumber") + fun transformConceptFile(specFile: Path): StringScriptSource { + val absolutePath = specFile.normalize().absolute() + val cachedTranslation = conceptTranslations[absolutePath] + if (cachedTranslation != null) { + return StringScriptSource(cachedTranslation, absolutePath.fileName.name) + } + + val fileScriptSource = FileScriptSource(specFile.toFile()) + + val fileText = fileScriptSource.text + val preliminaryScriptText = fileText + // Remove all comments + // TODO: Is there a way to specify that all Regexes should not include matches found in comments? + .replace(Regex("//.*\\n"), "\n") + // Handle all `op` keywords that represent an operationPointer (`'op' '=' ('|' )*`) + .replace(Regex("\\s+op\\s+.+=.+\\s")) { opPointerMatchResult -> + handleOpPointer(opPointerMatchResult, fileText) + } + + val scriptText = preliminaryScriptText + // Replace all `concept` keywords with `interface` and ensure that the name is capitalized + .replace(Regex("concept\\s+.")) { + makeLastCharUpperCase( + it.value.replace("concept", "interface") + ) + } + // Replace all `enum` keywords with `enum class` and ensure that the name is capitalized + .replace(Regex("enum\\s+.")) { + makeLastCharUpperCase( + it.value.replace("enum", "enum class") + ) + } + // Ensure that all type names are capitalized + .replace(Regex(":\\s*[a-zA-Z]")) { + it.value.uppercase() + } + // Replace all `op` keywords that represent an operation with `fun` and add types for the parameters + .replace(Regex("\\s+op\\s.+\\)\\s?")) { opMatchResult -> + opMatchResult.value + .replace("op", "fun") + .replace(Regex(",( )?.*\\.\\.\\.")) { + it.value.dropLast(3).replace(Regex(",( )?",), ", vararg ") + } + .replace(",", ": Any?,") + .replace(Regex("[^(]\\)")) { + "${it.value.dropLast(1)}: Any?): Op" + } + .plus("\n") + } + // Replace all `var` keywords with `val` and add a type if none is given + .replace(Regex("\\s+var\\s+.+\\s")) { varMatchResult -> + val property = varMatchResult.value.replace("var", "val").dropLast(1) + if (property.contains(':')) { + "$property\n" + } else { + "$property: Any\n" + } + } + + conceptTranslations[absolutePath] = scriptText + return StringScriptSource(scriptText, fileScriptSource.name) + } + + /** + * This translates a match of a `op` keyword that represent an + * operationPointer (`'op' '=' ('|' )*`) + * into a Kotlin function that returns a [GroupingOp]. + * + * Example: + * ``` + * op log = info | warn + * op info(msg) + * op warn(msg) + * ``` + * is translated into + * ``` + * fun log(msg: Any?): GroupingOp = opGroup(info(msg), warn(msg)) + * ``` + */ + private fun handleOpPointer(opPointerMatchResult: MatchResult, fileText: String): String { + val preliminaryResult = opPointerMatchResult.value + // remove the whitespace character at the end of the matchResult + .dropLast(1) + // Replace all `op` keywords with `fun` + .replace("op", "fun") + + // The index of the '{' character that starts the body of the concept that the "op" resides in + val conceptBodyStart = fileText.lastIndexOf('{', opPointerMatchResult.range.first) + // The index of the '}' character that ends the body of the concept that the "op" resides in + val conceptBodyEnd = fileText.indexOf('}', opPointerMatchResult.range.last) + + // The body of the concept as string + val conceptBody = fileText.subSequence(conceptBodyStart, conceptBodyEnd) + + // Split the definition of the operationPointer at the `=` + val (firstHalf, secondHalf) = preliminaryResult.split(Regex("\\s*=\\s*"), limit = 2) + // Split the grouped ops into separate strings + val opNames = secondHalf.split(Regex("\\s*\\|\\s*")) + + val sb = StringBuilder(firstHalf) + + sb.append("(") + // Find the definitions of the ops that are used for this opPointer + val opDefinitions = opNames.map { (Regex("\\s+op\\s+$it\\(.*\\)").find(conceptBody)?.value.orEmpty()) } + // Append parameters needed for the function which are built by combining + // the parameters of the grouped ops + sb.append(buildFunctionParameters(opDefinitions)) + sb.append("): Op = opGroup(") + + // Append calls to ops + val functionCalls = opDefinitions.map { opDefinition -> + // remove the `op` keyword and all `...` + opDefinition.replace(Regex("(\\s+op\\s+)|(\\.\\.\\.)"), "") + } + sb.append(functionCalls.joinToString()) + + sb.append(")\n") + return sb.toString() + } + + /** + * This combines all parameters of the ops in [opDefinitions] into a set of parameters + * that are needed to call all functions representing the ops and combines them into a string. + */ + @Suppress("MagicNumber") + private fun buildFunctionParameters(opDefinitions: List): String { + // Find out all needed parameters + val functionParameters = opDefinitions.flatMap { opDefinition -> + // find the parameters that are used for the op + val opParameters = Regex("\\(.*\\)").find(opDefinition)?.value.orEmpty() + // remove the `(` and `)` and then split the parameters + removeFirstAndLastChar(opParameters).split(Regex("\\s*,\\s*")) + } + .filter { it.isNotEmpty() } + .toSet() + // add types to the parameters + .map { + if (it.endsWith("...")) { + // translate vararg parameters to the correct Kotlin syntax + "vararg ${it.substring(0, it.length - 3)}: Any?" + } else { + "$it: Any?" + } + } + + return functionParameters.joinToString() + } + + private fun makeLastCharUpperCase(string: String): String { + val lastCharAsUpper = string.last().uppercaseChar() + return string.dropLast(1) + lastCharAsUpper + } + + private fun removeFirstAndLastChar(string: String): String = + if (string.isEmpty()) { + string + } else { + string.substring(1, string.length - 1) + } +} diff --git a/codyze-specification-languages/coko/coko-dsl/src/main/resources/concept.g4 b/codyze-specification-languages/coko/coko-dsl/src/main/resources/concept.g4 new file mode 100644 index 000000000..e41f11095 --- /dev/null +++ b/codyze-specification-languages/coko/coko-dsl/src/main/resources/concept.g4 @@ -0,0 +1,69 @@ +grammar concept; +file: (concept | ruleSet | rule | enum)* EOF; + +name: ID | EMPTY_ID; +type: ID; + +concept: 'concept' name conceptBody; +conceptBody: '{' conceptItem* '}'; +conceptItem: variable | operation | operationPointer; +variable: 'var' name (':' type)?; +operationPointer: 'op' name '=' name ('|' name)*; +operation: 'op' name parameterClause; +parameterClause: '(' parameterList? ')'; +parameterList: parameter (',' parameter)*; +parameter: name | name '...'; + +enum: 'enum' name enumBody; +enumBody: '{' name (',' name)* '}'; + +ruleSet: 'ruleset' name ruleSetBody; +ruleSetBody: '{' rule+ '}'; + +rule: 'rule' name ruleBody; +ruleBody: '{' ruleItem* '}'; +ruleItem: ruleVariable | when; + +ruleVariable: 'var' name ':' type; +when: 'when' condition '{' whenBody '}'; +whenBody: assert*; + +assert: assertCall | assertEnsure; + +assertCall: 'call' opReference assertCallLocation?; +assertCallLocation: eogDirection 'in' eogScope; +assertEnsure: 'ensure' booleanExpression; + +eogScope: 'function scope'; // currently, we only support function scope +eogDirection: 'afterwards' | 'before' | 'somewhere'; + +condition: booleanExpression; +expression: + name '.' name parameterClause #callExpression | + expression '.' name #memberExpression | + name #referenceExpression | + literal #literalExpression; +booleanExpression: + lhs op rhs #comparison | + lhs IN array #rangeExpression | + opReference #opExpression | + booleanExpression AND booleanExpression #andExpression; +array: '[' arrayElement (',' arrayElement)* ']'; +arrayElement: literal | name; +lhs: expression; +op: OPERATOR; +rhs: expression; +literal: LITERAL; + +opReference: name '::' (name | WILDCARD) parameterClause; + +AND: 'and'; +OR: 'or'; +IN: 'in'; +WILDCARD: '*'; +LITERAL: [0-9]+; +EMPTY_ID: '_'; // empty identifier +ID : [a-zA-Z]+; // identifier +WS : [ \t\r\n]+ -> skip; // skip spaces, tabs, newlines +OPERATOR: '==' | '<=' | '>=' | '!='; +LINE_COMMENT: '//' ~[\r\n]* -> skip; // skip comments \ No newline at end of file diff --git a/codyze-specification-languages/coko/coko-dsl/src/test/kotlin/de/fraunhofer/aisec/codyze/specificationLanguages/coko/dsl/ConceptTranslationTest.kt b/codyze-specification-languages/coko/coko-dsl/src/test/kotlin/de/fraunhofer/aisec/codyze/specificationLanguages/coko/dsl/ConceptTranslationTest.kt new file mode 100644 index 000000000..13cecd6cd --- /dev/null +++ b/codyze-specification-languages/coko/coko-dsl/src/test/kotlin/de/fraunhofer/aisec/codyze/specificationLanguages/coko/dsl/ConceptTranslationTest.kt @@ -0,0 +1,167 @@ +/* + * Copyright (c) 2022, Fraunhofer AISEC. All rights reserved. + * + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ +package de.fraunhofer.aisec.codyze.specificationLanguages.coko.dsl + +import de.fraunhofer.aisec.codyze.backends.cpg.CPGConfiguration +import de.fraunhofer.aisec.codyze.backends.cpg.coko.CokoCpgBackend +import de.fraunhofer.aisec.codyze.specificationLanguages.coko.dsl.host.CokoExecutor +import de.fraunhofer.aisec.cpg.passes.EdgeCachePass +import de.fraunhofer.aisec.cpg.passes.UnreachableEOGPass +import org.junit.jupiter.api.Assertions.assertFalse +import org.junit.jupiter.api.Test +import kotlin.io.path.Path +import kotlin.test.assertEquals +import kotlin.test.assertNotNull +import kotlin.test.assertTrue + +class ConceptTranslationTest { + + private val sourceFiles = listOfNotNull( + CokoCpgIntegrationTest::class.java.classLoader + .getResource("IntegrationTests/CokoCpg/Main.java"), + CokoCpgIntegrationTest::class.java.classLoader + .getResource("IntegrationTests/CokoCpg/SimpleOrder.java") + ).map { Path(it.path) }.also { assertEquals(2, it.size) } + + val cpgConfiguration = + CPGConfiguration( + source = sourceFiles, + useUnityBuild = false, + debugParser = false, + disableCleanup = false, + codeInNodes = true, + matchCommentsToNodes = false, + processAnnotations = false, + failOnError = false, + useParallelFrontends = false, + defaultPasses = true, + additionalLanguages = setOf(), + symbols = mapOf(), + includeBlocklist = listOf(), + includePaths = listOf(), + includeAllowlist = listOf(), + loadIncludes = false, + passes = listOf(UnreachableEOGPass::class, EdgeCachePass::class), + ) + + @Test + fun `test simple concept translation`() { + val specFiles = listOfNotNull( + CokoCpgIntegrationTest::class.java.classLoader + .getResource("concept/bsi-tr.concepts"), + ).map { Path(it.path) } + + val cokoConfiguration = + CokoConfiguration( + goodFindings = true, + pedantic = false, + spec = specFiles, + disabledSpecRules = emptyList(), + ) + + val backend = CokoCpgBackend(cpgConfiguration) + val specEvaluator = CokoExecutor.compileScriptsIntoSpecEvaluator(backend, specFiles) + + val expectedInterfaceToExpectedMembers = mapOf( + "Cypher" to listOf("algo", "mode", "keySize", "tagSize"), + "InitializationVector" to listOf("size"), + "Encryption" to listOf("cypher", "iv", "encrypt", "decrypt") + ) + + assertEquals(expectedInterfaceToExpectedMembers.size, specEvaluator.types.size) + + for ((expectedInterface, members) in expectedInterfaceToExpectedMembers) { + val actualInterfaces = specEvaluator.types.filter { it.simpleName?.contains(expectedInterface) ?: false } + assertEquals( + 1, + actualInterfaces.size, + "Found none or more than one actual interface representing the concept \"$expectedInterface\"" + ) + val actualInterface = actualInterfaces.first() + + assertTrue(actualInterface.members.map { it.name }.containsAll(members)) + } + } + + @Test + fun `test concept translation with op pointer`() { + val specFiles = listOfNotNull( + CokoCpgIntegrationTest::class.java.classLoader + .getResource("concept/some.concepts"), + ).map { Path(it.path) } + + val cokoConfiguration = + CokoConfiguration( + goodFindings = true, + pedantic = false, + spec = specFiles, + disabledSpecRules = emptyList(), + ) + + val backend = CokoCpgBackend(cpgConfiguration) + val specEvaluator = CokoExecutor.compileScriptsIntoSpecEvaluator(backend, specFiles) + + val expectedInterfaceToExpectedMembers = mapOf( + "Logging" to listOf("log", "info", "warn", "error"), + "Database" to listOf("init", "insert"), + "UserContext" to listOf("user") + ) + + assertEquals(3, specEvaluator.types.size) + for ((expectedInterface, members) in expectedInterfaceToExpectedMembers) { + val actualInterfaces = specEvaluator.types.filter { it.simpleName?.contains(expectedInterface) ?: false } + assertEquals( + 1, + actualInterfaces.size, + "Found none or more than one actual interface representing the concept \"$expectedInterface\"" + ) + val actualInterface = actualInterfaces.first() + assertTrue(actualInterface.members.map { it.name }.containsAll(members)) + + if (expectedInterface == "Logging") { + val log = actualInterface.members.firstOrNull { it.name == "log" } + assertNotNull(log) + assertFalse(log.isAbstract) + } + } + } + + @Test + fun `test concept in combination with coko scripts`() { + val specFiles = listOfNotNull( + CokoCpgIntegrationTest::class.java.classLoader + .getResource("concept/followedBy.concepts"), + CokoCpgIntegrationTest::class.java.classLoader + .getResource("concept/followedByImplementations.codyze.kts"), + CokoCpgIntegrationTest::class.java.classLoader + .getResource("concept/followedByRule.codyze.kts"), + ).map { Path(it.path) } + + val cokoConfiguration = + CokoConfiguration( + goodFindings = true, + pedantic = false, + spec = specFiles, + disabledSpecRules = emptyList(), + ) + + val backend = CokoCpgBackend(cpgConfiguration) + val executor = CokoExecutor(cokoConfiguration, backend) + + val run = executor.evaluate() + assertEquals(1, run.results?.size) + } +} diff --git a/codyze-specification-languages/coko/coko-dsl/src/test/kotlin/de/fraunhofer/aisec/codyze/specificationLanguages/coko/dsl/WheneverEvaluatorTest.kt b/codyze-specification-languages/coko/coko-dsl/src/test/kotlin/de/fraunhofer/aisec/codyze/specificationLanguages/coko/dsl/WheneverEvaluatorTest.kt new file mode 100644 index 000000000..5b5255a56 --- /dev/null +++ b/codyze-specification-languages/coko/coko-dsl/src/test/kotlin/de/fraunhofer/aisec/codyze/specificationLanguages/coko/dsl/WheneverEvaluatorTest.kt @@ -0,0 +1,86 @@ +/* + * Copyright (c) 2022, Fraunhofer AISEC. All rights reserved. + * + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ +package de.fraunhofer.aisec.codyze.specificationLanguages.coko.dsl + +import de.fraunhofer.aisec.codyze.backends.cpg.CPGConfiguration +import de.fraunhofer.aisec.codyze.backends.cpg.coko.CokoCpgBackend +import de.fraunhofer.aisec.codyze.specificationLanguages.coko.dsl.host.CokoExecutor +import de.fraunhofer.aisec.cpg.passes.EdgeCachePass +import de.fraunhofer.aisec.cpg.passes.UnreachableEOGPass +import io.github.detekt.sarif4k.ResultKind +import org.junit.jupiter.api.Test +import kotlin.io.path.Path +import kotlin.test.assertEquals + +// TODO: should probably in codyze-backends or coko-core +class WheneverEvaluatorTest { + + private val sourceFiles = listOfNotNull( + CokoCpgIntegrationTest::class.java.classLoader + .getResource("concept/CipherTestFile.java"), + ).map { Path(it.path) }.also { assertEquals(1, it.size) } + + val cpgConfiguration = + CPGConfiguration( + source = sourceFiles, + useUnityBuild = false, + debugParser = false, + disableCleanup = false, + codeInNodes = true, + matchCommentsToNodes = false, + processAnnotations = false, + failOnError = false, + useParallelFrontends = false, + defaultPasses = true, + additionalLanguages = setOf(), + symbols = mapOf(), + includeBlocklist = listOf(), + includePaths = listOf(), + includeAllowlist = listOf(), + loadIncludes = false, + passes = listOf(UnreachableEOGPass::class, EdgeCachePass::class), + ) + + /** + * Performs an end-to-end integration test of Codyze with the [CokoExecutor] and the [CokoCpgBackend] backend. + */ + @Test + fun `test coko with cpg backend and multiple spec files`() { + val specFiles = listOfNotNull( + CokoCpgIntegrationTest::class.java.classLoader + .getResource("concept/bsi-tr-rules.codyze.kts"), + CokoCpgIntegrationTest::class.java.classLoader + .getResource("concept/jca-cipher.codyze.kts") + ).map { Path(it.path) }.also { assertEquals(2, it.size) } + + val cokoConfiguration = + CokoConfiguration( + goodFindings = true, + pedantic = false, + spec = specFiles, + disabledSpecRules = emptyList(), + ) + + val backend = CokoCpgBackend(cpgConfiguration) + val executor = CokoExecutor(cokoConfiguration, backend) + + val run = executor.evaluate() + + // assertions for the order rule + assertEquals(1, run.results?.size, "Expected to find one result but was ${run.results?.size}") + assertEquals(ResultKind.Fail, run.results?.firstOrNull()?.kind, "Result was not fail") + } +} diff --git a/codyze-specification-languages/coko/coko-dsl/src/test/resources/concept/CipherTestFile.java b/codyze-specification-languages/coko/coko-dsl/src/test/resources/concept/CipherTestFile.java new file mode 100644 index 000000000..41e212c97 --- /dev/null +++ b/codyze-specification-languages/coko/coko-dsl/src/test/resources/concept/CipherTestFile.java @@ -0,0 +1,39 @@ +import java.security.InvalidAlgorithmParameterException; +import java.security.InvalidKeyException; +import java.security.Key; +import java.security.NoSuchAlgorithmException; +import java.security.NoSuchProviderException; +import java.security.SecureRandom; +import java.security.Security; +import java.security.spec.InvalidKeySpecException; + +import javax.crypto.Cipher; +import javax.crypto.NoSuchPaddingException; +import javax.crypto.SecretKeyFactory; +import javax.crypto.spec.IvParameterSpec; +import javax.crypto.spec.SecretKeySpec; + +import org.bouncycastle.jce.provider.BouncyCastleProvider; + +public class CipherTestFile { + + public static void main(String[] args) throws NoSuchAlgorithmException, NoSuchProviderException, NoSuchPaddingException, InvalidKeySpecException, InvalidKeyException, InvalidAlgorithmParameterException { + Security.addProvider(new BouncyCastleProvider()); + + String transform = "AES/CBC/NoPadding"; + Cipher c = Cipher.getInstance(transform, "BC"); + + SecureRandom sr = new SecureRandom(); + byte[] iv = sr.generateSeed(16); + IvParameterSpec ivParamSpec = new IvParameterSpec(iv); + + byte[] rawKey = sr.generateSeed(32); + SecretKeyFactory skf = SecretKeyFactory.getInstance("AES"); + Key k = skf.generateSecret(new SecretKeySpec(rawKey, "AES")); + + c.init(Cipher.ENCRYPT_MODE, k, ivParamSpec); + c.doFinal(); + System.out.println(c); + } + +} diff --git a/codyze-specification-languages/coko/coko-dsl/src/test/resources/concept/bsi-tr-rules.codyze.kts b/codyze-specification-languages/coko/coko-dsl/src/test/resources/concept/bsi-tr-rules.codyze.kts new file mode 100644 index 000000000..6b66258e6 --- /dev/null +++ b/codyze-specification-languages/coko/coko-dsl/src/test/resources/concept/bsi-tr-rules.codyze.kts @@ -0,0 +1,56 @@ +//@file:Import("bsi-tr.concepts") + +import de.fraunhofer.aisec.codyze.specificationLanguages.coko.core.modelling.DataItem + +enum class Algorithm { + AES, DES, TripleDES +} + +enum class Mode { + // Cipher Block Chaining Message Authentication + CCM, + // Galois/Counter Mode + GCM, + // Cipher Block Chaining + CBC, + // Counter Mode + CTR +} + +interface Cypher { + val algo: DataItem + val mode: DataItem + val keySize: DataItem // in bits + val tagSize: DataItem // in bits; only applicable for mode == CCM +} + +interface InitializationVector { + val size: Int // in bits +} + +interface Encryption { + val cypher: Cypher + val iv: InitializationVector + + fun encrypt(plaintext: Any?): Op + fun decrypt(ciphertext: Any?): Op +} + + +//@RuleSet +//class GoodCrypto { + @Rule + fun `must be AES`(enc: Encryption) = + whenever({ call(enc.encrypt(Wildcard)) }) { + ensure { enc.cypher.algo eq Algorithm.AES } + ensure { enc.cypher.mode within list[Mode.CCM, Mode.GCM, Mode.CTR] } +// ensure { enc.cypher.keySize within list[128, 192, 256]} + } + +// @Rule +// fun `modes of operation`(enc: Encryption) = +// whenever({ call(enc.encrypt(Wildcard)) and (enc.cypher.mode eq Mode.CCM) }) { +// ensure { enc.cypher.tagSize geq 96 } +// } +//} + diff --git a/codyze-specification-languages/coko/coko-dsl/src/test/resources/concept/bsi-tr.concepts b/codyze-specification-languages/coko/coko-dsl/src/test/resources/concept/bsi-tr.concepts new file mode 100644 index 000000000..0431eacaf --- /dev/null +++ b/codyze-specification-languages/coko/coko-dsl/src/test/resources/concept/bsi-tr.concepts @@ -0,0 +1,66 @@ +// This concepts file provides a ruleset about "Good Crypto", which we should be able to +// reference in some other concept file + +enum Algorithm { + AES, DES, TripleDES +} + +enum Mode { + // Cipher Block Chaining Message Authentication + CCM, + // Galois/Counter Mode + GCM, + // Cipher Block Chaining + CBC, + // Counter Mode + CTR +} + +concept Cypher { + var algo: Algorithm + var mode: Mode + var keySize: int // in bits + var tagSize: int // in bits; only applicable for mode == CCM +} + +concept InitializationVector { + var size: int // in bits +} + +concept Encryption { + var cypher: Cypher + var iv: InitializationVector + + op encrypt(plaintext) + op decrypt(ciphertext) +} + +//ruleset GoodCrypto { +// // Relates to 2.1.1 Betriebsarten +// rule MustBeAES { +// var enc: Encryption +// +// when enc::encrypt(_) { +// ensure enc.cypher.algo == AES +// ensure enc.cypher.mode in [CCM, GCM, CTR] +// ensure enc.cypher.keySize in [128, 192, 256] +// } +// } +// +// // Relates to 2.1.2 Betriebsbedingungen - CCM +// rule ModesOfOperation { +// var enc: Encryption +// +// when enc::encrypt(_) and enc.cypher.mode == CCM { +// ensure enc.cypher.tagSize >= 96 +// } +// +// when enc::encrypt(_) and enc.cypher.mode == GCM { +// ensure enc.iv.size >= 96 +// } +// +// when enc::encrypt(_) and enc.cypher.mode in [CCM, GCM, CTR] { +// // TODO: iv should not repeat itself +// } +// } +//} \ No newline at end of file diff --git a/codyze-specification-languages/coko/coko-dsl/src/test/resources/concept/followedBy.concepts b/codyze-specification-languages/coko/coko-dsl/src/test/resources/concept/followedBy.concepts new file mode 100644 index 000000000..d94727678 --- /dev/null +++ b/codyze-specification-languages/coko/coko-dsl/src/test/resources/concept/followedBy.concepts @@ -0,0 +1,11 @@ +concept LoggingForTest { + op log(msg, args...) +} + +concept ObjectRelationalMapperForTest { + op insert(obj) +} + +concept UserContextForTest { + var user +} diff --git a/codyze-specification-languages/coko/coko-dsl/src/test/resources/concept/followedByImplementations.codyze.kts b/codyze-specification-languages/coko/coko-dsl/src/test/resources/concept/followedByImplementations.codyze.kts new file mode 100644 index 000000000..112ec3b1d --- /dev/null +++ b/codyze-specification-languages/coko/coko-dsl/src/test/resources/concept/followedByImplementations.codyze.kts @@ -0,0 +1,33 @@ +@file:Import("followedBy.concepts") + +plugins { id("cpg") } + +class JavaLoggingTest : LoggingForTest { + override fun log(message: Any?, vararg args: Any?) = op { + definition("java.util.logging.Logger.info") { + signature { + group { + - message + args.forEach { - it } + } + } + } + } +} + +class JDBCTest : ObjectRelationalMapperForTest { + override fun insert(obj: Any?) = op { + definition("java.sql.Statement.executeUpdate") { + signature { + group { + - "INSERT.*" + - obj + } + } + } + } +} + +class JavalinJWTTest : UserContextForTest { + override val user = cpgCallFqn("javalinjwt.JavalinJWT.getTokenFromHeader") +} diff --git a/codyze-specification-languages/coko/coko-dsl/src/test/resources/concept/followedByRule.codyze.kts b/codyze-specification-languages/coko/coko-dsl/src/test/resources/concept/followedByRule.codyze.kts new file mode 100644 index 000000000..c931cccac --- /dev/null +++ b/codyze-specification-languages/coko/coko-dsl/src/test/resources/concept/followedByRule.codyze.kts @@ -0,0 +1,6 @@ +@file:Import("followedBy.concepts") + +// TODO: can we "assert" that the ctx.user is not null here? +@Rule("This is a dummy description.") +fun DBActionsAreAlwaysLogged(db: ObjectRelationalMapperForTest, log: LoggingForTest, ctx: UserContextForTest) = + db.insert(Wildcard) followedBy log.log(".*", ctx.user) \ No newline at end of file diff --git a/codyze-specification-languages/coko/coko-dsl/src/test/resources/concept/jca-cipher.codyze.kts b/codyze-specification-languages/coko/coko-dsl/src/test/resources/concept/jca-cipher.codyze.kts new file mode 100644 index 000000000..05460b971 --- /dev/null +++ b/codyze-specification-languages/coko/coko-dsl/src/test/resources/concept/jca-cipher.codyze.kts @@ -0,0 +1,103 @@ +@file:Import("bsi-tr-rules.codyze.kts") + +import de.fraunhofer.aisec.codyze.specificationLanguages.coko.core.modelling.BackendDataItem +import de.fraunhofer.aisec.codyze.specificationLanguages.coko.core.modelling.DataItem +import de.fraunhofer.aisec.codyze.specificationLanguages.coko.core.modelling.value + +class JCACipher { + fun getInstance(transformation: Any, provider: Any? = null) = op { + // TODO: Change back to "javax.crypto.Cipher.getInstance" when CPG resolves names correctly + "Cipher.getInstance" { + signature(transformation) + signature(transformation, provider) + } + } + + fun init(opmode: Any, certificate: Any?, random: Any?, key: Any?, params: Any?) = op { + "javax.crypto.Cipher.init" { + signature(opmode, certificate) + signature(opmode, certificate, random) + signature(opmode, key) + signature(opmode, key, params) + signature(opmode, key, params, random) + signature(opmode, key, random) + + } + } + + fun doFinal(input: Any?, output: Any?, outputOffset: Any?, inputOffset: Any?, inputLen: Any?) = op { + "javax.crypto.Cipher.doFinal" { + signature() + signature(input) + signature(output, outputOffset) + signature(input, inputOffset, inputLen) + signature(input, inputOffset, inputLen, output) + signature(input, inputOffset, inputLen, output, outputOffset) + signature(input, output) + } + } +} + +class JCAEncryptionImpl: Bsi_tr_rules_codyze.Encryption { + private val jcaCipher = JCACipher() + override val cypher: Bsi_tr_rules_codyze.Cypher + get() = JCACipherImpl() + override val iv: Bsi_tr_rules_codyze.InitializationVector + get() = TODO("Not yet implemented") + + override fun encrypt(plaintext: Any?): Op = + jcaCipher.doFinal(plaintext, Wildcard, Wildcard, Wildcard, Wildcard) with + jcaCipher.init(".*ENCRYPT_MODE", Wildcard, Wildcard, Wildcard, Wildcard) + + override fun decrypt(ciphertext: Any?): Op { + TODO("Not yet implemented") + } + +} + +// "AES/CBC/Padding" +class JCACipherImpl: Bsi_tr_rules_codyze.Cypher { + val cipher = JCACipher() + + override val algo: DataItem + get() = cipher.getInstance(Wildcard, Wildcard).arguments[0] withTransformation { dataItem -> + transformTransformationString(dataItem, 0, "an algorithm") { string -> + Bsi_tr_rules_codyze.Algorithm.entries.firstOrNull { it.name == string.uppercase() } + } + } + override val mode: DataItem + get() = cipher.getInstance(Wildcard, Wildcard).arguments[0] withTransformation { dataItem -> + transformTransformationString(dataItem, 1, "a mode") { string -> + Bsi_tr_rules_codyze.Mode.entries.firstOrNull { it.name == string.uppercase() } + } + } + override val keySize: DataItem + get() = value(1) + override val tagSize: DataItem + get() = value(1) + + + fun transformTransformationString( + dataItem: BackendDataItem, + index: Int, + errorMessage: String, + stringToResult: (String) -> E?): TransformationResult { + val stringValue = dataItem.value as? String + return if(dataItem.value == null) + TransformationResult.failure("Value of BackendDataItem is null.") + else if(stringValue == null) { + TransformationResult.failure("Value of BackendDataItem is not a string.") + } + else { + val string = stringValue.split('/')[index] + val result = stringToResult(string) + if(result == null) + TransformationResult.failure("Could not resolve the string value to $errorMessage") + else + TransformationResult.success(result) + } + } +} + + + diff --git a/codyze-specification-languages/coko/coko-dsl/src/test/resources/concept/rpc.concepts b/codyze-specification-languages/coko/coko-dsl/src/test/resources/concept/rpc.concepts new file mode 100644 index 000000000..f2d9a86c2 --- /dev/null +++ b/codyze-specification-languages/coko/coko-dsl/src/test/resources/concept/rpc.concepts @@ -0,0 +1,14 @@ +concept Request {} + +concept Validation { + op validate(obj) +} + +//rule AlwaysValidate { +// var req: Request +// var v: Validation +// +// when req::*() { +// call v::validate(req) before in function scope +// } +//} \ No newline at end of file diff --git a/codyze-specification-languages/coko/coko-dsl/src/test/resources/concept/some.concepts b/codyze-specification-languages/coko/coko-dsl/src/test/resources/concept/some.concepts new file mode 100644 index 000000000..137351cf7 --- /dev/null +++ b/codyze-specification-languages/coko/coko-dsl/src/test/resources/concept/some.concepts @@ -0,0 +1,25 @@ +concept Logging { + op log = info | warn | error + op info(msg, args...) + op warn(msg, args...) + op error(msg, args...) +} + +concept Database { + op init() + op insert(obj) +} + +concept UserContext { + var user +} + +//rule AuditLog { +// var db: Database +// var ctx: UserContext +// var log: Logging + +// when db::insert(x) { +// call log::log(_, ctx) afterwards in function scope +// } +//} \ No newline at end of file