Untitled
unknown
plain_text
2 years ago
6.3 kB
9
Indexable
public class WAFowasp extends GenericFunction{ boolean autoConfigured; private String ipAddress; DatatypeExpr waf; int nRules; Map<Integer, BoolExpr> notConfiguredConditions = new HashMap<>(); Map<Integer, Expr> srcConditions = new HashMap<>(); Map<Integer, Expr> dstConditions = new HashMap<>(); /** * Public constructor for the WAF for OWASP rules * @param source It is the Allocation Node on which the WAF is put * @param ctx It is the Z3 Context in which the model is generated * @param nctx It is the NetContext object to which constraints are sent */ public WAFowasp(AllocationNode source, Context ctx, NetContext nctx) { this.source = source; this.ctx = ctx; this.nctx = nctx; waf = source.getZ3Name(); ipAddress = source.getNode().getName(); constraints = new ArrayList<BoolExpr>(); isEndHost = false; // function can be used or not, autoplace follows it used = ctx.mkBoolConst(waf+"_used"); autoplace = true; //function can be autoConfigured is z3 must establish the firewall filtering policy autoConfigured = true; } /** * This method allows to create SOFT and HARD constraints for an auto-configured Owasp WAF */ public void automaticConfiguration() { List<BoolExpr> implications1 = new ArrayList<BoolExpr>(); List<BoolExpr> implications2 = new ArrayList<BoolExpr>(); // REMINDER: minizimePlaceholderRules function is not useful in this case because: // - SOURCES are not aggregable since they are no more IP addresses but user names // - there are NO MORE default action and Isolation/Reachability requirements nRules = source.getFlows().values().size(); if(autoplace) { // waf should not be used if possible nctx.softConstrAutoPlace.add(new Tuple<BoolExpr, String>(ctx.mkNot(used), "owasp_waf_auto_conf")); }else { used = ctx.mkTrue(); constraints.add(ctx.mkEq(used, ctx.mkTrue())); } for(int i = 0; i < nRules; i++){ Expr src = ctx.mkConst(waf + "_auto_src_"+i, ctx.mkStringSort()); Expr dst = ctx.mkConst(waf + "_auto_dst_"+i, ctx.mkStringSort()); /** * This section allows the creation of the following hard constraints: * 1) if in a rule the source isn't NULL, then also the destination shouldn't be NULL * 2) if in a rule the source is NULL, then also the destination should be NULL * This is done only with autoplacement feature. * Observation: maybe we can introduce the REVERSE rules! */ if(autoplace) { implications1.add(ctx.mkAnd(ctx.mkNot(ctx.mkEq( src, ctx.mkString("null"))), ctx.mkNot(ctx.mkEq( dst, ctx.mkString("null"))))); implications2.add(ctx.mkAnd(ctx.mkEq( src, ctx.mkString("null")), ctx.mkEq( dst, ctx.mkString("null")))); } BoolExpr notConfiguredRule = ctx.mkAnd( ctx.mkEq(ctx.mkString("null"), src), ctx.mkEq(ctx.mkString("null"), dst) ); nctx.softConstrAutoConf.add(new Tuple<BoolExpr, String>(notConfiguredRule, "waf_auto_conf")); notConfiguredConditions.put(i, notConfiguredRule); } /** * This section allows the insertion of previously created hard constraints in a list. */ if(autoplace) { BoolExpr[] implications_tmp = new BoolExpr[implications1.size()]; constraints.add(ctx.mkImplies(ctx.mkOr(implications1.toArray(implications_tmp)),used)); implications_tmp = new BoolExpr[implications2.size()]; constraints.add(ctx.mkImplies(ctx.mkNot(used), ctx.mkAnd(implications2.toArray(implications_tmp)))); } /** * This sections generates all the constraints to satisfy reachability and isolation requirements. */ for(Flow sr : source.getFlows().values()) { generateSatifiabilityConstraint(sr); } } /** * This method generates the hard constraint to satisfy a requirement for an automatically configured waf owasp. * @param sr it is the security requirement */ private void generateSatifiabilityConstraint(Flow sr) { BoolExpr firstA = used; BoolExpr secondA = ctx.mkEq((BoolExpr)nctx.deny.apply(source.getZ3Name(), ctx.mkInt(sr.getIdFlow())), ctx.mkTrue()); List<BoolExpr> listSecondC = new ArrayList<>(); for(int i = 0; i < nRules; i++) { BoolExpr component1 = ctx.mkNot(notConfiguredConditions.get(i)); BoolExpr component2 = ctx.mkAnd( nctx.equalIpAddressToPFRule(sr.getCrossedTraffic(ipAddress).getIPSrc(), srcConditions.get(i)), nctx.equalIpAddressToPFRule(sr.getCrossedTraffic(ipAddress).getIPDst(), dstConditions.get(i)) ); BoolExpr secondCPart = ctx.mkAnd(component1, component2); listSecondC.add(secondCPart); } BoolExpr[] tmp = new BoolExpr[listSecondC.size()]; BoolExpr secondC = ctx.mkOr(listSecondC.toArray(tmp)); constraints.add(ctx.mkImplies(ctx.mkAnd(firstA, secondA), secondC)); constraints.add(ctx.mkImplies(ctx.mkAnd(secondC, firstA), secondA)); } /** * This method allows to know if autoconfiguration feature is used *@return the value of autoconfigured boolean variable */ public boolean isAutoconfigured() { return autoConfigured; } /** * This method allows to know if autoplacement feature is used *@return the value of autoplace boolean variable */ public boolean isAutoplace() { return autoplace; } /** * This method allows to set autoconfigured variable *@param autoconfigured Value to set */ public void setAutoconfigured(boolean autoconfigured) { this.autoConfigured = autoconfigured; } /** * This method allows to set autoplace variable *@param autoplace Value to set */ public void setAutoplace(boolean autoplace) { this.autoplace = autoplace; } /** * This method allows to wrap the method which adds the constraints inside Z3 solver * @param solver Istance of Z3 solver */ @Override public void addContraints(Optimize solver) { BoolExpr[] constr = new BoolExpr[constraints.size()]; solver.Add(constraints.toArray(constr)); //additionalConstraints(solver); } }
Editor is loading...