CryptoAnalysis icon indicating copy to clipboard operation
CryptoAnalysis copied to clipboard

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

Open rakshitkr opened this issue 5 years ago • 1 comments

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 avatar Feb 07 '20 23:02 rakshitkr

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

rakshitkr avatar Jun 10 '20 08:06 rakshitkr

Fixed in #265

smeyer198 avatar Nov 24 '23 11:11 smeyer198