Untitled

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);
	}
}