Skip to content

Commit

Permalink
Update detection of PredicateContradiction errors
Browse files Browse the repository at this point in the history
  • Loading branch information
@smeyer198
smeyer198 committed Jul 24, 2024
1 parent 8034804 commit e327d16
Show file tree
Hide file tree
Showing 14 changed files with 308 additions and 150 deletions.
81 changes: 48 additions & 33 deletions CryptoAnalysis-Core/src/main/java/crypto/analysis/AnalysisSeedWithSpecification.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -95,9 +95,6 @@ public void execute() {
evaluateTypestateOrder();
evaluateIncompleteOperations();

// Check the REQUIRES section and ensure predicates in ENSURES section
checkConstraintsAndEnsurePredicates();

scanner.getAnalysisReporter().onSeedFinished(this);
}

Expand Down Expand Up @@ -316,7 +313,7 @@ public void addEnsuredPredicate(EnsuredCrySLPredicate ensPred, Statement stateme
}
}

private void checkConstraintsAndEnsurePredicates() {
public void checkConstraintsAndEnsurePredicates() {
boolean satisfiesConstraintSystem = isConstraintSystemSatisfied();

for (CrySLPredicate predToBeEnsured : specification.getPredicates()) {
Expand All @@ -340,7 +337,7 @@ private void checkConstraintsAndEnsurePredicates() {
if (!satisfiesConstraintSystem && predToBeEnsured.getConstraint().isEmpty()) {
// predicate has no condition, but the constraint system is not satisfied
ensPred = new HiddenPredicate(predToBeEnsured, constraintSolver.getCollectedValues(), this, HiddenPredicate.HiddenPredicateType.ConstraintsAreNotSatisfied);
} else if (predToBeEnsured.getConstraint().isPresent() && !isPredConditionSatisfied(predToBeEnsured)) {
} else if (predToBeEnsured.getConstraint().isPresent() && isPredConditionViolated(predToBeEnsured)) {
// predicate has condition, but condition is not satisfied
ensPred = new HiddenPredicate(predToBeEnsured, constraintSolver.getCollectedValues(), this, HiddenPredicate.HiddenPredicateType.ConditionIsNotSatisfied);
} else {
Expand Down Expand Up @@ -379,7 +376,7 @@ private void ensurePredicate(EnsuredCrySLPredicate ensuredPred, Statement statem
// TODO only for first parameter?
for (ICrySLPredicateParameter predicateParam : ensuredPred.getPredicate().getParameters()) {
if (predicateParam.getName().equals("this")) {
expectPredicateWhenThisObjectIsInState(ensuredPred, stateNode, statement);
expectPredicateWhenThisObjectIsInState(ensuredPred, stateNode);
}
}

Expand Down Expand Up @@ -431,11 +428,8 @@ private boolean predicateParameterEquals(List<ICrySLPredicateParameter> paramete
*
* @param ensuredPred the predicate to ensure on this seed
* @param stateNode the state, where the predicate is expected to be ensured
* @param statement the statement that leads to the state
*/
private void expectPredicateWhenThisObjectIsInState(EnsuredCrySLPredicate ensuredPred, State stateNode, Statement statement) {
predicateHandler.expectPredicate(this, statement, ensuredPred.getPredicate());

private void expectPredicateWhenThisObjectIsInState(EnsuredCrySLPredicate ensuredPred, State stateNode) {
for (Table.Cell<ControlFlowGraph.Edge, Val, TransitionFunction> e : analysisResults.asStatementValWeightTable().cellSet()) {
if (containsTargetState(e.getValue(), stateNode)) {
predicateHandler.addNewPred(this, e.getRowKey().getStart(), e.getColumnKey(), ensuredPred);
Expand Down Expand Up @@ -474,7 +468,6 @@ private void expectPredicateOnOtherObject(EnsuredCrySLPredicate ensPred, Stateme
AnalysisSeedWithEnsuredPredicate seedWithoutSpec = (AnalysisSeedWithEnsuredPredicate) otherSeed;

seedWithoutSpec.addEnsuredPredicate(ensPred);
predicateHandler.expectPredicate(seedWithoutSpec, statement, ensPred.getPredicate());
}
}
}
Expand Down Expand Up @@ -642,7 +635,7 @@ private void checkInternalConstraints() {
*/
private boolean isConstraintSystemSatisfied() {
if (internalConstraintsSatisfied) {
return computeMissingPredicates().isEmpty();
return computeMissingPredicates().isEmpty() && computeContradictedPredicates().isEmpty();
}
return false;
}
Expand All @@ -662,29 +655,19 @@ public Collection<ISLConstraint> computeMissingPredicates() {

if (pred instanceof RequiredCrySLPredicate) {
RequiredCrySLPredicate reqPred = (RequiredCrySLPredicate) pred;
int reqParamIndex = reqPred.getParamIndex();

// If a negated predicate is ensured, a PredicateContradictionError has to be reported
if (reqPred.getPred().isNegated()) {
// Check for negated predicates, e.g. !randomized
boolean violated = false;

// Negated predicates are violated if the corresponding predicate is ensured
for (Map.Entry<EnsuredCrySLPredicate, Integer> ensPredAtIndex : predsAtStatement) {
if (doReqPredAndEnsPredMatch(reqPred.getPred(), reqParamIndex, ensPredAtIndex)) {
violated = true;
}
}
remainingPredicates.remove(pred);
continue;
}

if (!violated) {
// Check for basic required predicates, e.g. randomized
int reqParamIndex = reqPred.getParamIndex();
for (Map.Entry<EnsuredCrySLPredicate, Integer> ensPredAtIndex : predsAtStatement) {
if (doReqPredAndEnsPredMatch(reqPred.getPred(), reqParamIndex, ensPredAtIndex)) {
remainingPredicates.remove(pred);
}
} else {
// Check for basic required predicates, e.g. randomized
for (Map.Entry<EnsuredCrySLPredicate, Integer> ensPredAtIndex : predsAtStatement) {
if (doReqPredAndEnsPredMatch(reqPred.getPred(), reqParamIndex, ensPredAtIndex)) {
remainingPredicates.remove(pred);
}
}
}
} else if (pred instanceof AlternativeReqPredicate) {
AlternativeReqPredicate altPred = (AlternativeReqPredicate) pred;
Expand Down Expand Up @@ -718,13 +701,13 @@ public Collection<ISLConstraint> computeMissingPredicates() {
if (rem instanceof RequiredCrySLPredicate) {
RequiredCrySLPredicate singlePred = (RequiredCrySLPredicate) rem;

if (isPredConditionSatisfied(singlePred.getPred())) {
if (isPredConditionViolated(singlePred.getPred())) {
remainingPredicates.remove(singlePred);
}
} else if (rem instanceof AlternativeReqPredicate) {
Collection<CrySLPredicate> altPred = ((AlternativeReqPredicate) rem).getAlternatives();

if (altPred.parallelStream().anyMatch(this::isPredConditionSatisfied)) {
if (altPred.parallelStream().anyMatch(this::isPredConditionViolated)) {
remainingPredicates.remove(rem);
}
}
Expand All @@ -733,6 +716,38 @@ public Collection<ISLConstraint> computeMissingPredicates() {
return remainingPredicates;
}

public Collection<RequiredCrySLPredicate> computeContradictedPredicates() {
Collection<ISLConstraint> requiredPredicates = constraintSolver.getRequiredPredicates();
Collection<RequiredCrySLPredicate> contradictedPredicates = new HashSet<>();

for (ISLConstraint pred : requiredPredicates) {
if (pred instanceof RequiredCrySLPredicate) {
RequiredCrySLPredicate reqPred = (RequiredCrySLPredicate) pred;

// Only negated predicates can be contradicted
if (!reqPred.getPred().isNegated()) {
continue;
}

if (isPredConditionViolated(reqPred.getPred())) {
continue;
}

// Check for basic negated required predicates, e.g. randomized
CrySLPredicate invertedPred = reqPred.getPred().invertNegation();
Set<Map.Entry<EnsuredCrySLPredicate, Integer>> predsAtStatement = ensuredPredicates.getOrDefault(pred.getLocation(), new HashSet<>());

for (Map.Entry<EnsuredCrySLPredicate, Integer> ensPredAtIndex : predsAtStatement) {
if (doReqPredAndEnsPredMatch(invertedPred, reqPred.getParamIndex(), ensPredAtIndex)) {
contradictedPredicates.add(reqPred);
}
}
}
}

return contradictedPredicates;
}

private boolean doReqPredAndEnsPredMatch(CrySLPredicate reqPred, int reqPredIndex, Map.Entry<EnsuredCrySLPredicate, Integer> ensPred) {
return reqPred.equals(ensPred.getKey().getPredicate()) && doPredsMatch(reqPred, ensPred.getKey()) && reqPredIndex == ensPred.getValue();
}
Expand All @@ -743,7 +758,7 @@ private boolean doReqPredAndEnsPredMatch(CrySLPredicate reqPred, int reqPredInde
* @param pred the predicate to be checked
* @return true if the condition is satisfied
*/
private boolean isPredConditionSatisfied(CrySLPredicate pred) {
private boolean isPredConditionViolated(CrySLPredicate pred) {
return pred.getConstraint().map(conditional -> {
EvaluableConstraint evalCons = EvaluableConstraint.getInstance(conditional, constraintSolver);
evalCons.evaluate();
Expand Down
70 changes: 20 additions & 50 deletions CryptoAnalysis-Core/src/main/java/crypto/analysis/PredicateHandler.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -6,11 +6,9 @@
import boomerang.scene.Statement;
import boomerang.scene.Val;
import com.google.common.collect.HashBasedTable;
import com.google.common.collect.Sets;
import com.google.common.collect.Table;
import crypto.analysis.errors.PredicateContradictionError;
import crypto.analysis.errors.RequiredPredicateError;
import crypto.rules.CrySLPredicate;
import crypto.rules.CrySLRule;
import crypto.rules.ISLConstraint;
import typestate.TransitionFunction;

Expand Down Expand Up @@ -101,37 +99,28 @@ private PredicateHandler getOuterType() {

}

private final Table<Statement, Val, Set<EnsuredCrySLPredicate>> existingPredicates = HashBasedTable.create();
private final Table<Statement, IAnalysisSeed, Set<EnsuredCrySLPredicate>> existingPredicatesObjectBased = HashBasedTable.create();
private final Table<Statement, IAnalysisSeed, Set<CrySLPredicate>> expectedPredicateObjectBased = HashBasedTable.create();
private final CryptoScanner cryptoScanner;
private final Table<Statement, Val, Set<EnsuredCrySLPredicate>> existingPredicates = HashBasedTable.create();
private final Map<AnalysisSeedWithSpecification, List<RequiredPredicateError>> requiredPredicateErrors;

public PredicateHandler(CryptoScanner cryptoScanner) {
this.cryptoScanner = cryptoScanner;
this.requiredPredicateErrors = new HashMap<>();
}

public boolean addNewPred(IAnalysisSeed seedObj, Statement statement, Val variable, EnsuredCrySLPredicate ensPred) {
public void addNewPred(IAnalysisSeed seedObj, Statement statement, Val variable, EnsuredCrySLPredicate ensPred) {
Set<EnsuredCrySLPredicate> set = getExistingPredicates(statement, variable);
boolean added = set.add(ensPred);

if (added) {
onPredicateAdded(seedObj, statement, variable, ensPred);
}

Set<EnsuredCrySLPredicate> predsObjBased = existingPredicatesObjectBased.get(statement, seedObj);
if (predsObjBased == null)
predsObjBased = Sets.newHashSet();
predsObjBased.add(ensPred);
existingPredicatesObjectBased.put(statement, seedObj, predsObjBased);
return added;
}

public Set<EnsuredCrySLPredicate> getExistingPredicates(Statement stmt, Val seed) {
Set<EnsuredCrySLPredicate> set = existingPredicates.get(stmt, seed);
if (set == null) {
set = Sets.newHashSet();
set = new HashSet<>();
existingPredicates.put(stmt, seed, set);
}
return set;
Expand Down Expand Up @@ -183,23 +172,20 @@ private void onPredicateAdded(IAnalysisSeed seedObj, Statement statement, Val fa
}
}

public void expectPredicate(IAnalysisSeed object, Statement stmt, CrySLPredicate predToBeEnsured) {
for (Statement successor : stmt.getMethod().getControlFlowGraph().getSuccsOf(stmt)) {
Set<CrySLPredicate> set = expectedPredicateObjectBased.get(successor, object);
if (set == null)
set = Sets.newHashSet();
set.add(predToBeEnsured);
expectedPredicateObjectBased.put(stmt, object, set);
}
}

public void checkPredicates() {
runPredicateMechanism();
collectMissingRequiredPredicates();
collectContradictingPredicates();
reportRequiredPredicateErrors();
checkForContradictions();
cryptoScanner.getAnalysisReporter().ensuredPredicates(existingPredicates);
}

private void runPredicateMechanism() {
for (AnalysisSeedWithSpecification seed : cryptoScanner.getAnalysisSeedsWithSpec()) {
seed.checkConstraintsAndEnsurePredicates();
}
}

private void collectMissingRequiredPredicates() {
for (AnalysisSeedWithSpecification seed : cryptoScanner.getAnalysisSeedsWithSpec()) {
requiredPredicateErrors.put(seed, new ArrayList<>());
Expand Down Expand Up @@ -238,30 +224,14 @@ private void reportRequiredPredicateErrors() {
}
}

private void checkForContradictions() {
Set<Map.Entry<CrySLPredicate, CrySLPredicate>> contradictionPairs = new HashSet<>();
for (CrySLRule rule : cryptoScanner.getRuleset()) {
if(!rule.getPredicates().isEmpty()) {
for (ISLConstraint cons : rule.getConstraints()) {
if (cons instanceof CrySLPredicate && ((CrySLPredicate) cons).isNegated()) {
// TODO This is weird; why is it always get(0)?
// contradictionPairs.add(new SimpleEntry<CrySLPredicate, CrySLPredicate>(rule.getPredicates().get(0), ((CrySLPredicate) cons).setNegated(false)));
}
}
}
}
for (Statement generatingPredicateStmt : expectedPredicateObjectBased.rowKeySet()) {
for (Map.Entry<Val, Set<EnsuredCrySLPredicate>> exPredCell : existingPredicates.row(generatingPredicateStmt).entrySet()) {
Set<String> preds = new HashSet<>();
for (EnsuredCrySLPredicate exPred : exPredCell.getValue()) {
preds.add(exPred.getPredicate().getPredName());
}
for (Map.Entry<CrySLPredicate, CrySLPredicate> disPair : contradictionPairs) {
if (preds.contains(disPair.getKey().getPredName()) && preds.contains(disPair.getValue().getPredName())) {
// TODO Rule should not be null
//cryptoScanner.getAnalysisListener().reportError(null, new PredicateContradictionError(generatingPredicateStmt, null, disPair));
}
}
private void collectContradictingPredicates() {
for (AnalysisSeedWithSpecification seed : cryptoScanner.getAnalysisSeedsWithSpec()) {
Collection<RequiredCrySLPredicate> contradictedPredicates = seed.computeContradictedPredicates();

for (RequiredCrySLPredicate pred : contradictedPredicates) {
PredicateContradictionError error = new PredicateContradictionError(seed, pred.getLocation(), seed.getSpecification(), pred.getPred());
seed.addError(error);
cryptoScanner.getAnalysisReporter().reportError(seed, error);
}
}
}
Expand Down
24 changes: 10 additions & 14 deletions CryptoAnalysis-Core/src/main/java/crypto/analysis/errors/PredicateContradictionError.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -6,35 +6,31 @@
import crypto.rules.CrySLRule;

import java.util.Arrays;
import java.util.Map.Entry;

public class PredicateContradictionError extends AbstractError {

private final Entry<CrySLPredicate, CrySLPredicate> mismatchedPreds;
private final CrySLPredicate contradictedPredicate;

public PredicateContradictionError(IAnalysisSeed seed, Statement errorStmt, CrySLRule rule, Entry<CrySLPredicate, CrySLPredicate> disPair) {
public PredicateContradictionError(IAnalysisSeed seed, Statement errorStmt, CrySLRule rule, CrySLPredicate contradictedPredicate) {
super(seed, errorStmt, rule);

this.mismatchedPreds = disPair;
this.contradictedPredicate = contradictedPredicate;
}

public Entry<CrySLPredicate, CrySLPredicate> getMismatchedPreds() {
return mismatchedPreds;
public CrySLPredicate getContradictedPredicate() {
return contradictedPredicate;
}

@Override
public String toErrorMarkerString() {
return "There is a predicate mismatch on the predicates " +
mismatchedPreds.getKey() +
" and " +
mismatchedPreds.getValue();
return "Predicate " + contradictedPredicate + " is ensured although it should not";
}

@Override
public int hashCode() {
return Arrays.hashCode(new Object[]{
super.hashCode(),
mismatchedPreds
contradictedPredicate
});
}

Expand All @@ -45,9 +41,9 @@ public boolean equals(Object obj) {
if (getClass() != obj.getClass()) return false;

PredicateContradictionError other = (PredicateContradictionError) obj;
if (mismatchedPreds == null) {
if (other.getMismatchedPreds() != null) return false;
} else if (!mismatchedPreds.equals(other.getMismatchedPreds())) {
if (contradictedPredicate == null) {
if (other.getContradictedPredicate() != null) return false;
} else if (!contradictedPredicate.equals(other.getContradictedPredicate())) {
return false;
}

Expand Down
Loading

0 comments on commit e327d16

Please sign in to comment.