JBMC and verification of URL encoding

[Etienne13]

Hi there,

Context: I am trying to use JBMC to verify the presence of vulnerabilities in source code of test cases of the Juliet 1.3 testsuite. I started with CWE113 and could run JBMC on a test case but realized JBMC was not dealing with the URL encoding bytcode as I was expecting.

Test case: here is a simplified example to test.

package jbmc_issues.urlencoder;

import java.net.URLEncoder;

public class EncodeTest
{
    public static void main(String[] args) throws Throwable
    {
	String data = "Hello world";
	String d = URLEncoder.encode(data, "UTF-8");
	if(d!=null && !d.isEmpty()) {
	    // d = d.replace("\r", " ");
	    assert(!d.contains("\r"));
	}
    }
}

Run command for jbmc : $JBMC_PATH/jbmc jbmc_issues/urlencoder/EncodeTest --max-nondet-string-length 10 --unwind 50 --classpath $JBMC_PATH../../../jbmc/lib/java-models-library/target/core-models.jar:. --main-class EncodeTest --trace

Expected behavior: verification succeeds, no counter-example

Observerd behavior: the verification of the assert fails, the trace seems to indicate that the encode function can throw a NPE but I am not sure I understand the trace properly and if my understanding is correct, why an NPE could be thrown.

Additional comment: if you uncomment the line d = d.replace("\r", " ");, the verification succeeds.

Thanks for your help on this!

[peterschrammel]

I think that you are missing the cprover-api.jar on the classpath, which connects the core models to JBMC itself.
It should be something like:

/path/to/jbmc/jbmc jbmc_issues.urlencoder.EncodeTest --max-nondet-string-length 10 --unwind 50 --classpath /path/to/project/classes/root:/path/to/jbmc/cprover-api.jar:/path/to/jbmc/core-models.jar

(I'm currently running version 6.3.1 with unwind 30 to validate, but it hasn't finished overnight yet...)

[Etienne13]

Thanks for the answer.

After adding cprover-api.jar in the command line, I re-run the verification of the code snippet I sent, but I get exactly the same result as before.

My configuration is : JBMC version 6.5.0 (cbmc-6.5.0-38-g5dc709dec3) 64-bit x86_64 linux

MiniSAT 2.2.1 seems to be the underlying solver in my config.

Not sure if this is a matter of jbmc version (6.3.1 vs 6.5.0)? If the verification succeeded with 6.3.1 (did it succeed?) then that would look like a regression.