Static field accesses is not properly modeled

[johspaeth]

The data-flow of a static field is not correctly detected.

The test case below succeeds

@Test
public void generateNewAES128GCMKeySet() throws GeneralSecurityException {
	KeyTemplate kt = AeadKeyTemplates.createAesGcmKeyTemplate(16);
	Assertions.hasEnsuredPredicate(kt);
}

whereas when we replace it to the equivalent usage of (AES128_GCM is instantiated via a call to createAesGcmKeyTemplate)

@Test
public void generateNewAES128GCMKeySet_static() throws GeneralSecurityException {
	KeyTemplate kt = AeadKeyTemplates.AES128_GCM;
	Assertions.hasEnsuredPredicate(kt);
}

The predicate does not reach the assertion

[kruegers]

Make sure to check out the examples given in #163 and eclipse-cognicrypt/CogniCrypt#292 when working on this issue.

[rakshitkr]

Current solution: Determine the actual method used for initialising the static field. If the method is an initial transition, then the seed is generated for the original statement that has the static field.

Roadblock: The above solution requires the body of the initialiser method (clinit) of the class whose static field is used in the test code. For this, one must avoid the addition of rule classes to excluded packages. With this, the analysis fails for the tests with two or more seeds (e.g. below). The reason is StatementValWeightTable in the boomerang results has values other than the ones from TestMAC.generateNewHMACSHA256_128BitTag method resulting in satisfied field in InAcceptingStateAssertion class not being set to true. However, this doesn't happen when one adds the rule classes to the excluded packages.

@Test
	public void generateNewHMACSHA256_128BitTag() throws GeneralSecurityException {
		KeyTemplate kt = MacKeyTemplates.createHmacKeyTemplate(32, 16, HashType.SHA256);
		KeysetHandle ksh = KeysetHandle.generateNew(kt);
		Assertions.mustBeInAcceptingState(kt);
		Assertions.mustBeInAcceptingState(ksh);
	}

Alternate solution : Retrieve the body of the initialiser method (clinit) of the class whose static field is used in the test code while excluding the rule classes.