Is CodeQL capable of inferring possible parameter values of a function via symbolic modeling?

[wooyune1]

Inspired by https://github.com/github/codeql/blob/main/csharp/ql/src/Security%20Features/CWE-798/HardcodedConnectionString.ql, I wrote code to get the possible string literals that may flow into the "WriteLine" function, as shown below.

import csharp
import semmle.code.csharp.frameworks.system.Data
import semmle.code.csharp.security.dataflow.HardcodedCredentialsQuery

module StringLiteralFlowConfig implements DataFlow::ConfigSig {
  predicate isSource(DataFlow::Node source) { source instanceof NonEmptyStringLiteral}

  predicate isSink(DataFlow::Node sink) {
    exists(MethodCall mc|
      mc.getTarget().hasName("WriteLine")
      and sink.asExpr() = mc.getAnArgument()
    )
    and not sink.asExpr() instanceof StringLiteral
  }

  predicate isBarrier(DataFlow::Node node) {
     node instanceof StringFormatSanitizer 
  }
}
module MyFlow = TaintTracking::Global<StringLiteralFlowConfig>;

from DataFlow::Node source, DataFlow::Node sink, string s
where
  MyFlow::flow(source, sink)
  and source.asExpr().(StringLiteral).getValue() = s
select s, sink

However, the string literals passed to 'WriteLine' do not determine the actual possible values of its argument. Example is below.

string a = "a";
string b = "b";
Console.WriteLine(a + b);

Can CodeQL infer a function's possible parameter values via modeling some key functions (e.g., string concatenation)? Since I'm a beginner, I'm not sure if CodeQL can solve this problem. I'd really appreciate any help!

[adityasharad]

Thanks for your interest using CodeQL.

Can CodeQL infer a function's possible parameter values via modeling some key functions (e.g., string concatenation)?

In general, this is not possible for a static analysis tool like CodeQL to compute precisely, since doing so would be equivalent to running the program (and so would hit theoretical limits). However, there are some ways to approximate this idea, where you can find some possible constant values if we know them from the program at compile time.

• The Expr type has predicates hasValue() (which holds if the given expression has a compile-time constant value), and getValue() (which gets you that value if it exists). See https://codeql.github.com/docs/codeql-language-guides/codeql-library-for-csharp/#id24. This will handle constants and a few operations on those constants, but may not handle all possible operations.
• You could use those as part of your query to identify the value of your sources -- https://codeql.github.com/docs/codeql-language-guides/analyzing-data-flow-in-csharp/#exercise-1 is very similar to the example you describe. What I would do is to write your logic so that if there is a source value, you report it, and if there is no known source value, you still report the data flow but don't attempt to compute the source value.
• For some supported languages in CodeQL, there are CompileTimeConstantExpr classes in the standard library, or library modules named Constants or ConstantExprs. Those contain operations to help you reason about such constant-valued expressions, with a very limited set of symbolic evaluation.
• For C# I don't think we expose this kind of symbolic evaluation in the libraries. A common pattern in our standard libraries is to expose helper predicates that compare between two expressions to see if they have the same value, but don't make any attempt to symbolically compute the value itself. Constants and StructuralComparison are examples I found for C#.

[michaelnebel]

That covers it really well @adityasharad !
It is worth noting that the getValue() predicate on Expr do get the compile time constant / folded expression value (if computed by Roslyn), but this is limited and will not cover the case presented in the example.

As a rule of thumb

• Roslyn (which is used by our extractor) folds expressions that are purely composed by compile time constants.
• Roslyn folds expressions where all operands are constants

That is, for the examples below the right hand side expressions are folded and will have a pre-computed constant value, which can be retrieved by Expr.getValue() except for string s4 = s1 + s2; (which is the most interesting case) as the operands are not constant.

const string c1 = "Hello";
const string c2 = "World";
const string c3 = "Hello" + "World";
const string c4 = c1 + c2;

string s1 = "Hello";
string s2 = "World";
string s3 = "Hello" + "World";
string s4 = s1 + s2;

[hvitved]

As @adityasharad writes, we do not currently attempt to do any constant propagation in QL for C#, like we for example do for Ruby. In Ruby we would e.g. be able to infer that z has the value "ab" in

x = "a"
y = "b"
z = a + b

[wooyune1]

Thank you very much to @adityasharad for the response, and to @michaelnebel and @hvitved for the additional insights.
Is it possible to compute the set of possible values for a given variable? Here's an example:

string a = "a"; // line 1  
string b;  
if (1 == 1) {  
    b = "b"; // line 4  
} else if (1 != 1) {  
    b = "unreachable"; // line 6  
} else {  
    b = getNAC(); // line 8  
}  
string value = a + b; // line 10  
Console.WriteLine(value); // line 11  

My current approach is to use dfs and use-def chains. Assuming we have already modeled string concatenation, here is the manual analysis process:

1. The definition of value on line 11 comes from line 10.
2. The value on line 10 depends on the function call on the right-hand side. Since we have modeled string concatenation, we need to further analyze the strings being concatenated.
3. The value of variable a is defined at line 1, and it clearly has only one possible value: "a".
4. Variable b is defined in three places (lines 4, 6, and 8), so its possible values are "b" and "unreachable". Since we haven't modeled the getNAC function, we will ignore that value.
5. Finally, we take the Cartesian product of the possible values of a and b, so value could possibly be "ab" or "aunreachable".

[hvitved]

It should in principle be doable, but I doubt it will be very useful in practice when expressions like getNAC() have unknown values.