CryptoAnalysis does not check CONSTRAINTS if no ORDER is specified.

[shahrzadav]

CryptoAnalysis does not throw an error when a constraint is violated when the ORDER section is empty and the EVENTS and OBJECTS are not used in the ORDER section. For example, this code shows the CrySL rule for KeyAgreement class from BouncyCastle-JCA API.

SPEC javax.crypto.KeyAgreement
OBJECTS
	java.lang.String algorithm;
	java.security.Provider provider;
	java.lang.String providerS;
	java.security.Key key;
	java.security.SecureRandom random;
	java.security.spec.AlgorithmParameterSpec params;
	boolean lastPhase;
	byte[] sharedSecret;

EVENTS
	ins1 : getInstance(algorithm);
	ins2 : getInstance(algorithm, provider);
	ins3 : getInstance(algorithm, providerS);
	Instances := ins1| ins2| ins3;
	
	i1 : init(key);
	i2 : init(key, random);
	i3 : init(key, params);
	i4 : init(key, params, random);
	Inits := i1| i2| i3| i4;

	d : doPhase(key, lastPhase);
	Do := d;
	
	g1 : generateSecret();
	g2 : generateSecret(sharedSecret, _);
	g3 : generateSecret(algorithm);
	GenerateSecrets := g1| g2| g3;


ORDER
       Instances, Inits

CONSTRAINTS
	providerS in {"BC"};
	instanceOf[provider, org.bouncycastle.jce.provider.BouncyCastleProvider];

REQUIRES
	BCProvider[provider];

//ENSURES//*

If we use this rule like this to test the below code we see the error that the providerS object should be of "BC". But, if we remove the order, we will get no error in that line (second pic).

I used the latest version of CogniCrypt from develop branch. The test code is generated by CogniCrypt-TestGen

[AnakinRaW]

I suppose this also happens when using the CLI of CryptoAnalysis? Is there any way to find out if the CrySL or CryptoAnalysis is causing the issue?

[shahrzadav]

@AnakinSklavenwalker My guess is that it is the CryptoAnalysis, but it should be debugged to see how it proves the CONSTRAINTS.

[marvinvo]

Well, I don't found a fix yet, but I have an idea where it should be debugged:

As far as I know, CryptoAnalysis will generate a seed for each object. That is happening in CryptoScanner's scan() method... in detail, scan() does a call to initialize()which creates the start seeds and does a call to getOrCreateSeedWithSpec() which will add these seeds to the attribute worklist. https://github.com/CROSSINGTUD/CryptoAnalysis/blob/35d09163f97b6919a4359fcaa0e846af95c1fed1/CryptoAnalysis/src/main/java/crypto/analysis/CryptoScanner.java#L77

With worklist initialized, execute() is called on each seed. Here is where validation of crysl rules takes place. This is happening in steps:

• runTypestateAnalysis() Here is where soot magic happens I guess. This should put ForwardBoomerangResults<TransitionFunction> into results.

  debug: result should not be null, otherwise no other checks would be done.

• allCallsOnObject = results.getInvokedMethodOnInstance(); As the name says, this should return all methods as HashMap<Statement, SootMethod>.

  debug: allCallsOnObject should hold all method calls of seeds regarding java object, especially it should hold the method with the constraint violation, otherwise I think no constraint checks would be done for it, because...

• runExtractParameterAnalysis(); ...as far as I see, will filter or sort allCallsOnObject and store results in this.parameterAnalysis, which will be used in constraint validation:

• checkInternalConstraints();

see https://github.com/CROSSINGTUD/CryptoAnalysis/blob/35d09163f97b6919a4359fcaa0e846af95c1fed1/CryptoAnalysis/src/main/java/crypto/analysis/AnalysisSeedWithSpecification.java#L115

[marvinvo]

But with the whitelisting approach in mind, that should actually throw an typestate violation instead of constraint violation. In instance, if a method does not appear in the order section, it is not used to be used. Hence there may be no constraint validation on methods, that doesn't appear in the order section. But then there should be an typestate error thrown in computeTypestateErrorUnits(); or computeTypestateErrorsForEndOfObjectLifeTime();.

[lukasngl]

Not documented, but you can use * in place of an actual order. This generates a StateMachine with a loop transition on every specified event. Then constraintes should be checked.

[smeyer198]

In CrySL the ORDER section is mandatory. Therefore, if the ORDER section is missing (or the expression is not valid), CryptoAnalysis will not parse the rules correctly and the constraints will not be checked. If the ORDER section is not needed, i.e. the EVENTS can be called in an arbitrary order, the expression ()* can be used (as mentioned by Lukas). This could look like this:

...
ORDER
    ()*
...