Skip to content

Commit

Permalink
Add implementation for the length predicate
Browse files Browse the repository at this point in the history
  • Loading branch information
@smeyer198
smeyer198 committed Jan 29, 2025
1 parent 3367660 commit d8de4c1
Show file tree
Hide file tree
Showing 6 changed files with 239 additions and 24 deletions.
90 changes: 85 additions & 5 deletions CryptoAnalysis/src/main/java/crypto/constraints/ComparisonConstraint.java
View file
Original file line number Diff line number Diff line change
@@ -1,6 +1,7 @@
package crypto.constraints;

import boomerang.scene.Statement;
import boomerang.scene.Val;
import com.google.common.collect.Multimap;
import crypto.analysis.AnalysisSeedWithSpecification;
import crypto.analysis.errors.ConstraintError;
Expand All @@ -13,6 +14,7 @@
import crysl.rule.CrySLComparisonConstraint;
import crysl.rule.CrySLObject;
import crysl.rule.CrySLPredicate;
import crysl.rule.ICrySLPredicateParameter;
import crysl.rule.ISLConstraint;
import java.util.Collection;
import java.util.Collections;
Expand Down Expand Up @@ -64,11 +66,19 @@ public EvaluationResult evaluate() {
impreciseResults.addAll(leftResult.impreciseResults());
impreciseResults.addAll(rightResult.impreciseResults());

if (!(leftResult.evaluatedValues().isEmpty() || rightResult.evaluatedValues().isEmpty())
|| !impreciseResults.isEmpty()) {
isRelevant = true;
// Check if left side is relevant
if (leftResult.evaluatedValues().isEmpty() && leftResult.impreciseResults().isEmpty()) {
continue;
}

// Check if right side is relevant
if (rightResult.evaluatedValues().isEmpty()
&& rightResult.impreciseResults().isEmpty()) {
continue;
}

isRelevant = true;

if (impreciseResults.isEmpty()) {
evaluateConstraint(statement, leftResult, rightResult);
} else {
Expand Down Expand Up @@ -373,12 +383,82 @@ public ArithmeticLength(

@Override
public IntermediateResult evaluate(Statement statement) {
return new IntermediateResult(Collections.emptySet(), Collections.emptySet());
if (!predicate.getPredName().equals("length")) {
return new IntermediateResult(Collections.emptySet(), Collections.emptySet());
}

if (predicate.getParameters().size() != 1) {
return new IntermediateResult(Collections.emptySet(), Collections.emptySet());
}

String paramName = predicate.getParameters().get(0).getName();
Collection<ParameterWithExtractedValues> params = statementToValues.get(statement);
Collection<ParameterWithExtractedValues> values = filterParameters(params, paramName);

Collection<Integer> preciseValues = new HashSet<>();
Collection<ImpreciseResult> impreciseResults = new HashSet<>();

for (ParameterWithExtractedValues parameter : values) {
for (ExtractedValue extractedValue : parameter.extractedValues()) {
Val val = extractedValue.val();

if (val.isArrayAllocationVal()) {
Val arrLength = val.getArrayAllocationSize();

// TODO Add transformation for complex array sizes, e.g.
// int size = 10;
// byte[] arr = new byte[size];
if (arrLength.isIntConstant()) {
preciseValues.add(arrLength.getIntValue());
} else {
ImpreciseResult impreciseResult =
new ImpreciseResult.ImpreciseExtractedValue(
parameter, extractedValue);
impreciseResults.add(impreciseResult);
}
} else if (val.isStringConstant()) {
String value = val.getStringValue();
preciseValues.add(value.length());
} else if (val.isIntConstant()) {
int value = val.getIntValue();
preciseValues.add(String.valueOf(value).length());
} else {
ImpreciseResult impreciseResult =
new ImpreciseResult.ImpreciseExtractedValue(
parameter, extractedValue);
impreciseResults.add(impreciseResult);
}
}
}

return new IntermediateResult(preciseValues, impreciseResults);
}

private Collection<ParameterWithExtractedValues> filterParameters(
Collection<ParameterWithExtractedValues> parameters, String varName) {
Collection<ParameterWithExtractedValues> result = new HashSet<>();

for (ParameterWithExtractedValues parameter : parameters) {
if (parameter.varName().equals(varName)) {
result.add(parameter);
}
}

return result;
}

@Override
public String toString() {
return predicate.toString();
if (predicate.getPredName().equals("length")) {
Collection<String> params =
predicate.getParameters().stream()
.map(ICrySLPredicateParameter::getName)
.toList();

return "length[" + String.join(", ", params) + "]";
} else {
return predicate.toString();
}
}
}

Expand Down
12 changes: 12 additions & 0 deletions CryptoAnalysis/src/test/java/tests/error/lengthpred/Length.java
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,12 @@
package tests.error.lengthpred;

public class Length {

public Length() {}

public void lengthArray(@SuppressWarnings("unused") byte[] arr) {}

public void lengthString(@SuppressWarnings("unused") String s) {}

public void lengthInteger(@SuppressWarnings("unused") int i) {}
}
99 changes: 99 additions & 0 deletions CryptoAnalysis/src/test/java/tests/error/lengthpred/LengthTest.java
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,99 @@
package tests.error.lengthpred;

import java.util.UUID;
import org.apache.commons.lang3.RandomUtils;
import org.junit.Test;
import test.TestConstants;
import test.UsagePatternTestingFramework;
import test.assertions.Assertions;

public class LengthTest extends UsagePatternTestingFramework {

@Override
protected String getRulesetPath() {
return TestConstants.RULES_TEST_DIR + "predefinedPredicates";
}

@Test
public void positiveArrayLengthTest() {
Length length = new Length();

// length[arr] == 7
byte[] arr = new byte[] {'a', 'b', 'c', 'd', 'e', 'f', 'g'};
length.lengthArray(arr);

Assertions.constraintErrors(length, 0);
}

@Test
public void negativeArrayLengthTest() {
Length length = new Length();

// length[arr] == 7
byte[] arr = new byte[] {'a', 'b'};
length.lengthArray(arr);

Assertions.constraintErrors(length, 1);
}

@Test
public void positiveStringLengthTest() {
Length length = new Length();

// length[s] == 5
String s = "12345";
length.lengthString(s);

Assertions.constraintErrors(length, 0);
}

@Test
public void negativeStringLengthTest() {
Length length = new Length();

// length[s] == 5
String s = "1234567";
length.lengthString(s);

Assertions.constraintErrors(length, 1);
}

@Test
public void positiveIntegerLengthTest() {
Length length = new Length();

// length[i] == 2
int i = 12;
length.lengthInteger(i);

Assertions.constraintErrors(length, 0);
}

@Test
public void negativeIntegerLengthTest() {
Length length = new Length();

// length[i] == 2
int i = 123;
length.lengthInteger(i);

Assertions.constraintErrors(length, 1);
}

@Test
public void unknownLengthTest() {
byte[] arr = RandomUtils.secure().randomBytes(7);
Length arrLength = new Length();
arrLength.lengthArray(arr);

String s = UUID.randomUUID().toString();
Length stringLength = new Length();
stringLength.lengthString(s);

int i = (int) (Math.random() * 99) + 10;
Length integerLength = new Length();
integerLength.lengthInteger(i);

Assertions.impreciseValueExtractionErrors(3);
}
}
12 changes: 0 additions & 12 deletions CryptoAnalysis/src/test/java/tests/jca/SignatureTest.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -76,18 +76,6 @@ public void positiveSignUsagePatternTest1() throws GeneralSecurityException {
Assertions.hasEnsuredPredicate(signature);
}

@Test
public void test() throws GeneralSecurityException {
KeyPairGenerator keyGen = KeyPairGenerator.getInstance("DSA");
Assertions.extValue(0);
keyGen.initialize(3072);
KeyPair kp = keyGen.generateKeyPair();
Assertions.hasEnsuredPredicate(kp);

final PrivateKey privateKey = kp.getPrivate();
Assertions.hasEnsuredPredicate(privateKey);
}

@Test
public void negativeSignUsagePatternTest1() throws GeneralSecurityException {
String input = "TestTestTest";
Expand Down
22 changes: 22 additions & 0 deletions CryptoAnalysis/src/test/resources/testrules/predefinedPredicates/Length.crysl
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,22 @@
SPEC tests.error.lengthpred.Length

OBJECTS
byte[] arr;
java.lang.String s;
int i;

EVENTS
Con: Length();
Arr: lengthArray(arr);
Str: lengthString(s);
Int: lengthInteger(i);

Len := Arr | Str | Int;

ORDER
Con, Len*

CONSTRAINTS
length[arr] == 7; // corresponds to arr.length
length[s] == 5; // corresponds to s.length()
length[i] == 2; // corresponds to String.valueOf(i).length()
28 changes: 21 additions & 7 deletions HeadlessJavaScanner/src/test/java/scanner/targets/BouncyCastleHeadlessTest.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -52,7 +52,7 @@ public void testBCMacExamples() {

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

addErrorSpecification(
Expand Down Expand Up @@ -209,14 +209,27 @@ public void testBCDigestExamples() {
MavenProject mavenProject = createAndCompile(mavenProjectPath);
HeadlessJavaScanner scanner = createScanner(mavenProject, BOUNCY_CASTLE_RULESET_PATH);

addErrorSpecification(
new ErrorSpecification.Builder("pattern.DigestTest", "digestWithReset", 0)
.withTPs(ImpreciseValueExtractionError.class, 2)
.build());
addErrorSpecification(
new ErrorSpecification.Builder("pattern.DigestTest", "digestWithoutUpdate", 0)
.withTPs(TypestateError.class, 1)
.withTPs(ImpreciseValueExtractionError.class, 1)
.build());
addErrorSpecification(
new ErrorSpecification.Builder("pattern.DigestTest", "digestWithMultipleUpdates", 0)
.withTPs(TypestateError.class, 1)
.withTPs(ImpreciseValueExtractionError.class, 2)
.withTPs(ImpreciseValueExtractionError.class, 3)
.build());
addErrorSpecification(
new ErrorSpecification.Builder("pattern.DigestTest", "multipleDigests", 0)
.withTPs(ImpreciseValueExtractionError.class, 1)
.build());
addErrorSpecification(
new ErrorSpecification.Builder("pattern.DigestTest", "digestDefaultUsage", 0)
.withTPs(ImpreciseValueExtractionError.class, 1)
.build());

addErrorSpecification(
Expand All @@ -234,7 +247,7 @@ public void testBCDigestExamples() {
addErrorSpecification(
new ErrorSpecification.Builder(
"inflatable_donkey.KeyBlobCurve25519Unwrap", "curve25519Unwrap", 4)
.withTPs(ImpreciseValueExtractionError.class, 4)
.withTPs(ImpreciseValueExtractionError.class, 5)
.build());

addErrorSpecification(
Expand All @@ -247,17 +260,18 @@ public void testBCDigestExamples() {
new ErrorSpecification.Builder(
"pluotsorbet.BouncyCastleSHA256", "TestSHA256DigestOne", 0)
.withTPs(TypestateError.class, 2)
.withTPs(ImpreciseValueExtractionError.class, 1)
.build());
addErrorSpecification(
new ErrorSpecification.Builder(
"pluotsorbet.BouncyCastleSHA256", "testSHA256DigestTwo", 0)
.withTPs(TypestateError.class, 1)
.withTPs(ImpreciseValueExtractionError.class, 2)
.withTPs(ImpreciseValueExtractionError.class, 4)
.build());

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

scanner.run();
Expand Down

0 comments on commit d8de4c1

Please sign in to comment.