Writing new MARK rules

[shahrzadav]

I tried to make new MARK rules for JCA. I created an entity file and a rule file for each class and I write rules like this:

...
rule JCAProvider_PBEParameterSpec_2{
	using
		PBEParameterSpec as pbeps,
		SecureRandom as sr
	ensure
		_is(pbeps.salt, sr)
	onfail
		NotRandomizedSaltPBEParameterSpec
}
...

but the problem is when I try analysis on a test project with this new ruleset, I see multiple errors on one line and most of them are not even related to that line. Can you please tell me what is wrong? here is the error message (the result of analysis):

Multiple markers at this line
	- Rule JCAProvider_PBEParameterSpec_2 violated
	- Rule JCAProvider_AlgorithmParameterGenerator_5 
	 violated
	- Rule JCAProvider_SecureRandom_3 violated
	- Rule JCAProvider_SecureRandom_2 verified
	- Rule JCAProvider_SSLContext_5 violated
	- Rule JCAProvider_SecureRandom_4 violated
	- Verified Order: JCAProvider_SecureRandom_1
	- Rule JCAProvider_PBEKeySpec_4 violated

and here is the line of code: SecureRandom secureRandom = SecureRandom.getInstance("SHA1PRNG");

Note: PBEParameterSpec is not even used in the test project.

[fwendland]

Hi @shahrzadav

I assume all these rules are your own. Without knowing all the rules it's difficult to say, why Codyze marks a specific line with all these rule checks.

For one, are the rules evaluated incorrectly? Does the problem they indicate exist? Or are these spurious evalutations?

Side note: We have small code samples to test specific rules. However, these small samples often violate some other rule. We recently added a the method containsFinding() in AbstractMarkTest (https://github.com/Fraunhofer-AISEC/codyze/blob/f0115b0ce72bf363b6bdf0836511a0507c7d19e5/src/test/java/de/fraunhofer/aisec/crymlin/AbstractMarkTest.java#L165). This method checks only against a set of specific findings instead of verifying all of them. This helps us to ignore findings, we know to appear in the analysis, and focus on the ones we're actually interested in.

[shahrzadav]

Hi @fwendland, yes, I use only all the rules that I wrote. I wrote them based on the JCA ruleset of CrySL (https://github.com/CROSSINGTUD/Crypto-API-Rules/tree/master/JavaCryptographicArchitecture/src). For each class, there is a CrySL rule that described the correct usage of it. For that line of code, there should not be any errors (the only thing that can go wrong there is the algorithm, which is correct in this case). But as you can see, some others rules have been checked for that line of code that are unrelated! I made a repository for the rules I made. I will give you access; would you please check that? https://github.com/shahrzadav/TranslatedRules

[shahrzadav]

Hi @fwendland, were you able to check the MARK rules I made?

[fwendland]

Hi @shahrzadav,

Sorry, it slipped my mind. Thank you for the reminder.

I've taken a look at your code and just pushed a simple mwe: fw/issue-219. I see that the rule is triggered and evaluated as violated. This behavior is somewhat expected.

The analysis process tries to find matching nodes for the entities SecureRandom and PBEParameterSpec. For the latter it cannot find a node. Hence, it returns an error. The ensure part of the rule is now evaluated with an error value causing it to fail and returning violated.

To prevent these kinds of problems, you need to define appropriate when clauses the restrict the cases when a rule is evaluated. In general all rules are evaluated that don't define an exclusion via when. These rules are supposed to always hold that's why they are evaluated in the first place.

We may reconsider the evaluation. There are some cases where rule evaluations could be conditional on the matching of entities in a using clause.