How to perform strict constant detection

[fan-14]

I want to do strict constant queries，

A parameter is a constant only if all of its streams come from a constant source,

A parameter is a variable if there exist a data flow comes from a variable.

But I don't know how to represent a variable with no incoming data.

So I don't know how to distinguish the data stream from the variable....

God，I would really appreciate it if someone could help me...

Excuse my poor English

java code：

import javax.crypto.spec.PBEParameterSpec;
import java.security.SecureRandom;
import java.util.*;

public class StaticSaltsCorrected {
    public static void main(String [] args){
        StaticSaltsCorrected cs = new StaticSaltsCorrected();
        cs.key2();
    }
    public void key2(){
        SecureRandom random = new SecureRandom();

        long c;

        Date this_date = new Date(2016, 8, 20);
        c=this_date.getTime();

        PBEParameterSpec pbeParamSpec = null;
        byte[] salt = new byte[32];
        //random.nextBytes(salt);

        salt[0]=(byte)c;//Here c is a variable, salt is a constant, and salt is a variable when assigned this way
        int count = 1020;

        pbeParamSpec = new PBEParameterSpec(salt, count);
        //Variables as arguments are harmless and should not be queried
    }
}

codeql code：

import java

import semmle.code.java.dataflow.DataFlow

import semmle.code.java.dataflow.TaintTracking

import semmle.code.java.security.Random

import DataFlow::PathGraph

import semmle.code.java.ControlFlowGraph



/** Define a PBEParameterSpec constructor class */

class PBEParameterSpec extends Constructor{

 PBEParameterSpec(){

  this.getDeclaringType().hasQualifiedName("javax.crypto.spec", "PBEParameterSpec")

 }

}





class ConstantFlowConfiguration extends DataFlow::Configuration {

 ConstantFlowConfiguration() { this = "ConstantFlow" }



 override predicate isSource(DataFlow::Node source) {

  source.asExpr() instanceof PredictableSeedExpr

  // any()

 }



 override predicate isSink(DataFlow::Node sink) { 

  any()

 }



 override predicate isAdditionalFlowStep(DataFlow::Node node1, DataFlow::Node node2) {//When a subexpression marks, the parent expression marks

  ( node1.asExpr().getParent()=node2.asExpr() )

 }


}





from PBEParameterSpec a,Call sink,Expr source,ConstantFlowConfiguration conf

where 

//sink is a node of the function call called PBEParameterSpec
sink.getCallee() = a
and
conf.hasFlow(DataFlow::exprNode(source),DataFlow::exprNode(sink.getArgument(0)))
and
//Remove redundant expressions
not exists( Expr temp| temp.getParent()=source )

select source,sink

[smowton]

The flow step node1.asExpr().getParent()=node2.asExpr() is likely too vague to do anything useful: for example, if a PredictableSeedExpr flowed to x in f(x, y) then because f(x, y) is a parent we would note flow to the result of f, even if the function doesn't actually return x or anything related to it. It would even create flow from x in x == 100 ? y : z to the whole conditional expression, even though x definitely did not flow there.

It sounds like you want to know what expressions are always constant? In that case the data-flow library is probably not what you want: it determines when data may flow to a particular expression, whereas you want to determine when some property (constant-ness) must hold of an expression, i.e. it holds of all predecessors.

You could do this by defining a recursive relation: something like

DataFlow::Node getADefiniteConstant() {
  result.asExpr() instanceof CompileTimeConstantExpr // Base case
  or
  forall(DataFlow::Node pred | DataFlow::localFlowStep(pred, result) | pred = getADefiniteConstant()) // Intra-procedural flow from a constant
  or
  ...
}

If you want to propagate must-be-constant expressions across procedure calls you need to pair up argument and parameter nodes: you can see an example of this being done at the Expr (rather than DataFlow::Node) level in the controlledString and controlledStringProp predicates defined in ControlledString.qll: these look for specifically the case of a string constant that must be wholly controlled by the programmer, so may be adaptable to your needs.

[fan-14]

Thank you for you help!Though recursive relation didn't work.