pamunb / metacrysl Goto Github PK

MetaCrySL should also support the FORBIDDEN clause.

 FORBIDDEN
   method1(int); 
   method2(int, String) => methods() ;  
   // A(B) => C — a forbidden method named A with parameter of Type B and replacement C (from the original CrySL paper) 

Current grammar does not yet support a CONSTRAINTS clause. As per CrySL specification, this clause
specifies the constraints for the objects defined under OBJECTS and used as parameters or return values in the EVENTS section.

Example of CONSTRAINTS section:

CONSTRAINTS
algorithm in { " AES " , " Blowfish " };
algorithm in { " AES " } = > keySize in {128 , 192 , 256};
algorithm in { " Blowfish " } = > keySize in {128 , 192 , 256 , 320 , 384 ,
448};

The ENSURES section specifies what a clause guarantees, presuming that the object is used properly. This is a mandatory construct in a CrySL rule and specifies predicates to govern interactions between different classes.

Example:

ENSURES
generatedKey [ key , algorithm ];

This predicate may be required by another class.

As per #3 , a CrySL rule mandates a ENSURES section that specifies a predicate to govern interactions between classes. The REQUIRES section is a non-mandatory clause.

Example:

REQUIRES
generatedKey [ key , alg ( transformation ) ];

On branch add-tests, the generated spec for Android-cc, 0108 version Cipher.spec is not as expected.

-> Section CONSTRAINTS presented unfinished constraints like this:
part(0,transformation) in {"AES"} => part(1,transformation) in ${aes_modes};
and this
part(0,transformation) in {"RSA"} => part(2,transformation) in ${rsa_paddings};

where the expected results should look like
part(0,"/",transformation) in {"AES"} => part(1,"/",transformation) in {"OFB", "CBC", "CTS", "CTR", "CFB"};
and
part(0,"/",transformation) in {"RSA"} => part(2,"/",transformation) in {"NoPadding", "PKCS1Padding", ""};.

-> Section REQUIRES presented require expressions with null's
generatedKey[key,null]; and preparedAlg[param,null];

where the expected results should be
generatedKey[key, part(0,"/",transformation)]; and preparedAlg[param, part(0,"/",transformation)];

Here is the plain spec for the cited sections:

// Cipher.spec for Android-cc version 0108

CONSTRAINTS

	part(1,transformation) in {"CBC","PCBC","CTR","CTS","CFB","OFB"} && encmode!=1 => noCallTo[IWOIV];
	part(1,transformation) in {"CBC","PCBC","CTR","CTS","CFB","OFB"} && encmode==1 => callTo[iv];
	encmode in {1,2,3,4};
	length[pre_plaintext]>=pre_plain_off+len;
	length[pre_ciphertext]<=pre_ciphertext_off;
	length[plainText]<=plain_off+len;
	length[cipherText]<=ciphertext_off;
	part(0,transformation) in {"AES"} => part(1,transformation) in ${aes_modes};
	part(0,transformation) in {"AES"} && part(1,transformation) in {"CBC"} => part(2,transformation) in {"PKCS7Padding","PKCS5Padding","ISO10126Padding"};
	part(0,transformation) in {"AES"} && part(1,transformation) in {"CTR","CFB","OFB"} => part(2,transformation) in {"NoPadding"};
	part(0,transformation) in {"RSA"} => part(1,transformation) in {"","ECB"};
	part(0,transformation) in {"RSA"} => part(2,transformation) in ${rsa_paddings};
	part(0,transformation) in {"AES","RSA"};

REQUIRES

	generatedKey[key,null];
	randomized[ranGen];
	preparedAlg[param,null];
	!macced[_,plainText];
	part(1,transformation) in {"CBC","PCBC","CTR","CTS","CFB","OFB"} && encmode==1 => preparedIV[params];
	part(1,transformation) in {"GCM"} => preparedGCM[params];

Using add-tests branch, I ran MetaCrySLGeneratorTests and an output SPEC was not as expected. AlgorithmParameters Spec REQUIRES section should look like this after applying the refinements:

REQUIRES
  
    preparedAlg[parAr];
  
    alg in {"AES", "DESede"} => preparedIV[params];
  
    alg in {"DiffieHellman"} => preparedDH[params];
  
    alg in {"DH"} => preparedDH[params];

but instead, this was the result:

REQUIRES

	preparedAlg[parAr];

We've introduced some changes to the grammar on the code-gen branch. Those changes were needed to simplify the implementation of the code-writer, but it seems like some of those changes broke the parser for some constraint expressions.

These expressions, for instance, throws a parser error:

part(1, "/", transformation) in {"CBC", "PCBC", "CTR", "CTS", "CFB", "OFB"} && encmode != 1 => noCallTo[IWOIV] ;
length[pre_plaintext] >= pre_plain_off + len;

The differences between the old and new grammar for constraints are:

// old (used to work for expressions above)
ConstraintExp : BooleanExp; 
BooleanExp : exp = ImpliesExp;

// new (broken)
ConstraintExp : ImpliesExp;

Steps to reproduce

Pull the merge-strategy branch and run the MetaCrySLGeneratorTest. I've added a test called parseRefinement that is falling due to JvmParametrizedTypeRefence being null.

This test is parsing the following refinement:

SPEC Cipher REFINES javax.crypto.Cipher {
    define aes_modes = {"GCM"};  
	add constraint part(0, "/", transformation) in {"AES"} && part(1, "/", transformation) in {"GCM"} => part(2, "/", transformation) in {"NoPadding"};
}

Template based type in OBJECTS clause not working.

The bellow code spinet is not parsing:

ABSTRACT SPEC java.lang.String<T>
OBJECTS:
	<T> foo;

Error:
java.lang.AssertionError: Unexpected errors: XtextSyntaxDiagnostic: null:3 required (...)+ loop did not match anything at input '<'

Current grammar does not yet supports function on the left-side of constraint expressions, such as:

part(0, "/", transformation) in ${algorithm}; 

One option is to generalize the current PrimaryConstraintExp rule to accept functions, wildcards parameters, expNatural and expVar, eg:

wildcardParameter: "_"
> expNatural : Natural
| expVar : Id
| functionCall: Id "(" {ParameterDef ","}* ")"

Also needs to implement arithmetic support to deal with expressions such as:

length(pre_plaintext) >= pre_plain_off + len;

List of arithmetic operators to implement:

• +
• -
• <
• <
• <=
• >=
• ==
• !=

These arithmetics operatos can be implemented within the current ConstraintsExp rule (making use of left-factoring). Also needs to deal with associativity. For instance, in the following expression:

length(pre_plaintext) >= pre_plain_off + len;

The + operator has higher precedence than >=

Fix rules that puts EVENTS and ORDER as optional clauses.

The NEGATES section supports invalidating an existing predicate. This is a non-mandatory construct in a CrySL rules.
Example:

NEGATES
keyspec[this , _];

To obtain Variability on the Base Specification Class we need to implement template type parameters in OBJECTS clause. Current grammar does not yet support this.

Example:

ABSTRACT SPEC AbstractFactory<T>
OBJECTS
com.google.crypto.tink.KeysetHandle ksh;
<T> primitive;

Most parsing tests for the grammar are basically the same. @rbonifacio has suggested to automate the generation of these tests. The proposed solution is to look for the sample code files and generate testing methods based on the name of these files.

eg: for a file named testConstraintClause, we could generate a method with this name inside the testing file. We can use some templating language for that.

On branch add-test I have added the test resource structure for Android-cc.

Test cases testAndroidCc0116 and testAndroidCc25plus in MetaCrySLGeneratorTest are failing when they try to apply the refinements associated with the AlgorithmParameters refinement for version 10plus of Android-cc (br.unb.cic.mcsl.tests/test-resources/android-cc/10plus/AlgorithmParameters.ref); so, every configuration that applies this refinement causes the generator test to fail.

Removing this refinement parent directory load expression (load "10plus/") from the configurations in which they are applied (/android-cc/config/Android0116.config and /android-cc/config/Android25plus.config) makes previous cited tests run. When using individual references for each refinement in this folder (e.g. load "10plus/Cipher.ref"), the error occurred only when referring to load "10plus/AlgorithmParameters.ref", what makes me believe that the problem is happening specifically for this refinement.

The content of the cited refinement is:

SPEC AlgorithmParameters REFINES java.security.AlgorithmParameters {
	define algorithm = {"BLOWFISH"};
	
	add constraint alg in {"BLOWFISH"} => preparedIV[params];
}

Could not identify what is causing these tests to fail yet.

To obtain Variability on the Base Specification Class we need to implement template type parameters in SPEC clause. Current grammar does not yet support this.

Example:

ABSTRACT SPEC AbstractFactory<T>

Might be good to load MetaCrySl files (*.cryptsl) from directory in file system. It may help during development and in a future language files maintenance.

Current grammar does not supports meta-variables in CONSTRAINTS clause. To extend #2, we need to add support to meta-variables in CONSTRAINTS clause to deal with Variability on Set Constraints.

Example:

CONSTRAINTS
	randAlg in ${algorithm};

There is an error in ORDER clause. The current grammar rule for ORDER do not accept this construction:

ORDER
	c1, c2?, c3*

Added a failing test file to show the problem (basicModelWithOrderClause2.mcsl).

According to the original grammar file from CROSSING, the CONSTRAINT clause only supports the following functions: "alg" | "mode" | "pad" | "part". Another problem is that a constraint could be formed by the elements operation.

Link: CROSSINGTUD/CryptoAnalysis#178

The CodeWriter should write the resulting .crysl files to the PATH specified in the configuration file. This is not yet implemented.

Some parameters are not being parsed correctly, mainly when they are fully qualified names (maybe this has something to do with #59 ?)

Rules such as these (for Forbidden clause) are not working as well:

FORBIDDEN
	PBEKeySpec(char[]) => c1;
	PBEKeySpec(char[],byte[],int) => c1;

Maybe we should take a look at the FormalParams rule

For some reason, our parser is not accepting expressions of this kind for fully-qualified names

java.security.spec.AlgorithmParameterSpec params;

But it accepts like this (notice the upper case word on the third position)

java.security.Spec.AlgorithmParameterSpec params;