Skip to content

Error Types

Jump to bottom
Sven Meyer edited this page Jun 28, 2024 · 1 revision

CryptoAnalysis reports all kinds of errors that violate the CrySL rules. On this page, we give an overview and examples of the different error types. Note that the examples contain simple rules and programs to emphasize the concrete violation, they may not be part of the actual ruleset.

CallToError

CryptoAnalysis reports a CallToError if the predefined predicate callTo in the CONSTRAINTS section is violated. Consider the rule for the class KeyGenerator

SPEC java.security.KeyGenerator

OBJECTS
    java.lang.String algorithm;

EVENTS
    Con: getInstance(algorithm);
    In: init(_);

CONSTRAINTS
    algorithm in {"AES"} => callTo[In];

and the program

KeyGenerator kg = KeyGenerator.getInstance("AES");

In this case, CryptoAnalysis reports a CallToError because using the algorithm AES requires a call to the method init that is missing.

ConstraintError

CryptoAnalysis reports a ConstraintError if a contraint in the CONSTRAINTS section is violated that is not related to predefined predicates. Consider the following rule for the class Signature

SPEC java.security.Signature

OBJECTS
    java.lang.String algorithm;

EVENTS
    Con: getInstance(algorithm);

CONSTRAINTS
    algorithm in {"SHA256withRSA", "SHA512withRSA"};

and the program

Signature signature = Signature.getInstance("SHA1withRSA");

In this case, CryptoAnalysis reports a ConstraintError because the rule does not allow using the algorithm SHA1withRSA.

ForbiddenMethodError

CryptoAnalysis reports a ForbiddenMethodError if there is a call to method from the FORBIDDEN section. Consider the following rule for the class PBEKeySpec

SPEC javax.crypto.spec.PBEKeySpec

FORBIDDEN
    PBEKeySpec(char[]);

and the program

byte[] password = new byte[]{'p', 'w', 'd'};
PBEKeySpec spec = new PBEKeySpec(password);

In this case, CryptoAnalysis reports a ForbiddenMethodError because the rule does not allow the call to the constructor that has only char[] as parameter.

HardCodedError

CryptoAnalysis reports a HardCodedError if the predefined predicate notHardCoded in the CONSTRAINTS section is violated. Consider the following rule for the class PBEKeySpec

SPEC javax.crypto.spec.PBEKeySpec

OBJECTS
    char[] password;

EVENTS
    Con: PBEKeySpec(password);

CONSTRAINTS
    notHardCoded[password];

and the program

byte[] password = new byte[]{'p', 'w', 'd'};
PBEKeySpec spec = new PBEKeySpec(password);

In this case, CryptoAnalysis reports a HardCodedError because the variable password is hard coded (or more general, the concrete value can be extracted from the program).

ImpreciseValueExtractionError

CryptoAnalysis reports an ImpreciseValueExtractionError if it is not able to extract required information to check constraints from the CONSTRAINTS section. Consider the following rule for the class KeyGenerator

SPEC java.security.KeyGenerator

OBJECTS
    java.lang.String algorithm;
    int keysize;

EVENTS
    Con: getInstance(algorithm);
    In: init(keysize);

CONSTRAINTS
    algorithm in {"AES"} => keysize in {128, 256};

and the program

int keysize = (int)(Math.random() * 300);
KeyGenerator kg = KeyGenerator.getInstance("AES");
kg.init(keysize);

In this case, CryptoAnalysis reports an ImpreciseValueExtractionError for the variable keysize because it cannot statically model its value, that is, it cannot extract the precise value, leading to a potential violation of the rule.

IncompleteOperationError

CryptoAnalysis reports an IncompleteOperationError if the operations in the ORDER sections are not completed. Consider the following rule for the class KeyGenerator

SPEC java.security.KeyGenerator

EVENTS
    Con: getInstance(_);
    Init: init(_);
    Gen: generateKey();

ORDER
   Con, Init, Gen

and the program

KeyGenerator kg = KeyGenerator.getInstance("AES");
kg.init(128);

In this case, CryptoAnalysis reports an IncompleteOperationError because a call to generateKey() is missing to complete the sequence of operations in the ORDER section. In this example, the incomplete operation renders the code dead because the KeyGenerator is initialized but not used.

InstanceOfError

CryptoAnalysis reports an InstanceOfError if the predefined predicate instanceOf in the CONSTRAINTS section is violated. Consider the following rule for the class Cipher

SPEC javax.crypto.Cipher

OBJECTS
    java.security.Key key;
    java.lang.String algorithm;

EVENTS
    Con: getInstance(algorithm);
    Init: init(_, key);

CONSTRAINTS
    algorithm in {"RSA"} => instanceOf[key, java.security.PublicKey] || instanceOf[key, java.security.PrivateKey];

and the program

KeyGenerator kg = KeyGenerator.getInstance("AES");
Key key = kg.generateKey();                          // generate a key of type javax.crypto.SecretKey
Cipher cipher = Cipher.getInstance("RSA");
cipher.init(..., key);                               // key has to be of type java.security.PublicKey or java.security.PrivateKey

In this case, CryptoAnalysis reports an InstanceOfError because generateKey() returns a SecretKey, however, the cipher requires a PublicKey or a PrivateKey due to its initialization with the algorithm RSA.

NeverTypeOf

// TODO

NoCallToError

CryptoAnalysis reports a NoCallToError if the predefined predicate noCallTo in the CONSTRAINTS section is violated. Consider the following rule for the class KeyGenerator

SPEC java.security.KeyGenerator

OBJECTS
    java.lang.String algorithm;

EVENTS
    Con: getInstance(algorithm);
    Init: init(_);

CONSTRAINTS
    algorithm in {"RSA"} => noCallTo[Init];

and the program

KeyGenerator kg = KeyGenerator.getInstance("RSA");
kg.init(...);

In this case, CryptoAnalysis reports a NoCallToError because a call to init is not allowed if the algorithm is RSA.

RequiredPredicateError

CryptoAnalysis reports a RequiredPredicateError if predicates in the REQUIRES section are not ensured. Conider the following rules for the classes KeyGenerator and Key.

SPEC java.security.KeyGenerator

OBJECTS
    java.lang.String algorithm;
    java.security.Key key;

EVENTS
    Con: getInstance(algorithm);
    Gen: key = generateKey();

ORDER
    Con, Gen

CONSTRAINTS
    algorithm in {"AES"};

ENSURES
    generatedKey[key];

SPEC java.security.Key

REQUIRES
    generated[this];

and the program

KeyGenerator kg = KeyGenerator.getInstance("RSA");     // "RSA" causes a ConstraintError, i.e. the rule for kg is violated and not secure
Key key = kg.generateKey();                            // kg does not ensure a predicate on the key such that the required predicate 'generatedKey' is violated

In this case, CryptoAnalysis reports a ConstraintError because the algorithm is RSA is not allowed such that the rule for the KeyGenerator is violated and kg is not secure. Therefore, kg does not ensure any predicates such that the predicate generatedKey is not ensured on key which is required. Hence, CryptoAnalysis also reports a RequiredPredicateError to indicate that key is not secure, too.

TypestateError

CryptoAnalysis reports a TypestateError if the order of operations in the ORDER section is violated. Consider the following rule for the class KeyGenerator

SPEC java.security.KeyGenerator

EVENTS
    Con: getInstance(_);
    Init: init(_);
    Gen: generateKey();

ORDER
    Con, Init, Gen

and the program

KeyGenerator kg = KeyGenerator.getInstance(...);
Key key = kg.generateKey();

In this case, CryptoAnalysis reports a TypestateError because it expects a call to 'init' after getInstance and before generateKey.

Clone this wiki locally