Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

OR fails when none of the predicates in REQUIRES section are ensured #216

Closed
rakshitkr opened this issue Feb 7, 2020 · 2 comments
Closed
Assignees

Comments

@rakshitkr
Copy link
Contributor

Scenario 1 (works fine): creating RSAKeyParameters or others properly and passing it to RSAEngine.init method
Scenario 2 (doesn't work as expected): creating any incorrectly and passing it to RSAEngine.init method

Analysis doesn't give any RequiredPredicateError for the below program.

byte[] message = new byte[100];
RSAEngine engine2 = new RSAEngine();
engine2.init(false, null); //  expecting such error here
byte[] cipherText2 = engine2.processBlock(message, 0, message.length);

EXPECTED OUTPUT

RequiredPredicateError violating CrySL rule for org.bouncycastle.crypto.engines.RSAEngine
			Second parameter was not properly generated as generated generated R S A Key Parameters Or R S A Private Crt Key Parameters Or E C Public Key Parameters
			at statement: virtualinvoke r2.<org.bouncycastle.crypto.engines.RSAEngine: void init(boolean,org.bouncycastle.crypto.CipherParameters)>(varReplacer0, varReplacer1)

EXISTING OUTPUT

No violations

This behaviour is happening because of OR-ing of predicates in RSAEngine rule. For eg. The below rule for RSAEngine is used to test this scenario.

SPEC org.bouncycastle.crypto.engines.RSAEngine

OBJECTS
	org.bouncycastle.crypto.CipherParameters params;
	
	boolean is_encryption;
	byte[] cipherText;
	
EVENTS
	c : RSAEngine();
	
	i : init(is_encryption, params);
	
	p : cipherText = processBlock(_, _, _);
	
ORDER
	c, (i, p)+
	
REQUIRES
	generatedRSAKeyParameters[params] || generatedRSAPrivateCrtKeyParameters[params] || generatedECPublicKeyParameters[params];
	
ENSURES
	generatedRSAEngine[this] after c;
	encrypted[cipherText] after p;
rakshitkr added a commit that referenced this issue Feb 8, 2020
This commit updates the error counts of testBCEllipticCurveExamples headless tests to handle false negatives related to CryptSL/issue-11
@kruegers kruegers self-assigned this Feb 18, 2020
@kruegers kruegers assigned rakshitkr and unassigned kruegers May 29, 2020
@rakshitkr
Copy link
Contributor Author

@AnakinSklavenwalker I've fixed the above issue. Please review the code. Thanks...

@smeyer198
Copy link
Contributor

Fixed in #265

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

3 participants