Skip to content

Commit

Permalink
Merge pull request #772 from CROSSINGTUD/fix/issue295
Browse files Browse the repository at this point in the history
Fix edges in state machine when dealing with optionals
  • Loading branch information
schlichtig authored Nov 29, 2024
2 parents 9ed81e1 + a284c2f commit 67ad228
Show file tree
Hide file tree
Showing 13 changed files with 112 additions and 37 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -859,9 +859,6 @@ public Collection<ISLConstraint> computeMissingPredicates() {
Collection<ISLConstraint> remainingPredicates = new HashSet<>(requiredPredicates);

for (ISLConstraint pred : requiredPredicates) {
Collection<Map.Entry<EnsuredCrySLPredicate, Integer>> predsAtStatement =
ensuredPredicates.get(pred.getLocation());

if (pred instanceof RequiredCrySLPredicate) {
RequiredCrySLPredicate reqPred = (RequiredCrySLPredicate) pred;

Expand All @@ -873,6 +870,8 @@ public Collection<ISLConstraint> computeMissingPredicates() {
}

// Check for basic required predicates, e.g. randomized
Collection<Map.Entry<EnsuredCrySLPredicate, Integer>> predsAtStatement =
ensuredPredicates.get(reqPred.getLocation());
int reqParamIndex = reqPred.getParamIndex();
for (Map.Entry<EnsuredCrySLPredicate, Integer> ensPredAtIndex : predsAtStatement) {
if (doReqPredAndEnsPredMatch(
Expand All @@ -899,6 +898,8 @@ public Collection<ISLConstraint> computeMissingPredicates() {
.filter(CrySLPredicate::isNegated)
.collect(Collectors.toList());

Collection<Map.Entry<EnsuredCrySLPredicate, Integer>> predsAtStatement =
ensuredPredicates.get(altPred.getLocation());
for (Map.Entry<EnsuredCrySLPredicate, Integer> ensPredAtIndex : predsAtStatement) {
// If any positive alternative is satisfied, the whole predicate is satisfied
if (positives.stream()
Expand Down Expand Up @@ -967,7 +968,7 @@ public Collection<RequiredCrySLPredicate> computeContradictedPredicates() {
// Check for basic negated required predicates, e.g. randomized
CrySLPredicate invertedPred = reqPred.getPred().invertNegation();
Collection<Map.Entry<EnsuredCrySLPredicate, Integer>> predsAtStatement =
ensuredPredicates.get(pred.getLocation());
ensuredPredicates.get(reqPred.getLocation());

for (Map.Entry<EnsuredCrySLPredicate, Integer> ensPredAtIndex : predsAtStatement) {
if (doReqPredAndEnsPredMatch(
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -183,6 +183,13 @@ private SubStateMachine buildSubSMG(final Order order, final Collection<StateNod
right = buildSubSMG(order.getRight(), left.getEndNodes());
start.addAll(left.getStartNodes());
end.addAll(right.getEndNodes());

for (StateNode node : startNodes) {
if (left.getEndNodes().contains(node)) {
start.addAll(right.getStartNodes());
}
}

break;
case ALTERNATIVE:
left = buildSubSMG(order.getLeft(), startNodes);
Expand Down
Original file line number Diff line number Diff line change
@@ -1,6 +1,5 @@
package crypto.rules;

import boomerang.scene.Statement;
import java.util.List;

public class CrySLConstraint implements ISLConstraint {
Expand All @@ -15,7 +14,6 @@ public enum LogOps {
private final LogOps operator;
private final ISLConstraint left;
private final ISLConstraint right;
private Statement location;

public CrySLConstraint(ISLConstraint l, ISLConstraint r, LogOps op) {
left = l;
Expand Down Expand Up @@ -63,9 +61,4 @@ public List<String> getInvolvedVarNames() {
public String getName() {
return toString();
}

@Override
public Statement getLocation() {
return location;
}
}
Original file line number Diff line number Diff line change
@@ -1,6 +1,5 @@
package crypto.rules;

import boomerang.scene.Statement;
import java.util.Collections;
import java.util.List;

Expand All @@ -16,8 +15,6 @@ public class CrySLExceptionConstraint implements ISLConstraint {
/** The Exception thrown by the Method. */
private final CrySLException exception;

private Statement location = null;

/**
* Construct the {@link CrySLExceptionConstraint} given the method and the exception thrown
* thereby.
Expand Down Expand Up @@ -52,11 +49,6 @@ public String toString() {
return String.format("%s(%s, %s)", this.getClass().getName(), getMethod(), getException());
}

@Override
public Statement getLocation() {
return this.location;
}

@Override
public List<String> getInvolvedVarNames() {
return Collections.emptyList();
Expand Down
8 changes: 0 additions & 8 deletions CryptoAnalysis/src/main/java/crypto/rules/CrySLLiteral.java
Original file line number Diff line number Diff line change
@@ -1,14 +1,6 @@
package crypto.rules;

import boomerang.scene.Statement;

public abstract class CrySLLiteral implements ISLConstraint {

private Statement location;

protected CrySLLiteral() {}

public Statement getLocation() {
return location;
}
}
3 changes: 0 additions & 3 deletions CryptoAnalysis/src/main/java/crypto/rules/ISLConstraint.java
Original file line number Diff line number Diff line change
@@ -1,11 +1,8 @@
package crypto.rules;

import boomerang.scene.Statement;
import java.util.List;

public interface ISLConstraint extends ICrySLPredicateParameter {

List<String> getInvolvedVarNames();

Statement getLocation();
}
Original file line number Diff line number Diff line change
Expand Up @@ -94,8 +94,7 @@ protected DataFlowScope createDataFlowScope() {
@Override
protected SceneTransformer createAnalysisTransformer() throws ImprecisionException {

// Required since Soot 4.3.0
Options.v().setPhaseOption("jb.sils", "enabled:false");
Options.v().setPhaseOption("jb", "use-original-names:false");

return new SceneTransformer() {

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -15,6 +15,7 @@ public class InAcceptingStateAssertion implements Assertion, StateResult {
public InAcceptingStateAssertion(Statement unit, Collection<Val> val) {
this.unit = unit;
this.val = val;
this.satisfied = false;
}

public Collection<Val> getVal() {
Expand All @@ -41,6 +42,6 @@ public boolean isImprecise() {

@Override
public String toString() {
return "[" + val + "@" + unit + " must not be in error state]";
return "[" + val + " @ " + unit + " must not be in error state]";
}
}
Original file line number Diff line number Diff line change
Expand Up @@ -15,6 +15,7 @@ public class NotInAcceptingStateAssertion implements Assertion, StateResult {
public NotInAcceptingStateAssertion(Statement unit, Collection<Val> accessGraph) {
this.unit = unit;
this.val = accessGraph;
this.satisfied = true;
}

public Collection<Val> getVal() {
Expand All @@ -26,7 +27,7 @@ public Statement getStmt() {
}

public void computedResults(State s) {
satisfied |= !s.isAccepting();
satisfied &= !s.isAccepting();
}

@Override
Expand All @@ -41,6 +42,6 @@ public boolean isImprecise() {

@Override
public String toString() {
return "[" + val + "@" + unit + " must not be in error state]";
return "[" + val + " @ " + unit + " must not be in accepting state]";
}
}
91 changes: 91 additions & 0 deletions CryptoAnalysis/src/test/java/tests/jca/CogniCryptTestGenTest.java
Original file line number Diff line number Diff line change
Expand Up @@ -88,6 +88,97 @@ public void sSLParametersInvalidTest2() {
Assertions.mustNotBeInAcceptingState(sSLParameters0);
}

@Test
@SuppressWarnings("ConstantConditions")
public void keyStoreInvalidTest7()
throws NoSuchAlgorithmException,
IOException,
KeyStoreException,
CertificateException,
UnrecoverableEntryException {

// Related to issue 295: https://github.com/CROSSINGTUD/CryptoAnalysis/issues/295
char[] passwordKey = null;
String aliasGet = null;
String alias = null;
Entry entry = null;
String keyStoreAlgorithm = null;
String aliasSet = null;
ProtectionParameter protParamSet = null;
LoadStoreParameter paramStore = null;
ProtectionParameter protParamGet = null;

KeyStore keyStore0 = KeyStore.getInstance(keyStoreAlgorithm);
// loads skipped
keyStore0.getEntry(aliasGet, protParamGet);
Key key = keyStore0.getKey(alias, passwordKey);
keyStore0.setEntry(aliasSet, entry, protParamSet);
keyStore0.store(paramStore);
Assertions.notHasEnsuredPredicate(key);
Assertions.mustNotBeInAcceptingState(keyStore0);
}

@Test
@SuppressWarnings("ConstantConditions")
public void keyStoreInvalidTest8()
throws NoSuchAlgorithmException,
IOException,
KeyStoreException,
CertificateException,
UnrecoverableEntryException {

// Related to issue 295: https://github.com/CROSSINGTUD/CryptoAnalysis/issues/295
char[] passwordKey = null;
String aliasGet = null;
String alias = null;
Entry entry = null;
String keyStoreAlgorithm = null;
String aliasSet = null;
ProtectionParameter protParamSet = null;
LoadStoreParameter paramStore = null;
ProtectionParameter protParamGet = null;

KeyStore keyStore0 = KeyStore.getInstance(keyStoreAlgorithm, (Provider) null);
// loads skipped
keyStore0.getEntry(aliasGet, protParamGet);
Key key = keyStore0.getKey(alias, passwordKey);
keyStore0.setEntry(aliasSet, entry, protParamSet);
keyStore0.store(paramStore);
Assertions.notHasEnsuredPredicate(key);
Assertions.mustNotBeInAcceptingState(keyStore0);
}

@Test
@SuppressWarnings("ConstantConditions")
public void keyStoreInvalidTest9()
throws NoSuchAlgorithmException,
IOException,
KeyStoreException,
CertificateException,
UnrecoverableEntryException {

// Related to issue 295: https://github.com/CROSSINGTUD/CryptoAnalysis/issues/295
char[] passwordKey = null;
String aliasGet = null;
String alias = null;
Entry entry = null;
String keyStoreAlgorithm = null;
String aliasSet = null;
ProtectionParameter protParamSet = null;
OutputStream fileoutput = null;
char[] passwordOut = null;
ProtectionParameter protParamGet = null;

KeyStore keyStore0 = KeyStore.getInstance(keyStoreAlgorithm);
// loads skipped
keyStore0.getEntry(aliasGet, protParamGet);
Key key = keyStore0.getKey(alias, passwordKey);
keyStore0.setEntry(aliasSet, entry, protParamSet);
keyStore0.store(fileoutput, passwordOut);
Assertions.notHasEnsuredPredicate(key);
Assertions.mustNotBeInAcceptingState(keyStore0);
}

@Test
@SuppressWarnings("ConstantConditions")
public void keyStoreInvalidTest10()
Expand Down
2 changes: 2 additions & 0 deletions CryptoAnalysis/src/test/java/tests/jca/PBETest.java
Original file line number Diff line number Diff line change
Expand Up @@ -66,13 +66,15 @@ public void pbeUsagePatternMinPBEIterations() throws GeneralSecurityException {
Assertions.hasGeneratedPredicate(pbekeyspec);
Assertions.mustNotBeInAcceptingState(pbekeyspec);
pbekeyspec.clearPassword();
Assertions.mustBeInAcceptingState(pbekeyspec);
pbekeyspec = new PBEKeySpec(corPwd, salt, 9999, 128);
Assertions.extValue(1);
Assertions.extValue(2);
Assertions.extValue(3);
Assertions.hasNotGeneratedPredicate(pbekeyspec);
Assertions.mustNotBeInAcceptingState(pbekeyspec);
pbekeyspec.clearPassword();
Assertions.mustBeInAcceptingState(pbekeyspec);

PBEParameterSpec pbeParSpec1 = new PBEParameterSpec(salt, 10000);
Assertions.extValue(0);
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -213,7 +213,7 @@ public void testBCDigestExamples() {
addErrorSpecification(
new ErrorSpecification.Builder(
"pluotsorbet.BouncyCastleSHA256", "testSHA256DigestTwo", 0)
.withTPs(TypestateError.class, 4)
.withTPs(TypestateError.class, 1)
.withTPs(ImpreciseValueExtractionError.class, 1)
.build());

Expand Down
1 change: 0 additions & 1 deletion pom.xml
Original file line number Diff line number Diff line change
Expand Up @@ -420,7 +420,6 @@
<include>CryptoAnalysis/pom.xml</include>
<include>HeadlessAndroidScanner/pom.xml</include>
<include>HeadlessJavaScanner/pom.xml</include>
<include>ScannerTests/pom.xml</include>
</includes>
<sortPom>
<encoding>UTF-8</encoding>
Expand Down

0 comments on commit 67ad228

Please sign in to comment.