verigraph/src/it/polito/verigraph/mcnet/netobjs/PolitoIDS.java

   1 /*******************************************************************************
   2  * Copyright (c) 2017 Politecnico di Torino and others.
   3  *
   4  * All rights reserved. This program and the accompanying materials
   5  * are made available under the terms of the Apache License, Version 2.0
   6  * which accompanies this distribution, and is available at
   7  * http://www.apache.org/licenses/LICENSE-2.0
   8  *******************************************************************************/
   9 package it.polito.verigraph.mcnet.netobjs;
  10
  11 import java.util.ArrayList;
  12 import java.util.List;
  13 import com.microsoft.z3.BoolExpr;
  14 import com.microsoft.z3.Context;
  15 import com.microsoft.z3.DatatypeExpr;
  16 import com.microsoft.z3.Expr;
  17 import com.microsoft.z3.FuncDecl;
  18 import com.microsoft.z3.IntExpr;
  19 import com.microsoft.z3.Solver;
  20 import it.polito.verigraph.mcnet.components.NetContext;
  21 import it.polito.verigraph.mcnet.components.Network;
  22 import it.polito.verigraph.mcnet.components.NetworkObject;
  23
  24 public class PolitoIDS extends NetworkObject {
  25
  26     public static final int DROGA = 1; //no go
  27     public static final int GATTINI = 2;  //go
  28
  29     Context ctx;
  30     List<BoolExpr> constraints = new ArrayList<BoolExpr>();
  31     DatatypeExpr politoIDS;
  32     Network net;
  33     NetContext nctx;
  34     FuncDecl isInBlacklist;
  35
  36
  37     public PolitoIDS(Context ctx, Object[]...args){
  38         super(ctx, args);
  39     }
  40
  41     @Override
  42     public DatatypeExpr getZ3Node() {
  43         return politoIDS;
  44     }
  45
  46     @Override
  47     protected void init(Context ctx, Object[]... args) {
  48
  49         this.ctx = ctx;
  50         this.isEndHost = false;
  51         this.politoIDS = this.z3Node = ((NetworkObject)args[0][0]).getZ3Node();
  52         this.net = (Network)args[0][1];
  53         this.nctx = (NetContext)args[0][2];
  54
  55     }
  56
  57     @Override
  58     protected void addConstraints(Solver solver) {
  59         BoolExpr[] constr = new BoolExpr[constraints.size()];
  60         solver.add(constraints.toArray(constr));
  61
  62     }
  63
  64     public void installIDS(int[] blackList){
  65         Expr n_0 = ctx.mkConst(politoIDS + "_n_0", nctx.node);
  66         Expr n_1 = ctx.mkConst(politoIDS + "_n_1", nctx.node);
  67         Expr p_0 = ctx.mkConst(politoIDS + "_p_0", nctx.packet);
  68         IntExpr t_0 = ctx.mkIntConst(politoIDS + "_t_0");
  69         IntExpr t_1 = ctx.mkIntConst(politoIDS + "_t_1");
  70         Expr b_0 = ctx.mkIntConst(politoIDS + "_b_0");
  71
  72         isInBlacklist = ctx.mkFuncDecl(politoIDS + "_isInBlacklist", ctx.mkIntSort(), ctx.mkBoolSort());
  73
  74
  75         BoolExpr[] blConstraints = new BoolExpr[blackList.length];
  76         if(blackList.length != 0){
  77
  78             for(int i = 0; i<blackList.length; i++)
  79                 blConstraints[i] = ctx.mkEq(b_0, ctx.mkInt(blackList[i]));
  80
  81             this.constraints.add(ctx.mkForall(new Expr[]{b_0},
  82                     ctx.mkIff((BoolExpr)isInBlacklist.apply(b_0), ctx.mkOr(blConstraints)),
  83                     1,
  84                     null, null, null, null));
  85
  86         }else{
  87             this.constraints.add(ctx.mkForall(new Expr[]{b_0},
  88                     ctx.mkEq(isInBlacklist.apply(b_0), ctx.mkBool(false)),
  89                     1,
  90                     null, null, null, null));
  91         }
  92
  93         //Constraint2 send(politoIDS, n_0, p, t_0) && (p.proto(HTTP_RESPONSE) || p.proto(HTTP_REQUEST)) ->
  94         //(exist  n_1,t_1 : (recv(n_1, politoIDS, p, t_1) && t_1 < t_0)) && !isInBlackList(p.body)
  95
  96         this.constraints.add(ctx.mkForall(new Expr[]{n_0, p_0, t_0},
  97                 ctx.mkImplies(ctx.mkAnd((BoolExpr)nctx.send.apply(politoIDS, n_0, p_0, t_0), ctx.mkOr(ctx.mkEq(nctx.pf.get("proto").apply(p_0), ctx.mkInt(nctx.HTTP_RESPONSE)), ctx.mkEq(nctx.pf.get("proto").apply(p_0), ctx.mkInt(nctx.HTTP_REQUEST)))),
  98                         ctx.mkAnd(ctx.mkExists(new Expr[]{n_1,t_1},
  99                                 ctx.mkAnd((BoolExpr)nctx.recv.apply(n_1,politoIDS,p_0,t_1),ctx.mkLt(t_1, t_0)),
 100                                 1,
 101                                 null, null, null, null),
 102                                 ctx.mkNot((BoolExpr)isInBlacklist.apply(nctx.pf.get("body").apply(p_0))))),
 103                 1,
 104                 null, null, null, null));
 105
 106         //Constraint3 send(politoIDS, n_0, p, t_0) && p.proto(HTTP_REQUEST) ->
 107         //(exist n_1,t_1 : (recv(n_1, politoIDS, p, t_1) && t_1 < t_0)) Constraint not needed anymore (included in contr. 2)
 108         /* this.constraints.add(ctx.mkForall(new Expr[]{n_0, p_0, t_0},
 109               ctx.mkImplies(ctx.mkAnd((BoolExpr)nctx.send.apply(politoIDS, n_0, p_0, t_0), ctx.mkEq(nctx.pf.get("proto").apply(p_0), ctx.mkInt(nctx.HTTP_REQUEST))),
 110               ctx.mkAnd(ctx.mkExists(new Expr[]{n_1,t_1},
 111                  ctx.mkAnd((BoolExpr)nctx.recv.apply(n_1,politoIDS,p_0,t_1),ctx.mkLt(t_1, t_0)),
 112                  1,
 113                  null, null, null, null))),
 114               1,
 115               null, null, null, null));
 116          */
 117
 118         //Constraint5send(politoIDS, n_0, p, t_0) -> p.proto == HTTP_REQ || p.protpo == HTTP_RESP
 119
 120         this.constraints.add(ctx.mkForall(new Expr[]{n_0, p_0, t_0},
 121                 ctx.mkImplies((BoolExpr)nctx.send.apply(politoIDS, n_0, p_0, t_0),
 122                         ctx.mkOr(ctx.mkEq(nctx.pf.get("proto").apply(p_0), ctx.mkInt(nctx.HTTP_REQUEST)),
 123                                 ctx.mkEq(nctx.pf.get("proto").apply(p_0), ctx.mkInt(nctx.HTTP_RESPONSE)))),
 124                 1,
 125                 null,null,null,null));
 126
 127         //Constraint6send(politoIDS, n_0, p, t_0) -> nodeHasAddr(politoIDS,p.src)
 128
 129         this.constraints.add(ctx.mkForall(new Expr[]{n_0, p_0, t_0},
 130                 ctx.mkImplies((BoolExpr)nctx.send.apply(politoIDS, n_0, p_0, t_0),
 131                         ctx.mkNot((BoolExpr)nctx.nodeHasAddr.apply(politoIDS,nctx.pf.get("src").apply(p_0)))),
 132                 1,
 133                 null,null,null,null));
 134
 135
 136
 137     }
 138
 139 }