Taint propagation is blocked due to a reversed subtype check

[yyzzcchh]

📝 Overall Description

In Tai-e’s taint analysis, taint propagation across type cast is blocked due to a reversed subtype check in TypeFilter.

Tai-e/src/main/java/pascal/taie/analysis/pta/core/solver/TypeFilter.java

Lines 63 to 67 in 361345c

	private boolean isAssignable(Type from, Type to) {
	return (from instanceof NullType)
	? to instanceof ReferenceType
	: typeSystem.isSubtype(to, from);
	}

A type cast such as:

public static void main(String[] args) {
    testTypeCast("test");
}

private static void testTypeCast(Object obj) {
    System.out.println((String) obj);
}

isSubtype(str, obj) fails the type filter, and taint propagation is incorrectly stopped.

The propagation works correctly after changing the code to isSubtype(from, to).

🎯 Expected Behavior

Points-to sets of all variables
[]:<TypeCast: void main(java.lang.String[])>/%stringconst0 -> [[]:ConstantObj{java.lang.String: "test"}]
[]:<TypeCast: void main(java.lang.String[])>/args -> [[]:EntryPointObj{alloc=MethodParam{<TypeCast: void main(java.lang.String[])>/0},type=java.lang.String[] in <TypeCast: void main(java.lang.String[])>}]
[]:<TypeCast: void testTypeCast(java.lang.Object)>/obj -> [[]:ConstantObj{java.lang.String: "test"}, []:TaintObj{alloc=<TypeCast: void testTypeCast(java.lang.Object)>/0,type=java.lang.Object}]
[]:<TypeCast: void testTypeCast(java.lang.Object)>/temp$0 -> []
[]:<TypeCast: void testTypeCast(java.lang.Object)>/temp$1 -> [[]:ConstantObj{java.lang.String: "test"}, []:TaintObj{alloc=<TypeCast: void testTypeCast(java.lang.Object)>/0,type=java.lang.Object}]

Points-to sets of all static fields
<java.lang.System: java.io.PrintStream out> -> []

Points-to sets of all instance fields

Points-to sets of all array indexes
[]:EntryPointObj{alloc=MethodParam{<TypeCast: void main(java.lang.String[])>/0},type=java.lang.String[] in <TypeCast: void main(java.lang.String[])>}[] -> [[]:EntryPointObj{alloc=MethodParam{<TypeCast: void main(java.lang.String[])>/0}[],type=java.lang.String in <TypeCast: void main(java.lang.String[])>}]

Detected 1 taint flow(s):
TaintFlow{<TypeCast: void testTypeCast(java.lang.Object)>/0 -> <TypeCast: void testTypeCast(java.lang.Object)>[2@L7] invokevirtual temp$0.println(temp$1)/0}

🐛 Current Behavior

Points-to sets of all variables
[]:<TypeCast: void main(java.lang.String[])>/%stringconst0 -> [[]:ConstantObj{java.lang.String: "test"}]
[]:<TypeCast: void main(java.lang.String[])>/args -> [[]:EntryPointObj{alloc=MethodParam{<TypeCast: void main(java.lang.String[])>/0},type=java.lang.String[] in <TypeCast: void main(java.lang.String[])>}]
[]:<TypeCast: void testTypeCast(java.lang.Object)>/obj -> [[]:ConstantObj{java.lang.String: "test"}, []:TaintObj{alloc=<TypeCast: void testTypeCast(java.lang.Object)>/0,type=java.lang.Object}]
[]:<TypeCast: void testTypeCast(java.lang.Object)>/temp$0 -> []
[]:<TypeCast: void testTypeCast(java.lang.Object)>/temp$1 -> [[]:ConstantObj{java.lang.String: "test"}]

Points-to sets of all static fields
<java.lang.System: java.io.PrintStream out> -> []

Points-to sets of all instance fields

Points-to sets of all array indexes
[]:EntryPointObj{alloc=MethodParam{<TypeCast: void main(java.lang.String[])>/0},type=java.lang.String[] in <TypeCast: void main(java.lang.String[])>}[] -> [[]:EntryPointObj{alloc=MethodParam{<TypeCast: void main(java.lang.String[])>/0}[],type=java.lang.String in <TypeCast: void main(java.lang.String[])>}]

Detected 0 taint flow(s):

🔄 Reproducible Example

class TypeCast {
    public static void main(String[] args) {
        testTypeCast("test");
    }

    private static void testTypeCast(Object obj) {
        System.out.println((String) obj);
    }
}

taint-config:

sources:
  - { kind: param, method: "<TypeCast: void testTypeCast(java.lang.Object)>", index: 0 }

sinks:
  - { method: "<java.io.PrintStream: void println(java.lang.String>", index: 0 }

call-site-mode: true

run args:
-cp classes -m TypeCast -ap -pp -a pta=taint-config:taint-config.yml;implicit-entries:false;only-app:true;

⚙️ Tai-e Arguments

🔍 Click here to see Tai-e Options

{{The content of 'output/options.yml' file}}

🔍 Click here to see Tai-e Analysis Plan

{{The content of 'output/tai-e-plan.yml' file}}

📜 Tai-e Log

🔍 Click here to see Tai-e Log

{{The content of 'output/tai-e.log' file}}

ℹ️ Additional Information

No response

[jjppp]

isSubtype(str, obj) fails the type filter, and taint propagation is incorrectly stopped.

The propagation works correctly after changing the code to isSubtype(from, to).

No. TypeSystem.isSubtype(superType, subType) checks if subType (the second argument) is a subtype of superType (the first argument). In your case, a type filter checks if the type of the object (some TaintObject of type java.lang.Object) is a subtype of the cast operation (java.lang.String in your example). Apparently, the cast will fail by throwing a ClassCastException.

For resolving your issue, I strongly recommend you to have a look at our documentation for taint configurations.
{ kind: param, method: "<TypeCast: void testTypeCast(java.lang.Object)>", index: 0 } without a type information for the taint object in your taint config creates taint objects with the type specified by the parameter (which is exactly java.lang.Object).
I believe setting the type of the taint sources to be java.lang.String will fix your issue.

[yyzzcchh]

Thanks for the reply.
Sorry, I misunderstood the purpose of the isAssignment() method. In this case, setting the type of the taint sources does work. However, in practical cases, we usually cannot know the concrete types involved in taint propagation. Is there a way to define a type in a single transfer (e.g., java.lang.Object^) that includes all of its subtypes, or to propagate all taints while ignoring the type?

[jjppp]

The idea of using java.lang.Object^ in taint config seems reasonable and might worth implementing, but is currently not supported.

It is possible though to write your own TaintConfigProvider to programmatically create taint sources or transfers (using type hierarchy information provided by tai-e). A quick example can be found here.