crossingtud / cryptoanalysis Goto Github PK

CogniCrypt_SAST: CrySL-to-Static Analysis Compiler

License: Eclipse Public License 2.0

Java 100.00%

static-analysis jca cryptoanalysis cryptography misuse-detection command-line-tool java

cryptoanalysis's Introduction

CogniCrypt_SAST

This repository contains CogniCrypt_SAST, the static analysis component for CogniCrypt. The static analysis CogniCrypt_SAST takes rules written in the specification language CrySL as input, and performs a static analysis based on the specification of the rules. CrySL is a domain-specific language (DSL) designed to encode usage specifications for cryptographic libaries (e.g., the JCA in particular). More information on CrySL and the static analysis may be found in this paper.

Releases

You can checkout a pre-compiled version of CogniCrypt_SAST here. We recommend using the latest version.

Download the two files:

CryptoAnalysis-x.y.z-jar-with-dependencies.jar
JCA-CrySL-rules.zip

You can find CogniCrypt_SAST also on Maven Central.

Checkout and Build

CogniCrypt_SAST uses Maven as build tool. You can compile and build this project via

mvn package -DskipTests=true.

A packaged jar artifact including all dependency is found in CryptoAnalysis/build/CryptoAnalysis-x.y.z-jar-with-dependencies.jar. Building requires at least Java 11.

Usage

CogniCrypt_SAST can be started in headless mode (i.e., detached from Eclipse) via the class crypto.HeadlessCryptoScanner. It requires two arguments:

The path to the directory of the CrySL (source code format) rule files. The source code for the rules which contain specification for the JCA is found here.
The path of the application to be analyzed (.jar file or the root compilation output folder which contains the .class files in subdirectories)

java -cp <path-to-analysis-jar> crypto.HeadlessCryptoScanner 
      --rulesDir <path-to-crysl-source-code-format-rules> 
      --appPath <application-path>

For an easy start we prepared a .jar containing classes with crypto misuses. The source code for these misuses is found here. To run CogniCrypt_SAST on these classes, simply execute the following command (on a linux based system).

java -cp CryptoAnalysis/build/CryptoAnalysis-x.y.z-jar-with-dependencies.jar crypto.HeadlessCryptoScanner 
  --rulesDir $(pwd)/CryptoAnalysis/src/main/resources/JavaCryptographicArchitecture 
  --appPath $(pwd)/CryptoAnalysisTargets/CogniCryptDemoExample/Examples.jar

Other additional arguments that can be used are as follows:

--cg <selection_of_call_graph_for_analysis> (possible values are CHA, SPARK, SPARKLIB)
--sootPath <absolute_path_of_whole_project>
--identifier <identifier_for_labeling_output_files>
--reportPath <directory_location_for_cryptoanalysis_report>
--reportFormat <format of cryptoanalysis_report> (possible values are CMD, TXT, SARIF, CSV, CSV_SUMMARY)
--preanalysis (enables pre-analysis)
--visualization (enables the visualization, but also requires --reportPath option to be set)
--providerDetection (enables provider detection analysis)
--dstats (disables the output of the analysis statistics in the reports)
--ignoreSections (Text file with packages (e.g. `de.example.*`), classes (e.g. `de.example.exmapleClass`) or methods (e.g. `de.example.exampleClass.exampleMethod`), one per line. Those packages, classes and methods are ignored during the analysis)
--help (show more information for the CLI arguments)

Note, depending on the analyzed application, the analysis may require a lot of memory and a large stack size. Remember to set the necessary heap size (e.g. -Xmx8g) and stack size (e.g. -Xss60m).

Use as a GitHub Action

CogniCrypt_SAST can be used as a GitHub action.

- name: Run CogniCrypt
  uses: CROSSINGTUD/CryptoAnalysis@version
  with:
    appPath: "CryptoAnalysisTargets/HelloWorld/HelloWorld.jar"
    basePath: "CryptoAnalysisTargets/HelloWorld"

The appPath needs to be configured to point to a compiled version of your application.

The basePath is used to relate paths in the analyzed jar and the source tree. Class com.example is searched for at basePath/com/example.

See action.yml for all input options.

Report and Error Types

CogniCrypt_SAST reports misuses when the code is not compliant with the CrySL rules. For each misuse, CogniCrypt_SAST reports the class and the method the misuse is contained in. There are multiple misuse types:

ConstraintError: A constraint of a CrySL rule is violated, e.g., a key is generated with the wrong key size.
NeverTypeOfError: Reported when a value was found to be of a certain reference type: For example, a character array containing a password should never be converted from a String. (see KeyStore rule here).
ForbiddenMethodError: A method that is forbidden (CrySL block FORBIDDEN) to be called under some circumstances was found.
ImpreciseValueExtractionError: The static analysis was not able to extract all information required within the CrySL CONSTRAINT block. For example the key size could be supplied as a value listed in a configuration file. The static analysis does not model the file's content and may not constraint on the value.
TypestateError: The ORDER block of CrySL is violated, i.e., the expected method sequence call to be made is incorrect. For example, a Signature object expects a call to initSign(key) prior to update(data).
RequiredPredicateError: An object A expects an object B to have been used correctly (CrySL blocks REQUIRES and ENSURES). For example a Cipher object requires a SecretKey object to be correctly and securely generated.
IncompleteOperationError: The usage of an object may be incomplete: For example a Cipherobject may be initialized but never used for en- or decryption, this may render the code dead. This error heavily depends on the computed call graph (CHA by default).
UncaughtExceptionError: A method may throw an exception, but the exception is not caught in the program. For example, the method call is not surrounded by a try/catch block.

CogniCrypt_SAST supports different report formats, which can be set by using --reportformat option. The supported formats are:

CMD: The report is printed to the command line. The content is equivalent to the format from the TXT option.
TXT: The report is written to the text file CryptoAnalysis-Report.txt. The content is equivalent to the format from the CMD option. Additionally, the .jimple files of the classes, where misuses were found in, are output. Jimple is an intermediate representation close to the syntax of Java.
SARIF: The report is written to the JSON file CryptoAnalysis-Report.json. The content is formatted in the SARIF format.
CSV: The report is written to the CSV file CryptoAnalysis-Report.csv. The content is formatted in the CSV format.
CSV_SUMMARY: The report is written to the file CryptoAnalysis-Report-Summary.csv and contains a summary of the analysis results. Compared to the CSV format, this format does not provide concrete information about the errors, it only lists the amount of each misuse type. This option was previously implemented by the CSV option, which has been changed to provide more detailed information about the errors in the CSV format.
GITHUB_ANNOTATION: Works like CMD but also outputs all violations as annotations when running inside as a GitHub Action.

If the --reportformat option is not specified, CogniCrypt_SAST defaults to the CMD option. It also allows the usage of multiple different formats for the same analysis (e.g. --reportformat CMD,TXT,CSV creates a report, which is printed to the command line and is written to a text and CSV file). If the option --reportPath <directory_location_for_cryptoanalysis_report> is set, the reports are created in the specified directory.

Updating CrySL Rules

The tool takes CrySL rules in their source code formats (crysl). You can adapt the rules in any text editor. Additionaly, the Eclipse plugin CogniCrypt ships with a CrySL editor to modify the rules with IDE support (e.g., content assist, auto completion, etc.). A step-by-step-explanation on how edit CrySL rules is avialable at the tool's website cognicrypt.org.

CogniCrypt_SAST for Android Applications

CogniCrypt_SAST can also be run on Android Applications using the Android version for CogniCrypt_SAST in CryptoAnalysis-Android. Its usage does not deviate much from regular CogniCrypt_SAST's. CogniCrypt_SAST for Android can be started via the class de.fraunhofer.iem.crypto.CogniCryptAndroidAnalysis. It requires three arguments in this order:

The absolute path to the .apk file
The absolute path to the android SDK platforms. The platforms are obtainable via Android Studio. Under the Android SDK location you find a folder platforms. Supply CogniCrypt_SAST with the path to this folder.
The absolute path to the directory of the CrySL rules.

java -cp <path-to-analysis-jar> -Xmx8g -Xss60m de.fraunhofer.iem.crypto.CogniCryptAndroidAnalysis \
      <path-to-apk> <path-to-android-platforms> <path-to-crysl-rules>

As an optional fourth parameter one can specify an output folder:

java -cp <path-to-analysis-jar> -Xmx8g -Xss60m de.fraunhofer.iem.crypto.CogniCryptAndroidAnalysis \
      <path-to-apk> <path-to-android-platforms> <path-to-crysl-rules> <output-dir>

If specified, the analysis generates a report file CogniCrypt-Report.txt along with the .jimple output of the classes the analysis found misuses in. The format of the report file follows that described above.

Note, depending on the analyzed application, the analysis may require a lot of memory and a large stack size. Remember to set the necessary heap size (e.g. -Xmx8g) and stack size (e.g. -Xss60m).

cryptoanalysis's People

Contributors

Stargazers

Watchers

cryptoanalysis's Issues

Error reporting: Differentiate between Application and Android packages.

StateMachineGraph uses Lists instead of Sets to maintain the States and Edges

Missing predicate warning

In the following example, there is a parameter mismatch for KeyPairGenerator.getInstance("AES") (should be RSA). CC correctly shows an error at this line, but it does not show the "unfulfilled predicate" at the line signature.initSign(getPrivateKey());

This is different for typestate errors: when I comment out gen.initialize(1024); then the predicate error is shown.

public byte[] sign(String data) throws Exception {
	Signature signature = Signature.getInstance("SHA256withRSA");
	signature.initSign(getPrivateKey());
	signature.update(data.getBytes());
	return signature.sign();
}

private PrivateKey getPrivateKey() throws NoSuchAlgorithmException {
	KeyPairGenerator gen = KeyPairGenerator.getInstance("AES");
	gen.initialize(1024);
	KeyPair keyPair = gen.generateKeyPair();
	return keyPair.getPrivate();
}

typestateErrorAt should only be called once

Right now, if the type-state analysis detects an unexpected method call, it transitions the FSM into an error state and the method typestateErrorAt in the reports listener is being called at each statement after the original wrong method call. Instead, the method should only be called once - the first time the error state is reached.

Error in SecureRandom specification

The method name for the transition nextBytes(...) for SecureRandom is wrong.

When I retrieve the method name from the CryptSLMethod I get "java.util.Random.nextBytes". It should be "java.security.SecureRandom.nextBytes" instead. The declaring class is wrong.

That is weird, where does the the declaring class come from? Isn't it specified implicitlty by the rule? But nextBytes is specified in java.security.SecureRandom.

I intentionally hard-coded the correct method specification. When fixing the issue, please remove this hard-coding as well.

Implement TypestateErrorEndOfLife

Method typestateErrorEndOfLife in the reports listener should be called whenever an object reaches the end of its life and is not an accepting state. Please implement.

KeyStore generates predicate generatedPrivkey

A private key may also be loaded from a keystore, the analysis reports a missing predicate error here.

        $r42 = virtualinvoke r1.<java.security.KeyStore: java.security.Key getKey(java.lang.String,char[])>($r40, $r41);

        r109 = (java.security.PrivateKey) $r42;

        virtualinvoke r108.<java.security.Signature: void initSign(java.security.PrivateKey)>(r109);

Refactor the order transformation

All states should be accepting states in SecretKey rule

According to the specification, every state of SecretKey spec should be an accepting state. All calls are labeled as optional.

To circumvent this, I hardcoded an if-stmt in the code. Please remove it, once done.

Enable CI for this repository

Remove WPDS submodule and include a fixed version, the development of WPDS is stable by now. Hereby executing the tests for CryptoAnalysis will not execute the tests for WPDS.

Adjust test cases to new Benchmark methods

In UsagePatternTest we specified which Parameters the analysis has to extract, whether the object may or may not be in an error state. Done by the calls to the static methods within Benchmark.

We have to adjust the TestingFramework to read and extract this information from the code and fail the test when one information is missing/wrong.

Add test cases for Signature

TypestateErrorAt should receive expected method calls as parameter

How to handle "this" in predicate?

With a predicate genSth(this, alg, _, balg), there will be no variable in the whole smg that needs to be tracked forward because it is the object itself that should be tracked. Does this require special handling somehow somewhere?

Use new structure of StateMachineGraph to match SootMethods

Always check internal constraints

Re-build rulesets for CryptoLint and CMA

Use Sable/soot dependency instead of johspaeth/soot

We currently import the soot git accessible here:

https://github.com/johspaeth/soot

we might want to create a branch of the original soot here:

https://github.com/sable/soot

Use threading in the analysis

Distinguish between CI and GUI Modus

Forbidden methods for PBEKeySpec is not specified correctly.

The list of forbidden methods for PBEKeySpec delivers a list of nulls.

PBEKeySpec
forbiddenMethods:null,null,null,null,

I expected at least the constructors with 2 and 3 arguments here.

How to handle pre-defined predicates

These include:

callTo
noCallTo
neverTypeOf

Serialization of Cipher.cryptslbin

The test cases for UsagePatternTest (#2) require the CryptSLRule for Cipher.

Add test cases for messageDigest

SecureRandom specification has two initial transitions

Left: pre_init ====[java.security.SecureRandom();, java.security.SecureRandom(byte[] seed (true),);]====> Right:0
Left: pre_init ====[java.security.SecureRandom.getInstance(java.lang.String alg (true),);, java.security.SecureRandom.getInstance(java.lang.String alg (true),AnyType _ (true),);, java.security.SecureRandom.getInstanceStrong();]====> Right:0

There should be just one transition from pre_init -> 0 with the set union of the methods that ought to be selected.

Move maven-plugin related code to a new repository

The code within cognicrypt-maven-plugin is the source code for the maven plugin.

Task: Move the code to a different repository and either include this repository as a submodule or add this project as a dependency within the pom.xml file.

SecretKeySpec rule delivers wrong predicate parameters

During the analysis I retrieve "P:keySpec(,,)" as predicate to be ensured on the rule SecretKeySpec.
From the specification I expect "P:keySpec(this,_,)".

Revert commit listed below to remove hardcoded fix.

Verbose static analysis output

Improve the logging output of the analysis to provide more detailed information about the performance of the analysis.

Analysis does not find issue when passing wrong algorithm as parameter

I made a test in a corresponding branch to demonstrate what I found. I'm unsure whether this is known behavior or a bug.

https://github.com/CROSSINGTUD/CryptoAnalysis/tree/issue-%2353-behaviour-differs-with-parameter

KeyGenerator keygen = KeyGenerator.getInstance("AES");
This is detected as an error.

String trans = "AES";
KeyGenerator keygen = KeyGenerator.getInstance(trans);

This is not detected as an error.

Re-implement full predicate check

CryptSLMethod should not list the return value inside the parameter List.

We discussed that CryptSLMethod should have a method that returns and Optional name of the returned value.

The return value should also not be listed within the "parameters" List of the object. I.e. the length ot the parameter list should be what it is :)

I also think that we can remove the function getBackward() sooner(!) or later.

Analysis crashes when run on our own CryptoAnalysis-1.0.0-jar-with-dependencies.jar file

When the analysis is run on the own jar file, the analysis crashes. (see strack trace below)

Soot reads in the jar file incorrectly and tries to load a class with a prefix

META-INF.version9.

Debug where this prefix comes from and why the analysis crashes.

java -cp CryptoAnalysis-1.0.0-jar-with-dependencies.jar crypto.HeadlessCryptoScanner --rulesDir=<path-to-rules> --applicationCp=<path-to-har>/CryptoAnalysis-1.0.0-jar-with-dependencies.jar 
Using call graph algorithm CHA
Exception in thread "main" java.lang.RuntimeException: Class names not equal! org.apache.logging.log4j.core.util.SystemClock != META-INF.versions.9.org.apache.logging.log4j.core.util.SystemClock
at soot.asm.SootClassBuilder.visit(SootClassBuilder.java:99)
at org.objectweb.asm.ClassReader.accept(ClassReader.java:637)
at org.objectweb.asm.ClassReader.accept(ClassReader.java:521)
at soot.asm.AsmClassSource.resolve(AsmClassSource.java:62)
at soot.SootResolver.bringToHierarchyUnchecked(SootResolver.java:240)
at soot.SootResolver.bringToHierarchy(SootResolver.java:212)
at soot.SootResolver.bringToSignatures(SootResolver.java:273)
at soot.SootResolver.bringToBodies(SootResolver.java:313)
at soot.SootResolver.processResolveWorklist(SootResolver.java:167)
at soot.SootResolver.resolveClass(SootResolver.java:137)
at soot.Scene.loadClass(Scene.java:861)
at soot.Scene.loadClassAndSupport(Scene.java:847)
at soot.Scene.loadNecessaryClasses(Scene.java:1602)
at crypto.HeadlessCryptoScanner.initializeSootWithEntryPointAllReachable(HeadlessCryptoScanner.java:304)
at crypto.HeadlessCryptoScanner.exec(HeadlessCryptoScanner.java:149)
at crypto.HeadlessCryptoScanner.main(HeadlessCryptoScanner.java:61)

Extract Values on Call-Flow and Return-Flow

If the class of a CrySL rule is included and the method of this class has active bodies, the value extraction does not extract any values.

At the moment, the value extraction is only triggered through the call-to-return flow. Which means the value extraction does not work, if any of the classes of the rules is on the include list for Soot.

This needs a major refactoring. It probably makes sense to decouple the typestate analysis from the Value Extraction analysis.

Reporting of Predicates

Kill ensured predicates

How to handle size evaluation

Return value of CryptSLMethod.getRetObject().getValue()

To determine the return type of a CryptSLMethod the methods CryptSLMethod.getRetObject().getValue()
are used.

But for methods with return type "VOID" the result of CryptSLMethod.getRetObject().getValue() is "AnyType" instead of "void".

IncompleteOperationErrors are imprecise

The analysis generates a lot of IncompleteOperationErrors.

Extend the test cases found here to test more thoroughly for these errors.

PBEKeySpec should have a CryptSLCondPredicate

The predicate "keypsec" that shall be generated should be a conditional predicate, i.e. CryptSLCondPredicate, but it is a regular predicate of type CryptSLPredicate.

CalltoForbiddenMethod should include alternate call(s)

Cipher specification misses a transition

The typestate test case test.cipher.CipherTest testCipher4 fails because the Cipher state machine misses a transition.
When I look at the generated state machine graph, doFinal cannot be invoked multiple times as specified in the test case testCipher4.

Cipher state machine is not in an accepting state after call to doFinal

Cipher
Usage Pattern:Name: pre_init( init: true; accept: false)
Name: 0( init: false; accept: false)
Name: 1( init: false; accept: false)
Name: 2( init: false; accept: false)
Name: 3( init: false; accept: false)

All states of the state machine are non-accepting. (At least) State 2 should be an accepting state

Move Android-specific parts of this repository to a new repository

We should move the code that is specific to android to an extra repository.

The following folders/components can be moved

infoflow-android - FlowDroid - only required for the computation of an Android call graph
infoflow - Transitive Dependency, infoflow-android depends on this project.
android-callgraph - Code to execute a CogniCrypt analysis on an android App.

Implement proper hashCode and equals Methods for CryptSLPredicate

Hashcode and equals methods of CryptSLPredicate must be symmetric.

CryptSLPredicates are put in HashSets.

Object must be in an accepting state at the end of the object's lifetime

Include CogniCryptExample-Project and run static analysis in headless mode

Get the template code from here
Use CogniCrypt to generate code into the projects.
Specify how many error markes you expect on the project (hopefully none) in an additional HeadlessTest

A collection of RefType is not necessary in FiniteStateMachineToTypestateChangeFunction

The SootMethods returned by initialTransitonLabel() in SootBasedStateMachineGraph are expected to be of a single type.

Fix parameters in missingPredicates

Two issues:

Missing predicates receives a set of missing predicates, not just one.
It does not get any location information, so there is no way to generate the error marker.

Add license

Parse and read-in CrySL rules in source code format

CogniCrypt_SAST requires CrySL rules in binary format (cryptslbin) as input. The binary format can only be produced by the eclipse plugin CogniCrypt. To make CogniCrypt_SAST more user-friendly, it should accept CrySL rules in source code format as input.