Skip to content

CONSTRAINTS and REQUIRES sections are different from the expected for Cipher.spec #66

@fillypenascimento

Description

@fillypenascimento

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];

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions