From a42de79292d9541db7865b54e93be2d0b6e6a094 Mon Sep 17 00:00:00 2001 From: "serena.spinoso" Date: Thu, 7 Sep 2017 10:22:39 +0200 Subject: update verigraph JIRA: PARSER-154 code optimizations about graph manipulation and formula generation. Change-Id: Idebef19b128281aa2bc40d1aeab6e208c7ddd93d Signed-off-by: serena.spinoso --- .../polito/verigraph/solver/GeneratorSolver.java | 441 +++++++++++++++++++++ 1 file changed, 441 insertions(+) create mode 100644 verigraph/src/it/polito/verigraph/solver/GeneratorSolver.java (limited to 'verigraph/src/it/polito/verigraph/solver/GeneratorSolver.java') diff --git a/verigraph/src/it/polito/verigraph/solver/GeneratorSolver.java b/verigraph/src/it/polito/verigraph/solver/GeneratorSolver.java new file mode 100644 index 0000000..61e8210 --- /dev/null +++ b/verigraph/src/it/polito/verigraph/solver/GeneratorSolver.java @@ -0,0 +1,441 @@ +/******************************************************************************* + * Copyright (c) 2017 Politecnico di Torino and others. + * + * All rights reserved. This program and the accompanying materials + * are made available under the terms of the Apache License, Version 2.0 + * which accompanies this distribution, and is available at + * http://www.apache.org/licenses/LICENSE-2.0 + *******************************************************************************/ +package it.polito.verigraph.solver; + +import java.io.IOException; +import java.util.ArrayList; +import java.util.HashMap; +import java.util.List; +import java.util.Map; +import java.util.Map.Entry; +import java.util.logging.Logger; + +import com.microsoft.z3.BoolExpr; +import com.microsoft.z3.Context; +import com.microsoft.z3.DatatypeExpr; +import com.microsoft.z3.Expr; +import com.microsoft.z3.FuncDecl; +import com.microsoft.z3.IntExpr; +import com.microsoft.z3.Solver; +import com.microsoft.z3.Sort; +import com.microsoft.z3.Status; +import com.microsoft.z3.Z3Exception; + +import it.polito.neo4j.manager.Neo4jLibrary; +import it.polito.verigraph.exception.DataNotFoundException; +import it.polito.verigraph.mcnet.components.Checker; +import it.polito.verigraph.mcnet.components.IsolationResult; +import it.polito.verigraph.mcnet.components.NetContext; +import it.polito.verigraph.mcnet.components.Network; +import it.polito.verigraph.mcnet.components.NetworkObject; +import it.polito.verigraph.mcnet.components.Tuple; +import it.polito.verigraph.mcnet.netobjs.AclFirewall; +import it.polito.verigraph.mcnet.netobjs.EndHost; +import it.polito.verigraph.mcnet.netobjs.PacketModel; +import it.polito.verigraph.mcnet.netobjs.PolitoAntispam; +import it.polito.verigraph.mcnet.netobjs.PolitoCache; +import it.polito.verigraph.mcnet.netobjs.PolitoEndHost; +import it.polito.verigraph.mcnet.netobjs.PolitoFieldModifier; +import it.polito.verigraph.mcnet.netobjs.PolitoIDS; +import it.polito.verigraph.mcnet.netobjs.PolitoMailClient; +import it.polito.verigraph.mcnet.netobjs.PolitoMailServer; +import it.polito.verigraph.mcnet.netobjs.PolitoNat; +import it.polito.verigraph.mcnet.netobjs.PolitoVpnAccess; +import it.polito.verigraph.mcnet.netobjs.PolitoVpnExit; +import it.polito.verigraph.mcnet.netobjs.PolitoWebClient; +import it.polito.verigraph.mcnet.netobjs.PolitoWebServer; +import it.polito.verigraph.service.VerigraphLogger; + +public class GeneratorSolver{ + Scenario scenario; + Context ctx; + Network net; + NetContext nctx; + List constraints = new ArrayList(); + public Checker check; + Map mo=new HashMap(); + List path=new ArrayList(); + //private final static Logger LOGGER = Logger.getLogger(VerigraphLogger.class.getName()); + public static VerigraphLogger vlogger = VerigraphLogger.getVerigraphlogger(); + + public List getPaths(){ + if(path!=null) + return path; + else + return null; + } + + public GeneratorSolver(Scenario tmp, List s){ + this.scenario=tmp; + this.path=s; + } + + public void resetZ3() throws Z3Exception{ + HashMap cfg = new HashMap(); + cfg.put("model", "true"); + ctx = new Context(cfg); + } + + public String run(String src, String dst){ + IsolationResult result; + result=check.checkIsolationProperty((NetworkObject)mo.get(src), (NetworkObject)mo.get(dst)); + String res=new String(); + + if (result.result == Status.UNSATISFIABLE){ + res="UNSAT"; // Nodes a and b are isolated + }else if(result.result == Status.SATISFIABLE){ + res= "SAT"; + }else if(result.result == Status.UNKNOWN){ + res= "UNKNOWN"; + } + return res; + } + + public void genSolver() { + resetZ3(); + /*List names=new ArrayList(); + List addresses=new ArrayList(); + for(Map.Entry> a : scenario.chn.entrySet()){ + String name=a.getKey(); + Map nodo=a.getValue(); + String address=nodo.get("address"); + names.add(name); + addresses.add(address); + }*/ + + //String name_nctx=listToArguments(scenario.nodes_names); + //String type_nctx=listToArguments(scenario.nodes_addresses); + + //String name_nctx=listToArguments(names); + //String type_nctx=listToArguments(addresses); + + String[] name_nctx=listToStringArguments(scenario.nodes_names); + String[] address_nctx=listToStringArguments(scenario.nodes_addresses); + + nctx = new NetContext (ctx, name_nctx, address_nctx); + net = new Network (ctx,new Object[]{nctx}); + + //classes creation mcnet.objects: Map + for(int i=0; i>> adm = new ArrayList>>(); + doMappings(adm, mo); + //System.out.println("adm: " + adm); + net.setAddressMappings(adm); + //setRouting + Map>> ro=new HashMap>>(); + doRouting(ro, mo); + //configureDevice + configureDevice(); + check = new Checker(ctx,nctx,net); + } + + private void setDevice(String name) { + Map value=scenario.chn.get(name); + String type=value.get("functional_type"); + + if(type.compareTo("endhost")==0){ + PolitoEndHost endhost=new PolitoEndHost(ctx, new Object[]{nctx.nm.get(name), net, nctx}); + mo.put(name, endhost); + }else if(type.compareTo("cache")==0){ + PolitoCache cache=new PolitoCache(ctx, new Object[] { nctx.nm.get(name), net, nctx }); + mo.put(name, cache); + }else if(type.compareTo("antispam")==0){ + PolitoAntispam antispam=new PolitoAntispam(ctx, new Object[]{nctx.nm.get(name), net, nctx}); + mo.put(name, antispam); + }else if(type.compareTo("fieldmodifier")==0){ + PolitoFieldModifier fieldmodifier=new PolitoFieldModifier(ctx, new Object[]{nctx.nm.get(name), net, nctx}); + mo.put(name, fieldmodifier); + }else if(type.compareTo("mailclient")==0){ + String conf=(scenario.config_obj.get(name)).get("mailserver"); + PolitoMailClient mailclient=new PolitoMailClient(ctx, new Object[]{nctx.nm.get(name), net, nctx, nctx.am.get(conf)}); + mo.put(name, mailclient); + }else if(type.compareTo("mailserver")==0){ + PolitoMailServer mailserver=new PolitoMailServer(ctx, new Object[]{nctx.nm.get(name), net, nctx}); + mo.put(name, mailserver); + }else if(type.compareTo("nat")==0){ + PolitoNat nat=new PolitoNat(ctx, new Object[]{nctx.nm.get(name), net, nctx}); + mo.put(name, nat); + }else if(type.compareTo("vpnaccess")==0){ + PolitoVpnAccess vpnaccess=new PolitoVpnAccess(ctx, new Object[]{nctx.nm.get(name), net, nctx}); + mo.put(name, vpnaccess); + }else if(type.compareTo("vpnexit")==0){ + PolitoVpnExit vpnexit=new PolitoVpnExit(ctx, new Object[]{nctx.nm.get(name), net, nctx}); + mo.put(name, vpnexit); + }else if(type.compareTo("webserver")==0){ + PolitoWebServer webserver=new PolitoWebServer(ctx, new Object[]{nctx.nm.get(name), net, nctx}); + mo.put(name, webserver); + }else if(type.compareTo("webclient")==0){ + String conf=(scenario.config_obj.get(name)).get("webserver"); + PolitoWebClient webclient=new PolitoWebClient(ctx, new Object[]{nctx.nm.get(name), net, nctx, nctx.am.get(conf)}); + mo.put(name, webclient); + }else if(type.compareTo("dpi")==0){ + PolitoIDS dpi=new PolitoIDS(ctx, new Object[]{nctx.nm.get(name), net, nctx}); + mo.put(name, dpi); + }else if(type.compareTo("endpoint")==0){ + EndHost endpoint=new EndHost(ctx, new Object[]{nctx.nm.get(name), net, nctx}); + mo.put(name, endpoint); + }else if(type.compareTo("firewall")==0){ + AclFirewall firewall=new AclFirewall(ctx, new Object[]{nctx.nm.get(name), net, nctx}); + mo.put(name, firewall); + } + } + + private void configureDevice() { + vlogger.logger.info("Configuration service"); + //System.out.println("Configuration Device"); + for(Map.Entry cd : mo.entrySet()){ + String name=cd.getKey(); + String type=(scenario.chn.get(name)).get("functional_type"); + String address=(scenario.chn.get(name)).get("address"); + Object model=cd.getValue(); + if(model instanceof PolitoEndHost){ + Map packet=scenario.config_obj.get(name); + if(packet!=null){ + PacketModel pModel = new PacketModel(); + if(packet.get("body")!=null){ + pModel.setBody(String.valueOf(packet.get("body")).hashCode()); + } + if(packet.get("destination")!=null){ + pModel.setIp_dest(nctx.am.get(packet.get("destination"))); + } + if(packet.get("sequence")!=null){ + pModel.setSeq(String.valueOf(packet.get("sequence")).hashCode()); + } + if(packet.get("email_from")!=null){ + pModel.setEmailFrom(String.valueOf(packet.get("email_from")).hashCode()); + } + if(packet.get("url")!=null){ + pModel.setUrl(String.valueOf(packet.get("url")).hashCode()); + } + if(packet.get("options")!=null){ + pModel.setOptions(String.valueOf(packet.get("options")).hashCode()); + } + if(packet.get("protocol")!=null){ + String proto=packet.get("protocol"); + if(proto.compareTo("HTTP_REQUEST")==0) + pModel.setProto(nctx.HTTP_REQUEST); + else if(proto.compareTo("HTTP_RESPONSE")==0) + pModel.setProto(nctx.HTTP_RESPONSE); + else if(proto.compareTo("POP3_REQUEST")==0) + pModel.setProto(nctx.POP3_REQUEST); + else if(proto.compareTo("POP3_RESPONSE")==0) + pModel.setProto(nctx.POP3_RESPONSE); + } + ((PolitoEndHost)cd.getValue()).installEndHost(pModel); + } + else{ + vlogger.logger.info("Configuration endhost "+name+"empty"); + } + }else if(model instanceof PolitoCache){ + + List list_tmp=scenario.config_array.get(name); + for(int i=0; i list=trimIp(list_tmp); + if(list!=null){ + PolitoCache cache=(PolitoCache)cd.getValue(); + NetworkObject [] array_no=listToNetworkArguments(list); + ((PolitoCache)cd.getValue()).installCache(array_no); + } + else{ + vlogger.logger.info("Cache "+name+" empty"); + } + }else if(model instanceof PolitoAntispam){ + List list_tmp=scenario.config_array.get(name); + List list=trimIp(list_tmp); + if(list!=null){ + PolitoAntispam antispam=(PolitoAntispam)cd.getValue(); + int[] blackList=listToIntArguments(list); + ((PolitoAntispam)cd.getValue()).installAntispam(blackList); + } + else{ + vlogger.logger.info("Antispam "+name+" empty"); + } + }else if(model instanceof PolitoFieldModifier){ + ((PolitoFieldModifier)cd.getValue()).installFieldModifier(); + }else if(model instanceof PolitoMailClient){ + //the rules are inserted in the init method + continue; + }else if(model instanceof PolitoMailServer){ + //the rules are inserted in the init method + continue; + }else if(model instanceof PolitoNat){ + List list=scenario.config_array.get(name); + if(!list.isEmpty()){ + ArrayList ia = new ArrayList(); + for(String s : list){ + if(scenario.nodes_addresses.contains(s)){ + ia.add(nctx.am.get(s)); + } + } + ((PolitoNat)cd.getValue()).natModel(nctx.am.get(address)); + ((PolitoNat)cd.getValue()).setInternalAddress(ia); + } + else{ + vlogger.logger.info("Nat "+name+" empty"); + } + }else if(model instanceof PolitoVpnAccess){ + Map vpnexit=scenario.config_obj.get(name); + if(vpnexit!=null){ + for(Map.Entry a : vpnexit.entrySet()) + ((PolitoVpnAccess)cd.getValue()).vpnAccessModel(nctx.am.get(address), nctx.am.get(a.getValue())); + } + else{ + vlogger.logger.info("Vpnacces "+name+" empty"); + } + }else if(model instanceof PolitoVpnExit){ + Map vpnaccess=scenario.config_obj.get(name); + if(vpnaccess!=null){ + for(Map.Entry a : vpnaccess.entrySet()) + ((PolitoVpnExit)cd.getValue()).vpnExitModel(nctx.am.get(address), nctx.am.get(a.getValue())); + } + else{ + vlogger.logger.info("Vpnexit "+name+" empty"); + } + + }else if(model instanceof PolitoWebServer){ + //the rules are inserted in the init method + continue; + + }else if(model instanceof PolitoWebClient){ + //the rules are inserted in the init method + continue; + + }else if(model instanceof PolitoIDS){ + List list=scenario.config_array.get(name); + if(!list.isEmpty()){ + PolitoIDS dpi=(PolitoIDS)cd.getValue(); + int[] blackList=listToIntArguments(list); + ((PolitoIDS)cd.getValue()).installIDS(blackList); + } + else{ + vlogger.logger.info("Dpi "+name+" empty"); + } + }else if(model instanceof EndHost){ + //the rules are inserted in the init method + continue; + }else if(model instanceof AclFirewall){ + Map acls=scenario.config_obj.get(name); + ArrayList> acl = new ArrayList>(); + + if(!acls.isEmpty()){ + for(Map.Entry a : acls.entrySet()){ + String dest=a.getKey(); + String src=a.getValue(); + + if(scenario.nodes_addresses.contains("ip_"+dest) && scenario.nodes_addresses.contains("ip_"+src)){ + acl.add(new Tuple(nctx.am.get("ip_"+dest),nctx.am.get("ip_"+src))); + + } + } + ((AclFirewall)cd.getValue()).addAcls(acl); + + } + else{ + vlogger.logger.info("Acls firewall "+name+" empty"); + } + } + else + vlogger.logger.info("No configuration added"); + } + } + + private List trimIp(List list) { + List result=new ArrayList(); + for(String s : list){ + if(s.length()>3){ + if(s.substring(0, 3).compareTo("ip_")==0) + result.add(s.substring(3)); + else + result.add(s); + } + } + return result; + } + + private void doRouting(Map>> ro, Map mo) { + for(String nodes : scenario.nodes_names){ + Object obj=mo.get(nodes); + if(obj!=null){ + ArrayList> rt = new ArrayList>(); + Map route=scenario.routing.get(nodes); + for(Map.Entry r : route.entrySet()){ + String dest=r.getKey(); + NetworkObject next_hop=(NetworkObject)mo.get(r.getValue()); + rt.add(new Tuple(nctx.am.get(dest), next_hop)); + } + net.routingTable((NetworkObject)obj, rt); + net.attach((NetworkObject)obj); + ro.put(nodes, rt); + } + } + } + + private void doMappings(ArrayList>> adm, Map mo) { + for(Map.Entry obj : mo.entrySet()){ + String name=obj.getKey().toString(); + Object model=obj.getValue(); + ArrayList al = new ArrayList(); + al.add(nctx.am.get((scenario.chn.get(name)).get("address"))); + adm.add(new Tuple<>((NetworkObject)(model),al)); + } + } + + //function Arguments: + private String listToArguments(List nodes_names) { + StringBuffer result=new StringBuffer(); + for(int i=0; i arg){ + NetworkObject[] o= new NetworkObject[arg.size()]; + for(int i=0; i arg){ + String[] o= new String[arg.size()]; + for(int i=0; i arg) { + int[] o= new int[arg.size()]; + for(int i=0; i