IncompleteOperationErrors are imprecise

[johspaeth]

The analysis generates a lot of IncompleteOperationErrors.

Extend the test cases found here to test more thoroughly for these errors.

[mbruns42]

Just to be sure, the current state is

• All tests pass except the HeadlessTests
• oracleExample fails because of crypto.analysis.errors.RequiredPredicateError in method <Crypto.PWHasher: java.lang.Boolean verifyPWHash)
• cogniCryptDemoExample fails because of ImpreciseValueExtractionError in method <example.ImpreciseValueExtractionErrorExample: void main(java.lang.String[])>

Is that correct?

[johspaeth]

That is indeed weird, especially because shippable told that the Build suceeded. On my machine, the tests failed as well and I have just pushed the fixes to the repo. You should be fine, if you pull.

[mbruns42]

Works for me too, now. How does the compilation of OracleExample/src/main/Main.java work? It seems to be configured in Eclipse somehow, but I'm not sure how to start the correct one.

[johspaeth]

The class is just compiled to the bin folder (of the Eclipse project). This test case then executes the analysis on the class files contained in the directory.

[mbruns42]

Please add examples where too many of these errors occur.

[johspaeth]

Have a look at the CogniCrypt reports which contain a couple of IncompleteOperationErrors.

at.favre.lib-hkdf-1.0.0

• CogniCrypt Report.
• Source Code.

com.amazonaws-amazon-kinesis-aggregator-1.0.3

• CogniCrypt Report
• Source Code

If you classify the findings as false positives, it would be great to understand why the analysis reports the issues.

[mbruns42]

Here is the analysis of these errors: IncompleteOperationError.pdf

TL;DR:

• One potential bug when calling doFinal(), will be investigated
• Improvement: Add parameters to error message when expected call and observed call have the same name
• False positives may result from libraries initializing crypto objects, but only performing remaining operations when API functions are called
• Improvement suggestion: Number of displayed errors could be reduced by not reporting same IncompleteOperationError for different objects

[johspaeth]

Great work, thanks. I think we should actually have a wiki page explaining the false positives due to common over-approximation. (Loops, Library Analysis, etc). Do you want to write a wiki about these?

[mbruns42]

I'd be happy to add these ones, but I think others have a better overview and may need to complete the wiki.

[mbruns42]

Potential bug seems to be weird handling of loops. When the beginning of the loop separates one method in the correct sequence from the next, we get two IncompleteOperationExceptions, one in the loop, one outside.

Can be observed in useDoFinalInLoop in #74 in CryptoAnalysisTargets/OracleExample/src/main/Main.java

Can/should we do something about that?

[johspaeth]

I had a look at it, I wondered what we can actually do about it. It is related to this issue.

The same also happens in that simpler case:

foo(){
  Cipher c= Cipher.getInstance("AES");
  c.init(Cipher.ENCRYPT_MODE, key);
  if(staticallyUnknown()){
     c.doFinal("".getBytes());
  }
  return;
}

If the program executes along the false branch, the doFinal call is missing. Hence, the analysis should report one error. It reports two as of the following logic:

1. The analysis detects at the return statement, that variable c does not escape foo(). :+1:
2. At the return statement. the variable's object is not in an accepting. :+1:
3. From the return statement the analysis computes the last statement(s) that use the variable c and report the error(s) at those statements. In the example the backward control-flow reachable statement using c are the doDinal and the init calls. :-1:

[mbruns42]

So we should decide whether to throw IncompleteOperationErrors EITHER on the return statement or on the destructing statement? Would choosing just one lead to false negatives?

[johspaeth]

No, we would like to report on the last statement using the variable. It is strange to get a report at the return statement as it does not even use variabel c and their might be many lines between the last usage of the variable and the return.

[mbruns42]

Ok, that makes sense. So how should we proceed?