Error testing a predicate of Google Tink specification

[rbonifacio]

The following test case is failing, because a predicate to the key template object (kt) is not being generated.

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

The goal here is to verify if the specification for the class AeadKeyTemplates is correct. The Google Tink specifications are available at the Crypto-API-Rules repository

The test code is available at the branch issue-89. To run this test cases, it is necessary to configure Soot to find the Google Tink libraries. To this end, we have to add these lines

String userHome = System.getProperty("user.home");
//... 
sootCp += File.pathSeparator + userHome + "/.m2/repository/com/google/crypto/tink/tink/1.2.0/tink-1.2.0.jar";

to the method initializeSootWithEntryPoint (class AbstractTestingFramework of the WPDS project).

[johspaeth]

@rbonifacio Could you grant me access to the binary files of the rules? That would simplify the testing on my side.

[rbonifacio]

@johspaeth the binary files are available in a particular branch issue-89

[johspaeth]

I debugged the test case, fixed some issues for the specification and observed the following in this commit

• The rule AeadKeyTemplates has a constraint which can never become true. The values k16 and k32 both reference the same value of x at a call to createAesGcmKeyTemplate(x). Therefore k16 == k32. The rules also states k16 == 16 and k32 == 32 which is a contradiction. I suggest to change the rule to state k16 in {16,32}. If you changed the rule, please remove lines 349 and 350 of the commit (I did not want to change the rules and hard-coded to ignore the contradiction of the rule.)

• Then, I refactored one of your tests in the class TestAEADCipher. The test case still fails, but only at the last Assertions.hasEnsuredPredicate. There are two causes for the failure.
  (1) The statement Aead aead = AeadFactory.getPrimitive(ksh); returns a type Aead but there is no rule for Aead (only for AeadPrimitive, should be renamed to Aead). For debug purpose I also changed line 295 and 296 of the commit and added a TODO for you, please remove the code once the rule is updated.
  (2) The rule REQUIRES setAeadPrimitive[aead]; which can never be fulfilled because aead is never bound within the rules. Removing the REQUIRES clause of this rule should make test case encryptUsingAES128GCM_refactored() pass.

[rbonifacio]

Hi @johspaeth, I fixed the Google Tink specifications. Thanks for reporting the errors. The test cases for the AEAD are passing now, and I reverted your previous changes on classes AnalysisSeedWithSpecification and ConstraintSolver. I sent these contributions using the branch #92.

There are two points that I would like to discuss (perhaps in your next meeting, if you prefer).

(a) I think that it should be possible to specify a CrySL rule in a file with a different name of the class (or interface), or perhaps we should have to design a different approach to avoid name conflicts. For instance, both JCA and Google Tink have an interface named Mac, and it is not possible to have two specifications with the same name. For this reason, I decided to name the CrySL files for the Tink primitives with the suffix "Primitive", like AeadPrimitive and MacPrimitive (though the names of the interfaces are Aead and Mac). Nevertheless, based on your last message, it seems to me that this is not possible (or at least not recommended). For some reason, it is working for the MacPrimitive.

(b) As I said, the current test cases on branch #92 are leading to a "green bar". However, I could not understand one situation.

This next test case runs and leads to green bar.

@Test
public void generateNewAES128GCMKeySet() throws GeneralSecurityException {
   KeyTemplate kt = AeadKeyTemplates.AES128_GCM;
   KeysetHandle ksh = KeysetHandle.generateNew(kt);
   Assertions.hasEnsuredPredicate(kt);
   Assertions.mustBeInAcceptingState(kt);
   Assertions.mustBeInAcceptingState(ksh);		
}

This next test case also runs and leads to a green bar.

@Test
public void encryptUsingAES128GCM() throws GeneralSecurityException {
   KeyTemplate kt = AeadKeyTemplates.AES128_GCM;
   KeysetHandle ksh = KeysetHandle.generateNew(kt);
		
   final String plainText = "Just testing the encryption mode of AEAD"; 
   final String aad = "cryptsl";

   Aead aead = AeadFactory.getPrimitive(ksh);
   byte[] out = aead.encrypt(plainText.getBytes(), aad.getBytes());
		
   Assertions.mustBeInAcceptingState(aead);
   Assertions.hasEnsuredPredicate(out);
}

However, if I add this assertion Assertions.hasEnsuredPredicate(kt); after the ksh assigment to this last test cases, it fails. Is there any particular reason for that?

[johspaeth]

Regarding (a): I agree, it is confusing especially as we do warn the CrySL developer about this issue. There are only one or two lines in the code that use the actual filename of the rule, we should instead use the string listed in the SPEC clause at these points.

(b) That seems like a bug. I investigate it further.

[johspaeth]

I had a quick look. In my environment, the test cases in TestAEADCipher still fail. (I assumed you commited the binary rules into the repository, correct?)

Also, as of now, the analysis does not properly model the static field flows.
It eases debugging and specification, when you explicitly create the object your self by replacing this line
(1) KeyTemplate kt = AeadKeyTemplates.AES128_GCM;
by
(2) KeyTemplate kt = AeadKeyTemplates.createAesGcmKeyTemplate(16);

The simple difference is that by unsing the first line, the JVM implicitly calls the class initializer () of AedKeyTemplates and within the class initializer, it creates the object
AeadKeyTemplates.AES128_GCM = AeadKeyTemplates.createAesGcmKeyTemplate(16);

The test cases do not properly model the calls as they are not explicit within the code. I work on that and give you an update here. Until then line (2) in your test cases.

[rbonifacio]

I've just updated and built the WPDS project. Now I am getting the same results as yours (some test cases are failing). At least this might explain the different results that we were getting.

[johspaeth]

Good...or well bad. :)

Then I know where to look at.

[johspaeth]

While debuggnig, I still saw that the constraints lists
[key16 == 16 , key32 == 32] which yields to the problem discussed above.

Did you update the rules (and cryptslbin files) accordingly? In the repository, I cannot see any update on the master:
https://github.com/CROSSINGTUD/Crypto-API-Rules/blob/master/src/de/darmstadt/tu/crossing/tink/AeadKeyTemplates.cryptsl

We really need to be able to read in rules in CrySL-source code format...@kruegers is working on that! 👍

[rbonifacio]

Hi @johspaeth , I've just commited some changes to the test cases and binary versions of the specifications. The test cases are running again, and I hope that our environment is the same now. The source code of the specifications is available at:

https://github.com/rbonifacio/Crypto-API-Rules/tree/tink

[johspaeth]

Great, it works on my machine as well.

I will have a look at the data-flows of static fields, such that you can properly model the usages.