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