SOSA-DSL-FAIR

A Kotlin DSL for defining static program analyses over FAIR (Fixpoint-Aware Abstract Intermediate Representation). The DSL drives a Jimple→FAIR converter powered by SootUp, letting analysis authors specify abstract semantics with concise builder syntax while the framework handles structural IR translation, control-flow graph construction, and call graph resolution.

Project Structure

├── fair.core/          Core FAIR data structures (instructions, CFG, access paths, types)
├── fair.viz/           Ktor web server + four-panel visualization UI
├── src/
│   ├── main/kotlin/
│   │   ├── controller/     Controller, AnalysisContext, FAIRContext (eager/lazy)
│   │   ├── dsl/            DSL: lattice, domain operations, expression handlers, analysis builder
│   │   ├── dsl/examples/   Analysis definitions (taint, typestate, constant propagation)
│   │   ├── converter/      Jimple → FAIR converter pipeline
│   │   ├── interpreter/    Abstract interpreter (fixpoint engine, call handler, stmt executor)
│   │   ├── semantics/      Statement, expression, call, and heap semantics
│   │   ├── helper/         Call graph indexing, fold helpers
│   │   ├── rule/           Method-level rules (JVM defaults, string concat, taint)
│   │   └── sensitivity/    Access path and local variable factories
│   └── test/
│       ├── kotlin/         Unit tests
│       └── java/           Java test programs for conversion
├── build.gradle.kts
└── settings.gradle.kts

Prerequisites

• JDK 17+
• SootUp 2.0.0-SNAPSHOT — must be available in your local Maven repository (~/.m2). Build SootUp from source and run ./mvnw install if not already present.

Build

./gradlew build

This compiles all three modules (fair.core, root, fair.viz), runs tests, and applies Spotless formatting.

Running the CLI Converter

The convert task compiles the test Java programs and converts a named class to FAIR IR:

./gradlew convert --args="SimpleExample"

An optional second argument selects the analysis (default: taint), and a third selects the conversion mode (default: eager):

./gradlew convert --args="ConstantPropExample constprop"
./gradlew convert --args="TypestateExample typestate"
./gradlew convert --args="TaintExample taint"
./gradlew convert --args="SimpleExample taint lazy"

Available analyses: taint, typestate, constprop.

Available modes:

• eager (default) — converts all reachable methods upfront
• lazy — converts methods on demand when first accessed

This will:

1. Load the compiled class via SootUp
2. Build a call graph from the main method entry point
3. Run the selected DSL analysis to produce FAIR output
4. Print FAIR IR for every method in the class
5. Run the abstract interpreter to compute fixpoint results and report findings

Run without arguments to see available test cases:

./gradlew convert

Available test programs

Class	What it exercises
TaintExample	Source/sink/sanitizer taint tracking
TypestateExample	File open/read/close lifecycle (typestate)
ConstantPropExample	Integer constant propagation and arithmetic
SimpleExample	Basic assignment and return
SimpleExampleAccessPath	Field access paths
SimpleExampleBinaryOp	Arithmetic / binary expressions
SimpleExampleCallFunction	Inter-procedural calls
SimpleExampleConditional	If/else branching
SimpleExampleFoldCheck	Fold operations
SimpleExampleForLoop	Loop structures
SimpleExampleFunctionCall	Method invocations
SimpleExampleInvokeCheck	Invoke expression handling
SimpleExampleTaintAnalysisStringConcat	String concat taint propagation
SimpleExampleVirtualInvoke	Virtual dispatch

Running the Visualization Server

./gradlew :fair.viz:run

Opens a web server at http://localhost:8080 with a four-panel UI:

• Source — editable Java source code (or pick a test case from the dropdown)
• Jimple — SootUp's Jimple IR for each method
• FAIR IR — the converted FAIR instructions with source provenance mappings
• CFG — rendered control-flow graph (DOT via Graphviz)

Use the Analysis dropdown to select which analysis to apply (Taint, Typestate, or Constant Propagation), then click Analyze to compile the Java source on the fly, convert it through the selected DSL-driven pipeline, and view all four representations side by side.

Defining an Analysis with the DSL

Analysis definitions use a builder DSL rooted at fairAnalysis(). The DSL provides three layers: taint-specific convenience methods, generic rule()/transition() constructs, and constant-value mapping.

Taint analysis

fun defineTaintAnalysis() = fairAnalysis("TaintAnalysis", TaintLattice) {
    onInvokeExpr {
        source(matching { it.name == "getParam" }, sourceId = "HTTP_PARAM") {
            taintsReturnValue()
        }
        sink(matching { it.name == "sqlQuery" }, sinkId = "SQL") {
            checksArgument(0) { finding ->
                println("!! FINDING: ${finding.kind} — ${finding.detail}")
            }
        }
        sanitizer(matching { it.name == "sanitize" }, sanitizerId = "HTML_SANITIZE") {
            killsTaintOnReturnValue()
        }
    }
}

Typestate analysis

fun defineTypestateAnalysis() = fairAnalysis("FileTypestate", FileStateLattice) {
    onInvokeExpr {
        transition(matching { it.name == "open" }, id = "FILE_OPEN") {
            updatesReceiver(from = Flat.Element(FileState.CLOSED), to = Flat.Element(FileState.OPEN))
        }
        transition(matching { it.name == "read" }, id = "FILE_READ") {
            requiresReceiverState(Flat.Element(FileState.OPEN)) { finding ->
                println("Error: read() on non-open file: ${finding.detail}")
            }
        }
        transition(matching { it.name == "close" }, id = "FILE_CLOSE") {
            updatesReceiver(from = Flat.Element(FileState.OPEN), to = Flat.Element(FileState.CLOSED))
        }
    }
    onNewExpr {
        customTransfer(SetValueOp(Flat.Element(FileState.CLOSED), "FILE_INIT"))
    }
}

Constant propagation

fun defineConstantPropagation() = fairAnalysis("ConstantProp", IntLattice) {
    onConstant {
        mapInt { value -> Flat.Element(value) }
    }
    onBinopExpr {
        customTransfer(TransformOp({ args ->
            when {
                args.all { it is Flat.Element } -> {
                    val (l, r) = args.map { (it as Flat.Element<Int>).value }
                    Flat.Element(l + r)
                }
                args.any { it is Flat.Bottom } -> Flat.Bottom
                else -> Flat.Top
            }
        }, "CONST_ARITH"))
    }
    onInvokeExpr {
        rule(matching { it.name == "abs" }, id = "ABS") {
            transformsReturnValue { args ->
                when (val v = args.firstOrNull()) {
                    is Flat.Element -> Flat.Element(kotlin.math.abs((v as Flat.Element<Int>).value))
                    else -> v ?: Flat.Top
                }
            }
        }
    }
}

Key concepts

Concept	Description
Lattice<T>	Abstract domain with bottom, top, join, meet, leq
DomainOperation<T>	Lattice mutation embedded in FAIR apply statements
ExprHandler<T>	Maps a SootUp expression category to FAIR instructions
ConstantHandler<T>	Maps Jimple constants to abstract values via typed callbacks
FAIRAnalysisDefinition<T>	Immutable analysis config produced by the builder
DslOperator<T>	Bridges DomainOperation to FAIR's FAIROperator interface

Domain operations

Operation	Behavior	Used by
IdentityOp	dest = env[args[0]]	Default for unary expressions
JoinOp	dest = join(args...)	Default for binary expressions
SetTopOp	dest = ⊤	Taint sources, allocation default
SetBottomOp	dest = ⊥	Taint sanitizers
CheckTopOp	Report if any arg is ⊤	Taint sinks
SetValueOp	dest = value	Typestate transitions, constant literals
TransformOp	dest = f(args...)	Constant propagation arithmetic
CheckOp	Report if predicate holds	Typestate state requirements

Two-phase architecture

1. Conversion time — the converter walks Jimple, calls analysisDefinition.processExpression(expr). Matcher predicates fire as callbacks; the first match determines which DomainOperations are embedded in FAIR apply statements.
2. Interpretation time — the FAIR interpreter executes apply statements, calling DomainOperation.execute(dest, args, env) to perform lattice mutations.

Expression handler defaults

Expression type	Default operation	Rationale
Constant (10, "hello")	Structural FAIRReplaceStmt (source is FAIRConstant)	No abstract value unless onConstant is configured
Binary (a + b)	JoinOp	Result carries taint from either operand
Unary (-a, cast, length, instanceof)	IdentityOp	Propagate abstract value unchanged
Allocation (new, newarray)	SetTopOp	Fresh objects start at ⊤
Invoke (unmatched)	IdentityOp	Conservative propagation for unknown calls

Tests

./gradlew test

Code Quality

Spotless (ktlint) and Detekt are configured:

./gradlew spotlessApply   # Auto-format
./gradlew detekt          # Static analysis