Demo

build.gradle.kts

@@ -8,7 +8,7 @@ plugins {
 }
 
 group = "org.byteflow"
-version = "0.1.0-SNAPSHOT"
+version = "0.1.1-SNAPSHOT"
 
 subprojects {
     group = rootProject.group

buildSrc/src/main/kotlin/Dependencies.kt

@@ -87,13 +87,30 @@ object Libs {
         name = "jacodb-analysis",
         version = Versions.jacodb
     )
+    val jacodb_approximations = dep(
+        group = jacodb,
+        name = "jacodb-approximations",
+        version = Versions.jacodb
+    )
 
     // https://github.com/detekt/sarif4k
     val sarif4k = dep(
         group = "io.github.detekt.sarif4k",
         name = "sarif4k",
         version = Versions.sarif4k
     )
+
+    val ksmt_core = dep(
+        group ="io.ksmt",
+        name = "ksmt-core",
+        version = "0.5.7"
+    )
+
+    val ksmt_z3 = dep(
+        group ="io.ksmt",
+        name = "ksmt-z3",
+        version = "0.5.7"
+    )
 }
 
 /**

byteflow-core/build.gradle.kts

@@ -2,13 +2,56 @@ plugins {
     `maven-publish`
 }
 
+val dist = projectDir.resolve("dist")
+val usvmJar = dist.resolve("usvm-jvm-all.jar")
+val usvmApiJar = dist.resolve("usvm-api.jar")
+
+val `usvm-approximations` by configurations.creating
+
+val examples by sourceSets.creating {
+    java {
+        srcDir("src/examples/java")
+    }
+}
+
 dependencies {
     api(Libs.jacodb_api)
     api(Libs.jacodb_core)
     api(Libs.jacodb_analysis)
+    api(Libs.jacodb_approximations)
+
     implementation(Libs.kotlinx_coroutines_core)
+    implementation(kotlin("reflect"))
 
     implementation(Libs.kotlin_logging)
+
+    implementation(Libs.ksmt_core)
+    implementation(Libs.ksmt_z3)
+
+    implementation(files(usvmJar))
+    `usvm-approximations`("com.github.UnitTestBot.java-stdlib-approximations:approximations:c992f31c14")
+
+    testImplementation(examples.output)
+}
+
+tasks.withType<ProcessResources> {
+    into("/approximations") {
+        `usvm-approximations`.resolvedConfiguration.resolvedArtifacts.forEach {
+            from(it.file) {
+                rename { "approximations.jar" }
+            }
+        }
+
+        from(usvmApiJar) {
+            rename { "api.jar" }
+        }
+    }
+}
+
+tasks.withType<Jar> {
+    into("/") {
+        from(zipTree(usvmJar))
+    }
 }
 
 publishing {
@@ -23,3 +66,7 @@ publishing {
         }
     }
 }
+
+tasks.withType<Test> {
+    maxHeapSize = "2G"
+}

byteflow-core/src/examples/java/org/byteflow/examples/SqlInjectionSample.java

@@ -0,0 +1,72 @@
+package org.byteflow.examples;
+
+import java.sql.Connection;
+import java.sql.DriverManager;
+import java.sql.ResultSet;
+import java.sql.SQLException;
+import java.sql.Statement;
+
+@SuppressWarnings({"unused", "DuplicatedCode"})
+public class SqlInjectionSample {
+    boolean isProduction;
+
+    public boolean isAdmin(String userId) throws SQLException {
+        String adminUserName;
+        if (isProduction) {
+            adminUserName = getAdminUserNameProd();
+        } else {
+            adminUserName = getAdminUserNameDev();
+        }
+
+        boolean isAdmin;
+        if (isProduction) {
+            isAdmin = checkUserIsAdminProd(userId, adminUserName);
+        } else {
+            isAdmin = checkUserIsAdminDev(userId, adminUserName);
+        }
+
+        return isAdmin;
+    }
+
+    private String getAdminUserNameProd() {
+        return "root";
+    }
+
+    private String getAdminUserNameDev() {
+        return System.getenv("admin_name");
+    }
+
+    private boolean checkUserIsAdminProd(String userId, String adminName) throws SQLException {
+        String adminId;
+        try (Connection dbConnection = DriverManager.getConnection("url://127.0.0.1:8080");
+             Statement statement = dbConnection.createStatement()) {
+            // SECS: potential SQL injection
+            ResultSet rs = statement.executeQuery("SELECT id from users where name='" + adminName + "'");
+            if (rs.next()) {
+                adminId = rs.getString(0);
+            } else {
+                throw new IllegalStateException("No admin id");
+            }
+        }
+
+        if (adminId == null) {
+            throw new IllegalStateException("No admin id");
+        }
+
+        return adminId.equals(userId);
+    }
+
+    private boolean checkUserIsAdminDev(String userId, String adminName) {
+        String adminId;
+        if ("root_1".equals(adminName)) {
+            adminId = "1";
+        } else if ("root_2".equals(adminName)) {
+            adminId = "2";
+        } else {
+            adminId = "0";
+        }
+
+        return adminId.equals(userId);
+    }
+
+}

byteflow-core/src/examples/java/org/byteflow/examples/SqlInjectionSample2.java

@@ -0,0 +1,72 @@
+package org.byteflow.examples;
+
+import java.sql.Connection;
+import java.sql.DriverManager;
+import java.sql.ResultSet;
+import java.sql.SQLException;
+import java.sql.Statement;
+
+@SuppressWarnings({"unused", "DuplicatedCode"})
+public class SqlInjectionSample2 {
+    boolean isProduction;
+
+    public boolean isAdmin(String userId) throws SQLException {
+        String adminUserName;
+        if (isProduction) {
+            adminUserName = getAdminUserNameProd();
+        } else {
+            adminUserName = getAdminUserNameDev();
+        }
+
+        boolean isAdmin;
+        if (isProduction) {
+            isAdmin = checkUserIsAdminProd(userId, adminUserName);
+        } else {
+            isAdmin = checkUserIsAdminProd(userId, adminUserName);
+        }
+
+        return isAdmin;
+    }
+
+    private String getAdminUserNameProd() {
+        return "root";
+    }
+
+    private String getAdminUserNameDev() {
+        return System.getenv("admin_name");
+    }
+
+    private boolean checkUserIsAdminProd(String userId, String adminName) throws SQLException {
+        String adminId;
+        try (Connection dbConnection = DriverManager.getConnection("url://127.0.0.1:8080");
+             Statement statement = dbConnection.createStatement()) {
+            // SECS: potential SQL injection
+            ResultSet rs = statement.executeQuery("SELECT id from users where name='" + adminName + "'");
+            if (rs.next()) {
+                adminId = rs.getString(0);
+            } else {
+                throw new IllegalStateException("No admin id");
+            }
+        }
+
+        if (adminId == null) {
+            throw new IllegalStateException("No admin id");
+        }
+
+        return adminId.equals(userId);
+    }
+
+    private boolean checkUserIsAdminDev(String userId, String adminName) {
+        String adminId;
+        if ("root_1".equals(adminName)) {
+            adminId = "1";
+        } else if ("root_2".equals(adminName)) {
+            adminId = "2";
+        } else {
+            adminId = "0";
+        }
+
+        return adminId.equals(userId);
+    }
+
+}

byteflow-core/src/main/kotlin/org/byteflow/Analysis.kt

@@ -25,6 +25,7 @@ import org.jacodb.analysis.library.newNpeRunnerFactory
 import org.jacodb.analysis.library.newSqlInjectionRunnerFactory
 import org.jacodb.api.JcMethod
 import org.jacodb.api.analysis.JcApplicationGraph
+import java.io.File
 
 private val logger = KotlinLogging.logger {}
 
@@ -37,6 +38,7 @@ fun runAnalysis(
     graph: JcApplicationGraph,
     methods: List<JcMethod>,
     timeoutMillis: Long = Long.MAX_VALUE,
+    useUsvmAnalysis: Boolean = false
 ): List<VulnerabilityInstance> {
     logger.info { "Launching analysis: '$analysis'" }
     val runner = when (analysis) {
@@ -60,5 +62,27 @@ fun runAnalysis(
     logger.info { "Using unit resolver: '$unitResolverName'" }
     val unitResolver = UnitResolver.getByName(unitResolverName)
     val manager = MainIfdsUnitManager(graph, unitResolver, runner, methods, timeoutMillis)
-    return manager.analyze()
+
+    val vulnerabilities = manager.analyze()
+    if (!useUsvmAnalysis) {
+        return vulnerabilities
+    }
+
+    return analyzeVulnerabilitiesWithUsvm(analysis, options, graph, methods, timeoutMillis, vulnerabilities)
 }
+
+fun resolveApproximationsClassPath() = listOf(
+    JarUnpacker.unpackFromResources("approximations/api.jar"),
+    JarUnpacker.unpackFromResources("approximations/approximations.jar")
+)
+
+private object JarUnpacker {
+    fun unpackFromResources(name: String): File {
+        val resource = this::class.java.classLoader.getResourceAsStream(name)
+        val unpacked = File(name).also {
+            it.parentFile.mkdirs()
+        }
+        resource.use { inp -> unpacked.outputStream().use { inp.copyTo(it) } }
+        return unpacked
+    }
+}