Skip to content

Introduce utbot taint analysis #1966

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 8 commits into from
Jun 9, 2023
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion .github/workflows/framework-tests-matrix.json
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@
},
{
"PART_NAME": "composite-part2",
"TESTS_TO_RUN": "--tests \"org.utbot.engine.*\" --tests \"org.utbot.framework.*\" --tests \"org.utbot.sarif.*\""
"TESTS_TO_RUN": "--tests \"org.utbot.engine.*\" --tests \"org.utbot.framework.*\" --tests \"org.utbot.sarif.*\" --tests \"org.utbot.examples.taint.*\""
},
{
"PART_NAME": "composite-part3",
Expand Down
5 changes: 3 additions & 2 deletions gradle.properties
Original file line number Diff line number Diff line change
Expand Up @@ -60,8 +60,9 @@ kryoVersion=5.4.0
kryoSerializersVersion=0.45
asmVersion=9.2
testNgVersion=7.6.0
kamlVersion = 0.51.0
jacksonVersion = 2.12.3
kamlVersion=0.51.0
jacksonVersion=2.12.3
kotlinxSerializationVersion=1.5.0
slf4jVersion=1.7.36
eclipseAetherVersion=1.1.0
mavenWagonVersion=3.5.1
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -153,6 +153,13 @@ class UtExpressionStructureCounter(private val input: Iterable<UtExpression>) :
return stat
}

override fun visit(expr: UtBvNotExpression): NestStat {
val stat = buildState(expr.variable.expr)
stat.level++
stat.nodes++
return stat
}

override fun visit(expr: UtCastExpression): NestStat {
val stat = buildState(expr.variable.expr)
stat.level++
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -265,6 +265,30 @@ object UtSettings : AbstractSettings(logger, defaultKeyForSettingsPath, defaultS
DEFAULT_EXECUTION_TIMEOUT_IN_INSTRUMENTED_PROCESS_MS
)

/**
* Enable taint analysis or not.
*/
var useTaintAnalysis by getBooleanProperty(false)

/**
* If it is true, [Traverser] forks the state and creates checks for each taint mark separately,
* otherwise, it processes all available taint marks in one [Traverser.implicitlyThrowException] request.
*
* @see [org.utbot.engine.Traverser.processTaintSink]
*/
var throwTaintErrorForEachMarkSeparately = true

/**
* How deep we should analyze the throwables.
*/
val exploreThrowableDepth: ExploreThrowableDepth
get() =
if (useTaintAnalysis) {
ExploreThrowableDepth.EXPLORE_ALL_STATEMENTS
} else {
ExploreThrowableDepth.SKIP_ALL_STATEMENTS
}

// region engine process debug

/**
Expand Down Expand Up @@ -680,3 +704,24 @@ enum class SummariesGenerationType {
*/
NONE,
}

/**
* Enum to describe how deep we should analyze the throwables.
*/
enum class ExploreThrowableDepth {

/**
* Skip all statements between throwable's `new` and `<init>` statements.
*/
SKIP_ALL_STATEMENTS,

/**
* Skip only throwable's <init> statement.
*/
SKIP_INIT_STATEMENT,

/**
* Do not skip statements.
*/
EXPLORE_ALL_STATEMENTS
}
Original file line number Diff line number Diff line change
Expand Up @@ -65,6 +65,7 @@ import org.utbot.framework.plugin.api.util.isSubtypeOf
import org.utbot.framework.plugin.api.util.utContext
import org.utbot.framework.process.OpenModulesContainer
import soot.SootField
import soot.SootMethod

const val SYMBOLIC_NULL_ADDR: Int = 0

Expand Down Expand Up @@ -101,6 +102,17 @@ data class Step(
}
}

/**
* One symbolic step.
*
* @see UtSymbolicExecution.symbolicSteps
*/
data class SymbolicStep(
val method: SootMethod,
val lineNumber: Int,
val callDepth: Int,
)


/**
* Traverse result.
Expand Down Expand Up @@ -150,7 +162,8 @@ class UtSymbolicExecution(
coverage: Coverage? = null,
summary: List<DocStatement>? = null,
testMethodName: String? = null,
displayName: String? = null
displayName: String? = null,
/** Convenient view of the full symbolic path */ val symbolicSteps: List<SymbolicStep> = listOf(),
) : UtExecution(stateBefore, stateAfter, result, coverage, summary, testMethodName, displayName) {
/**
* By design the 'before' and 'after' states contain info about the same fields.
Expand Down Expand Up @@ -201,7 +214,8 @@ class UtSymbolicExecution(
coverage,
summary,
testMethodName,
displayName
displayName,
symbolicSteps,
)
}
}
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -15,4 +15,17 @@ sealed class ArtificialError(message: String): Error(message)
*
* See [TraversalContext.intOverflowCheck] for more details.
*/
class OverflowDetectionError(message: String): ArtificialError(message)
class OverflowDetectionError(message: String): ArtificialError(message)

/**
* An artificial error that could be implicitly thrown by the symbolic engine during taint sink processing.
*/
class TaintAnalysisError(
/** Sink method name: "${classId.simpleName}.${methodId.name}". */
val sinkName: String,
/** Some information about a tainted var, for example, its type. */
val taintedVar: String,
/** Name of the taint mark. */
val taintMark: String,
message: String = "'$taintedVar' marked '$taintMark' was passed into '$sinkName' method"
) : ArtificialError(message)
Original file line number Diff line number Diff line change
Expand Up @@ -23,6 +23,10 @@ data class UtOverflowFailure(
override val exception: Throwable,
) : UtExecutionFailure()

data class UtTaintAnalysisFailure(
override val exception: Throwable
) : UtExecutionFailure()

data class UtSandboxFailure(
override val exception: Throwable
) : UtExecutionFailure()
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -545,6 +545,9 @@ val ExecutableId.humanReadableName: String
return "$executableName($parameters)"
}

val ExecutableId.simpleNameWithClass: String
get() = "${classId.simpleName}.${name}"

val Constructor<*>.displayName: String
get() = executableId.humanReadableName

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -59,6 +59,16 @@ inline fun <reified T> withTreatingOverflowAsError(block: () -> T): T {
}
}

inline fun <reified T> withoutThrowTaintErrorForEachMarkSeparately(block: () -> T): T {
val prev = UtSettings.throwTaintErrorForEachMarkSeparately
UtSettings.throwTaintErrorForEachMarkSeparately = false
try {
return block()
} finally {
UtSettings.throwTaintErrorForEachMarkSeparately = prev
}
}

inline fun <reified T> withPushingStateFromPathSelectorForConcrete(block: () -> T): T {
val prev = UtSettings.saveRemainingStatesForConcreteExecution
UtSettings.saveRemainingStatesForConcreteExecution = true
Expand Down
Original file line number Diff line number Diff line change
@@ -0,0 +1,31 @@
package org.utbot.examples.taint

import org.junit.jupiter.api.Test
import org.utbot.framework.plugin.api.TaintAnalysisError
import org.utbot.taint.TaintConfigurationProviderResources
import org.utbot.testcheckers.eq
import org.utbot.testing.UtValueTestCaseCheckerForTaint
import org.utbot.testing.isException

internal class TaintBranchingTest : UtValueTestCaseCheckerForTaint(
testClass = TaintBranching::class,
taintConfigurationProvider = TaintConfigurationProviderResources("taint/TaintBranchingConfig.yaml")
) {
@Test
fun testTaintBad() {
checkWithException(
TaintBranching::bad,
eq(3), // success (x2) & taint error
{ cond, r -> cond == r.isException<TaintAnalysisError>() },
)
}

@Test
fun testTaintGood() {
checkWithException(
TaintBranching::good,
eq(2), // success in both cases
{ _, r -> r.isSuccess },
)
}
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,70 @@
package org.utbot.examples.taint

import org.junit.jupiter.api.Test
import org.utbot.framework.plugin.api.TaintAnalysisError
import org.utbot.taint.TaintConfigurationProviderResources
import org.utbot.testcheckers.eq
import org.utbot.testing.UtValueTestCaseCheckerForTaint
import org.utbot.testing.isException

internal class TaintCleanerConditionsTest : UtValueTestCaseCheckerForTaint(
testClass = TaintCleanerConditions::class,
taintConfigurationProvider = TaintConfigurationProviderResources("taint/TaintCleanerConditionsConfig.yaml")
) {
@Test
fun testTaintBadArg() {
checkWithException(
TaintCleanerConditions::badArg,
eq(2), // success & taint error
{ r -> r.isException<TaintAnalysisError>() },
{ r -> r.isSuccess },
)
}

@Test
fun testTaintBadReturn() {
checkWithException(
TaintCleanerConditions::badReturn,
eq(2), // success & taint error
{ r -> r.isException<TaintAnalysisError>() },
{ r -> r.isSuccess },
)
}

@Test
fun testTaintBadThis() {
checkWithException(
TaintCleanerConditions::badThis,
eq(2), // success & taint error
{ r -> r.isException<TaintAnalysisError>() },
{ r -> r.isSuccess },
)
}

@Test
fun testTaintGoodArg() {
checkWithException(
TaintCleanerConditions::goodArg,
eq(1), // only success
{ r -> r.isSuccess },
)
}

@Test
fun testTaintGoodReturn() {
checkWithException(
TaintCleanerConditions::goodReturn,
eq(1), // only success
{ r -> r.isSuccess },
)
}

@Test
fun testTaintGoodThis() {
checkWithException(
TaintCleanerConditions::goodThis,
eq(1), // only success
{ r -> r.isSuccess },
)
}
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,32 @@
package org.utbot.examples.taint

import org.junit.jupiter.api.Test
import org.utbot.framework.plugin.api.TaintAnalysisError
import org.utbot.taint.TaintConfigurationProviderResources
import org.utbot.testcheckers.eq
import org.utbot.testing.UtValueTestCaseCheckerForTaint
import org.utbot.testing.isException

internal class TaintCleanerSimpleTest : UtValueTestCaseCheckerForTaint(
testClass = TaintCleanerSimple::class,
taintConfigurationProvider = TaintConfigurationProviderResources("taint/TaintCleanerSimpleConfig.yaml")
) {
@Test
fun testTaintBad() {
checkWithException(
TaintCleanerSimple::bad,
eq(2), // success & taint error
{ r -> r.isException<TaintAnalysisError>() },
{ r -> r.isSuccess },
)
}

@Test
fun testTaintGood() {
checkWithException(
TaintCleanerSimple::good,
eq(1), // only success
{ r -> r.isSuccess },
)
}
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,32 @@
package org.utbot.examples.taint

import org.junit.jupiter.api.Test
import org.utbot.framework.plugin.api.TaintAnalysisError
import org.utbot.taint.TaintConfigurationProviderResources
import org.utbot.testcheckers.eq
import org.utbot.testing.UtValueTestCaseCheckerForTaint
import org.utbot.testing.isException

internal class TaintLongPathTest : UtValueTestCaseCheckerForTaint(
testClass = TaintLongPath::class,
taintConfigurationProvider = TaintConfigurationProviderResources("taint/TaintLongPathConfig.yaml")
) {
@Test
fun testTaintBad() {
checkWithException(
TaintLongPath::bad,
eq(2), // success & taint error
{ r -> r.isException<TaintAnalysisError>() },
{ r -> r.isSuccess },
)
}

@Test
fun testTaintGood() {
checkWithException(
TaintLongPath::good,
eq(1), // only success
{ r -> r.isSuccess },
)
}
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,32 @@
package org.utbot.examples.taint

import org.junit.jupiter.api.Test
import org.utbot.framework.plugin.api.TaintAnalysisError
import org.utbot.taint.TaintConfigurationProviderResources
import org.utbot.testcheckers.eq
import org.utbot.testing.UtValueTestCaseCheckerForTaint
import org.utbot.testing.isException

internal class TaintOtherClassTest : UtValueTestCaseCheckerForTaint(
testClass = TaintOtherClass::class,
taintConfigurationProvider = TaintConfigurationProviderResources("taint/TaintOtherClassConfig.yaml")
) {
@Test
fun testTaintBad() {
checkWithException(
TaintOtherClass::bad,
eq(2), // success & taint error
{ r -> r.isException<TaintAnalysisError>() },
{ r -> r.isSuccess },
)
}

@Test
fun testTaintGood() {
checkWithException(
TaintOtherClass::good,
eq(1), // only success
{ r -> r.isSuccess },
)
}
}
Loading