Skip to content

Commit

Permalink
Adapt tests to new constraints evaluation
Browse files Browse the repository at this point in the history
  • Loading branch information
smeyer198 committed Jan 8, 2025
1 parent cc2fd33 commit 7b69874
Show file tree
Hide file tree
Showing 13 changed files with 149 additions and 59 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -46,11 +46,12 @@ public AlternativeReqPredicateError(
IAnalysisSeed seed,
Statement statement,
CrySLRule rule,
Collection<CrySLPredicate> predicates,
Collection<AbstractConstraintsError> violatedPredicateErrors) {
Collection<CrySLPredicate> allPredicates,
Collection<AbstractConstraintsError> missingPredicates) {
super(seed, statement, rule, new HashSet<>());

this.contradictedPredicate = predicates;
this.contradictedPredicate = allPredicates;
this.relevantPredicates = new HashSet<>();
}

public Collection<CrySLPredicate> getContradictedPredicate() {
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -42,7 +42,7 @@ public String toErrorMarkerString() {
return "Constraint "
+ evaluableConstraint
+ " on object "
+ getSeed().getFact()
+ getSeed().getFact().getVariableName()
+ " is violated due to the following reasons:";
}

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,6 @@
import crypto.extractparameter.ExtractedValue;
import crypto.extractparameter.ParameterWithExtractedValues;
import crysl.rule.CrySLRule;
import crysl.rule.ISLConstraint;
import java.util.Objects;

public class ImpreciseValueExtractionError extends AbstractConstraintsError {
Expand All @@ -23,18 +22,6 @@ public ImpreciseValueExtractionError(
this.violatedConstraint = constraint;
}

public ImpreciseValueExtractionError(
IAnalysisSeed seed, Statement errorStmt, CrySLRule rule, ISLConstraint constraint) {
super(seed, errorStmt, rule);

violatedConstraint = null;
}

private enum ConstraintType {
ValueConstraint,
ComparisonConstraint,
}

public ImpreciseValueExtractionError(
AnalysisSeedWithSpecification seed,
Statement statement,
Expand All @@ -44,7 +31,7 @@ public ImpreciseValueExtractionError(
EvaluableConstraint constraint) {
super(seed, statement, rule);

violatedConstraint = null;
violatedConstraint = constraint;
}

public EvaluableConstraint getViolatedConstraint() {
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -368,6 +368,11 @@ public ArithmeticLength(
public IntermediateResult evaluate(Statement statement) {
return new IntermediateResult(Collections.emptySet(), Collections.emptySet());
}

@Override
public String toString() {
return predicate.toString();
}
}

private record IntermediateResult(
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -7,6 +7,8 @@
import crypto.analysis.AnalysisSeedWithSpecification;
import crypto.analysis.errors.AbstractConstraintsError;
import crypto.analysis.errors.AlternativeReqPredicateError;
import crypto.analysis.errors.PredicateContradictionError;
import crypto.analysis.errors.RequiredPredicateError;
import crypto.definition.Definitions;
import crypto.extractparameter.ExtractParameterAnalysis;
import crypto.extractparameter.ParameterWithExtractedValues;
Expand Down Expand Up @@ -226,8 +228,6 @@ private Collection<AbstractConstraintsError> evaluateAlternativeReqPredicate(
return errors;
}

boolean satisfied = false;

Multimap<Statement, AbstractConstraintsError> statementToErrors = HashMultimap.create();
for (CrySLPredicate predicate : predicates) {
EvaluableConstraint constraint =
Expand All @@ -238,12 +238,20 @@ private Collection<AbstractConstraintsError> evaluateAlternativeReqPredicate(
for (AbstractConstraintsError error : constraint.getErrors()) {
statementToErrors.put(error.getErrorStatement(), error);
}

satisfied |= constraint.isSatisfied();
}

if (!satisfied) {
for (Statement statement : statementToErrors.keySet()) {
for (Statement statement : statementToErrors.keySet()) {
Collection<CrySLPredicate> ensuredPreds = new HashSet<>(predicates);

for (AbstractConstraintsError error : statementToErrors.get(statement)) {
if (error instanceof RequiredPredicateError reqPredError) {
ensuredPreds.remove(reqPredError.getContradictedPredicates());
} else if (error instanceof PredicateContradictionError predContradictionError) {
ensuredPreds.remove(predContradictionError.getContradictedPredicate());
}
}

if (ensuredPreds.isEmpty()) {
AlternativeReqPredicateError error =
new AlternativeReqPredicateError(
seed,
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -49,7 +49,9 @@ public EvaluationResult evaluate() {
allowedValues = formatAllowedValues(allowedValues);

for (ParameterWithExtractedValues parameter : relevantParameters) {
// TODO Collect not allowed values and report a single error with them
for (ExtractedValue extractedValue : parameter.extractedValues()) {
// TODO Extract call sites that are not part of the dataflow scope
if (extractedValue.val().equals(Val.zero())
|| (!extractedValue.val().isConstant() && !extractedValue.val().isNull())) {
ImpreciseValueExtractionError error =
Expand Down
Original file line number Diff line number Diff line change
@@ -1,6 +1,8 @@
import javax.crypto.SecretKeyFactory;
import javax.crypto.spec.PBEKeySpec;
import java.security.SecureRandom;
import java.util.stream.Collectors;
import java.util.stream.IntStream;

public class TrueNegative {

Expand All @@ -13,10 +15,12 @@ public void trueNegative() {
secureRandom.nextBytes(pass);

// convert byte array to char array
char[] passwd = new char[pass.length];
for(int i=0; i < pass.length; i++){
passwd[i] = (char) (pass[i]&0xff);
}
char[] passwd = IntStream
.range(0, salt.length)
.map(i -> (char) (pass[i]&0xff))
.mapToObj(Character::toString)
.collect(Collectors.joining())
.toCharArray();

byte[] key = getKey(passwd, salt, 10000, 256);
}
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -52,6 +52,7 @@ public void testBCMacExamples() {

addErrorSpecification(
new ErrorSpecification.Builder("bunkr.PBKDF2Descriptor", "calculateRounds", 1)
.withTPs(ImpreciseValueExtractionError.class, 2)
.withTPs(TypestateError.class, 2)
.withTPs(IncompleteOperationError.class, 1)
.build());
Expand Down Expand Up @@ -79,13 +80,14 @@ public void testBCSymmetricCipherExamples() {
addErrorSpecification(
new ErrorSpecification.Builder(
"gcm_aes_example.GCMAESBouncyCastle", "processing", 2)
.withTPs(ImpreciseValueExtractionError.class, 2)
.withTPs(RequiredPredicateError.class, 2)
.withTPs(AlternativeReqPredicateError.class, 1)
.build());
addErrorSpecification(
new ErrorSpecification.Builder(
"gcm_aes_example.GCMAESBouncyCastle", "processingCorrect", 2)
.withTPs(RequiredPredicateError.class, 0)
.withTPs(ImpreciseValueExtractionError.class, 2)
.build());

addErrorSpecification(
Expand Down Expand Up @@ -115,8 +117,13 @@ public void testBCAsymmetricCipherExamples() {
.build());
addErrorSpecification(
new ErrorSpecification.Builder("rsa_misuse.RSATest", "Decrypt", 2)
.withTPs(ImpreciseValueExtractionError.class, 2)
.withTPs(AlternativeReqPredicateError.class, 1)
.build());
addErrorSpecification(
new ErrorSpecification.Builder("rsa_nomisuse.RSATest", "Decrypt", 2)
.withTPs(ImpreciseValueExtractionError.class, 2)
.build());

// These two errors occur because AsymmetricCipherKeyPair ensures the predicate only after
// the constructor call
Expand All @@ -129,35 +136,58 @@ public void testBCAsymmetricCipherExamples() {
.withTPs(AlternativeReqPredicateError.class, 1)
.build());

addErrorSpecification(
new ErrorSpecification.Builder("crypto.RSAEngineTest", "testEncryptOne", 0)
.withTPs(ImpreciseValueExtractionError.class, 1)
.withTPs(AlternativeReqPredicateError.class, 1)
.build());
addErrorSpecification(
new ErrorSpecification.Builder("crypto.RSAEngineTest", "testEncryptTwo", 0)
.withTPs(ImpreciseValueExtractionError.class, 1)
.withTPs(TypestateError.class, 1)
.build());
addErrorSpecification(
new ErrorSpecification.Builder("crypto.RSAEngineTest", "testDecryptOne", 1)
.withTPs(RequiredPredicateError.class, 2)
.withTPs(AlternativeReqPredicateError.class, 1)
.withTPs(ImpreciseValueExtractionError.class, 1)
.withTPs(ImpreciseValueExtractionError.class, 4)
.build());
addErrorSpecification(
new ErrorSpecification.Builder("crypto.RSAEngineTest", "testDecryptTwo", 1)
.withTPs(TypestateError.class, 1)
.withTPs(RequiredPredicateError.class, 2)
.withTPs(ImpreciseValueExtractionError.class, 1)
.withTPs(ImpreciseValueExtractionError.class, 4)
.build());
addErrorSpecification(
new ErrorSpecification.Builder(
"params.RSAPrivateCrtKeyParametersTest", "testOne", 0)
.withTPs(ImpreciseValueExtractionError.class, 2)
.withTPs(RequiredPredicateError.class, 2)
.build());

addErrorSpecification(
new ErrorSpecification.Builder("params.RSAKeyParametersTest", "testOne", 0)
.withTPs(ImpreciseValueExtractionError.class, 1)
.build());
addErrorSpecification(
new ErrorSpecification.Builder("params.RSAKeyParametersTest", "testTwo", 0)
.withTPs(ImpreciseValueExtractionError.class, 1)
.build());

addErrorSpecification(
new ErrorSpecification.Builder("generators.RSAKeyPairGeneratorTest", "testTwo", 0)
.withTPs(RequiredPredicateError.class, 1)
.build());
addErrorSpecification(
new ErrorSpecification.Builder("params.ParametersWithRandomTest", "testOne", 0)
.withTPs(ImpreciseValueExtractionError.class, 1)
.withTPs(AlternativeReqPredicateError.class, 1)
.build());
addErrorSpecification(
new ErrorSpecification.Builder("params.ParametersWithRandomTest", "testTwo", 0)
.withTPs(ImpreciseValueExtractionError.class, 1)
.withTPs(RequiredPredicateError.class, 1)
.withTPs(AlternativeReqPredicateError.class, 1)
.build());
addErrorSpecification(
new ErrorSpecification.Builder("generators.RSAKeyPairGeneratorTest", "testThree", 0)
Expand Down Expand Up @@ -186,7 +216,7 @@ public void testBCDigestExamples() {
addErrorSpecification(
new ErrorSpecification.Builder("pattern.DigestTest", "digestWithMultipleUpdates", 0)
.withTPs(TypestateError.class, 1)
.withTPs(ImpreciseValueExtractionError.class, 1)
.withTPs(ImpreciseValueExtractionError.class, 2)
.build());

addErrorSpecification(
Expand All @@ -201,6 +231,11 @@ public void testBCDigestExamples() {
.withTPs(ForbiddenMethodError.class, 1)
.withTPs(RequiredPredicateError.class, 1)
.build());
addErrorSpecification(
new ErrorSpecification.Builder(
"inflatable_donkey.KeyBlobCurve25519Unwrap", "curve25519Unwrap", 4)
.withTPs(ImpreciseValueExtractionError.class, 4)
.build());

addErrorSpecification(
new ErrorSpecification.Builder("fabric_api_archieve.Crypto", "sign", 2)
Expand All @@ -217,12 +252,12 @@ public void testBCDigestExamples() {
new ErrorSpecification.Builder(
"pluotsorbet.BouncyCastleSHA256", "testSHA256DigestTwo", 0)
.withTPs(TypestateError.class, 1)
.withTPs(ImpreciseValueExtractionError.class, 1)
.withTPs(ImpreciseValueExtractionError.class, 2)
.build());

addErrorSpecification(
new ErrorSpecification.Builder("ipack.JPAKEExample", "deriveSessionKey", 1)
.withTPs(ImpreciseValueExtractionError.class, 1)
.withTPs(ImpreciseValueExtractionError.class, 2)
.build());

scanner.run();
Expand All @@ -239,20 +274,22 @@ public void testBCSignerExamples() {
addErrorSpecification(
new ErrorSpecification.Builder(
"gwt_crypto.ISO9796SignerTest", "doShortPartialTest", 0)
.withTPs(ImpreciseValueExtractionError.class, 1)
.withTPs(IncompleteOperationError.class, 1)
.build());
addErrorSpecification(
new ErrorSpecification.Builder(
"gwt_crypto.ISO9796SignerTest", "doFullMessageTest", 0)
.withTPs(ConstraintError.class, 1)
.withTPs(ImpreciseValueExtractionError.class, 2)
.withTPs(IncompleteOperationError.class, 1)
.build());
addErrorSpecification(
new ErrorSpecification.Builder("gwt_crypto.PSSBlindTest", "testSig", 6)
.withTPs(IncompleteOperationError.class, 1)
.withTPs(RequiredPredicateError.class, 1)
.withTPs(AlternativeReqPredicateError.class, 2)
.withTPs(ImpreciseValueExtractionError.class, 1)
.withTPs(ImpreciseValueExtractionError.class, 2)
.build());
addErrorSpecification(
new ErrorSpecification.Builder("gwt_crypto.PSSTest", "testSig", 6)
Expand All @@ -263,11 +300,13 @@ public void testBCSignerExamples() {
addErrorSpecification(
new ErrorSpecification.Builder(
"gwt_crypto.X931SignerTest", "shouldPassSignatureTestOne", 0)
.withTPs(ImpreciseValueExtractionError.class, 1)
.withTPs(IncompleteOperationError.class, 1)
.build());
addErrorSpecification(
new ErrorSpecification.Builder(
"gwt_crypto.X931SignerTest", "shouldPassSignatureTestTwo", 0)
.withTPs(ImpreciseValueExtractionError.class, 3)
.withTPs(IncompleteOperationError.class, 2)
.withTPs(RequiredPredicateError.class, 2)
.build());
Expand All @@ -286,7 +325,7 @@ public void testBCSignerExamples() {
new ErrorSpecification.Builder(
"diqube.TicketSignatureService", "isValidTicketSignature", 1)
.withTPs(AlternativeReqPredicateError.class, 1)
.withTPs(ImpreciseValueExtractionError.class, 1)
.withTPs(ImpreciseValueExtractionError.class, 2)
.build());

addErrorSpecification(
Expand All @@ -300,13 +339,15 @@ public void testBCSignerExamples() {

addErrorSpecification(
new ErrorSpecification.Builder("pattern.SignerTest", "testSignerGenerate", 0)
.withTPs(ImpreciseValueExtractionError.class, 2)
.withTPs(RequiredPredicateError.class, 2)
.withTPs(AlternativeReqPredicateError.class, 1)
.build());
addErrorSpecification(
new ErrorSpecification.Builder("pattern.SignerTest", "testSignerVerify", 0)
.withTPs(ImpreciseValueExtractionError.class, 3)
.withTPs(RequiredPredicateError.class, 2)
.withTPs(AlternativeReqPredicateError.class, 1)
.withTPs(AlternativeReqPredicateError.class, 2)
.build());

scanner.run();
Expand Down
Loading

0 comments on commit 7b69874

Please sign in to comment.