-
Notifications
You must be signed in to change notification settings - Fork 40
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Merge pull request #522 from CROSSINGTUD/develop
Add detection of subsequent errors to CryptoAnalysis with release 3.1.0
- Loading branch information
Showing
34 changed files
with
1,207 additions
and
482 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
639 changes: 407 additions & 232 deletions
639
CryptoAnalysis/src/main/java/crypto/analysis/AnalysisSeedWithSpecification.java
Large diffs are not rendered by default.
Oops, something went wrong.
91 changes: 91 additions & 0 deletions
91
CryptoAnalysis/src/main/java/crypto/analysis/HiddenPredicate.java
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,91 @@ | ||
package crypto.analysis; | ||
|
||
import com.google.common.collect.Lists; | ||
import com.google.common.collect.Multimap; | ||
import crypto.analysis.errors.AbstractError; | ||
import crypto.analysis.errors.ConstraintError; | ||
import crypto.analysis.errors.HardCodedError; | ||
import crypto.analysis.errors.ImpreciseValueExtractionError; | ||
import crypto.analysis.errors.IncompleteOperationError; | ||
import crypto.analysis.errors.InstanceOfError; | ||
import crypto.analysis.errors.NeverTypeOfError; | ||
import crypto.analysis.errors.RequiredPredicateError; | ||
import crypto.analysis.errors.TypestateError; | ||
import crypto.extractparameter.CallSiteWithParamIndex; | ||
import crypto.extractparameter.ExtractedValue; | ||
import crypto.rules.CrySLPredicate; | ||
|
||
import java.util.List; | ||
import java.util.stream.Collectors; | ||
|
||
public class HiddenPredicate extends EnsuredCrySLPredicate { | ||
|
||
private final AnalysisSeedWithSpecification generatingSeed; | ||
private final HiddenPredicateType type; | ||
|
||
public HiddenPredicate(CrySLPredicate predicate, Multimap<CallSiteWithParamIndex, ExtractedValue> parametersToValues2, AnalysisSeedWithSpecification generatingSeed, HiddenPredicateType type) { | ||
super(predicate, parametersToValues2); | ||
this.generatingSeed = generatingSeed; | ||
this.type = type; | ||
} | ||
|
||
public AnalysisSeedWithSpecification getGeneratingSeed() { | ||
return generatingSeed; | ||
} | ||
|
||
public enum HiddenPredicateType { | ||
GeneratingStateIsNeverReached, | ||
ConstraintsAreNotSatisfied, | ||
ConditionIsNotSatisfied | ||
} | ||
|
||
public HiddenPredicateType getType() { | ||
return type; | ||
} | ||
|
||
/** | ||
* Node: Errors are only in complete count at the end of the analysis. | ||
* @return errors list of all preceding errors | ||
*/ | ||
public List<AbstractError> getPrecedingErrors(){ | ||
List<AbstractError> results = Lists.newArrayList(); | ||
List<AbstractError> allErrors = generatingSeed.getErrors(); | ||
switch(type) { | ||
case GeneratingStateIsNeverReached: | ||
List<AbstractError> typestateErrors = allErrors.stream().filter(e -> (e instanceof IncompleteOperationError || e instanceof TypestateError)).collect(Collectors.toList()); | ||
if(typestateErrors.isEmpty()) { | ||
// Seed object has no typestate errors that might be responsible for this hidden predicate | ||
// TODO: report new info error type to report, | ||
// that the seeds object could potentially ensure the missing predicate which might cause further subsequent errors | ||
// but therefore requires a call to the predicate generating statement | ||
} | ||
|
||
// TODO: check whether the generating state is not reached due to a typestate error | ||
return allErrors; | ||
|
||
case ConstraintsAreNotSatisfied: | ||
// Generating state was reached but constraints are not satisfied. | ||
// Thus, return all constraints & required predicate errors. | ||
return allErrors.stream().filter(e -> (e instanceof RequiredPredicateError || e instanceof ConstraintError || e instanceof HardCodedError || e instanceof ImpreciseValueExtractionError || e instanceof InstanceOfError || e instanceof NeverTypeOfError)).collect(Collectors.toList()); | ||
case ConditionIsNotSatisfied: | ||
// Generating state was reached but the predicates condition is not satisfied. | ||
// Thus, return all errors that causes the condition to be not satisfied | ||
List<AbstractError> precedingErrors = Lists.newArrayList(generatingSeed.retrieveErrorsForPredCondition(this.getPredicate())); | ||
// This method is called from a RequiredPredicateError that wants to retrieve its preceding errors. | ||
// In this case, preceding errors are not reported yet because the predicate condition wasn't required to be satisfied. | ||
// Since the hidden predicate is required to be an ensured predicate, we can assume the condition required to be satisfied. | ||
// Thus, we report all errors that causes the condition to be not satisfied. | ||
precedingErrors.forEach(e -> this.generatingSeed.cryptoScanner.getAnalysisListener().reportError(generatingSeed, e)); | ||
// Further, preceding errors can be of type RequiredPredicateError. | ||
// Thus, we have to recursively map preceding errors for the newly reported errors. | ||
for(AbstractError e: precedingErrors) { | ||
if(e instanceof RequiredPredicateError) { | ||
((RequiredPredicateError)e).mapPrecedingErrors(); | ||
} | ||
} | ||
return precedingErrors; | ||
|
||
} | ||
return results; | ||
} | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.