verigraph/service/src/mcnet/components/Checker.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.components;
  11
  12
  13 import java.util.ArrayList;
  14 import java.util.Arrays;
  15 import java.util.List;
  16
  17 import com.microsoft.z3.BoolExpr;
  18 import com.microsoft.z3.Context;
  19 import com.microsoft.z3.Expr;
  20 import com.microsoft.z3.IntExpr;
  21 import com.microsoft.z3.Model;
  22 import com.microsoft.z3.Solver;
  23 import com.microsoft.z3.Status;
  24
  25 /**Various checks for specific properties in the network.
  26  *
  27  */
  28 public class Checker {
  29
  30         Context ctx;
  31         Network net;
  32         NetContext nctx;
  33         Solver solver;
  34         ArrayList<BoolExpr> constraints;
  35         public BoolExpr [] assertions;
  36         public Status result;
  37         public Model model;
  38
  39
  40    public Checker(Context context,NetContext nctx,Network network){
  41         this.ctx = context;
  42         this.net = network;
  43         this.nctx = nctx;
  44         this.solver = ctx.mkSolver();
  45         this.constraints = new ArrayList<BoolExpr>();
  46    }
  47
  48    /**Resets the constraints
  49     *
  50     */
  51     public void clearState (){
  52         this.solver.reset();
  53         this.constraints = new ArrayList<BoolExpr>();
  54     }
  55
  56         /**Checks whether the source provided can reach the destination
  57          *
  58          * @param src
  59          * @param dest
  60          * @return
  61          */
  62         public IsolationResult checkIsolationProperty (NetworkObject src, NetworkObject dest){
  63                 assert(net.elements.contains(src));
  64             assert(net.elements.contains(dest));
  65             solver.push ();
  66             addConstraints();
  67
  68             Expr p0 = ctx.mkConst("check_isolation_p0_"+src.getZ3Node()+"_"+dest.getZ3Node(), nctx.packet);
  69             Expr p1 = ctx.mkConst("check_isolation_p1_"+src.getZ3Node()+"_"+dest.getZ3Node(), nctx.packet);
  70             Expr n_0 =ctx.mkConst("check_isolation_n_0_"+src.getZ3Node()+"_"+dest.getZ3Node(), nctx.node);
  71             Expr n_1 =ctx.mkConst("check_isolation_n_1_"+src.getZ3Node()+"_"+dest.getZ3Node(), nctx.node);
  72             IntExpr t_0 = ctx.mkIntConst("check_isolation_t0_"+src.getZ3Node()+"_"+dest.getZ3Node());
  73             IntExpr t_1 = ctx.mkIntConst("check_isolation_t1_"+src.getZ3Node()+"_"+dest.getZ3Node());
  74
  75         //              Constraint1             recv(n_0,destNode,p0,t_0)
  76             this.solver.add((BoolExpr)nctx.recv.apply(n_0, dest.getZ3Node(), p0, t_0));
  77
  78         //              Constraint2             send(srcNode,n_1,p1,t_1)
  79             this.solver.add((BoolExpr)nctx.send.apply(src.getZ3Node(), n_1, p1, t_1));
  80
  81         //              Constraint3             nodeHasAddr(srcNode,p1.srcAddr)
  82             this.solver.add((BoolExpr)nctx.nodeHasAddr.apply(src.getZ3Node(), nctx.pf.get("src").apply(p1)));
  83
  84         //              Constraint4             p1.origin == srcNode
  85             this.solver.add(ctx.mkEq(nctx.pf.get("origin").apply(p1), src.getZ3Node()));
  86
  87         //              Constraint5             nodeHasAddr(destNode,p1.destAddr)
  88             this.solver.add((BoolExpr)nctx.nodeHasAddr.apply(dest.getZ3Node(), nctx.pf.get("dest").apply(p1)));
  89
  90                 //NON sembrano necessari
  91                 //         this.solver.add(z3.Or(this.ctx.nodeHasAddr(src.getZ3Node(), this.ctx.packet.src(p0)),\
  92                 //                               this.ctx.nodeHasAddr(n_0, this.ctx.packet.src(p0)),\
  93                 //                               this.ctx.nodeHasAddr(n_1, this.ctx.packet.src(p0))))
  94                 //this.solver.add(this.ctx.packet.dest(p1) == this.ctx.packet.dest(p0))
  95
  96         //              Constraint6             p1.origin ==  p0.origin
  97             this.solver.add(ctx.mkEq(nctx.pf.get("origin").apply(p1),nctx.pf.get("origin").apply(p0)));
  98
  99         //              Constraint7             nodeHasAddr(destNode, p0.destAddr)
 100             this.solver.add((BoolExpr)nctx.nodeHasAddr.apply(dest.getZ3Node(), nctx.pf.get("dest").apply(p0)));
 101
 102             result = this.solver.check();
 103             model = null;
 104             assertions = this.solver.getAssertions();
 105             if (result == Status.SATISFIABLE){
 106                 model = this.solver.getModel();
 107             }
 108             this.solver.pop();
 109             return new IsolationResult(ctx,result, p0, n_0, t_1, t_0, nctx, assertions, model);
 110         }
 111
 112
 113
 114         public IsolationResult CheckIsolationFlowProperty (NetworkObject src, NetworkObject dest){
 115                 assert(net.elements.contains(src));
 116             assert(net.elements.contains(dest));
 117             solver.push ();
 118             addConstraints();
 119
 120             Expr p = ctx.mkConst("check_isolation_p_"+src.getZ3Node()+"_"+dest.getZ3Node(), nctx.packet);
 121             Expr n_0 =ctx.mkConst("check_isolation_n_0_"+src.getZ3Node()+"_"+dest.getZ3Node(), nctx.node);
 122             Expr n_1 =ctx.mkConst("check_isolation_n_1_"+src.getZ3Node()+"_"+dest.getZ3Node(), nctx.node);
 123             Expr n_2 =ctx.mkConst("check_isolation_n_1_"+src.getZ3Node()+"_"+dest.getZ3Node(), nctx.node);
 124
 125             IntExpr t_0 = ctx.mkIntConst("check_isolation_t0_"+src.getZ3Node()+"_"+dest.getZ3Node());
 126             IntExpr t_1 = ctx.mkIntConst("check_isolation_t1_"+src.getZ3Node()+"_"+dest.getZ3Node());
 127             IntExpr t_2 = ctx.mkIntConst("check_isolation_t2_"+src.getZ3Node()+"_"+dest.getZ3Node());
 128
 129         //              Constraint1             recv(n_0,destNode,p,t_0)
 130             this.solver.add((BoolExpr)nctx.recv.apply(n_0, dest.getZ3Node(), p, t_0));
 131
 132         //              Constraint2             send(srcNode,n_1,p1,t_1)
 133             this.solver.add((BoolExpr)nctx.send.apply(src.getZ3Node(), n_1, p, t_1));
 134
 135         //              Constraint3             nodeHasAddr(srcNode,p.srcAddr)
 136             this.solver.add((BoolExpr)nctx.nodeHasAddr.apply(src.getZ3Node(), nctx.pf.get("src").apply(p)));
 137
 138         //              Constraint4             p.origin == srcNode
 139             this.solver.add(ctx.mkEq(nctx.pf.get("origin").apply(p), src.getZ3Node()));
 140
 141
 142             Expr p_2 = ctx.mkConst("check_isolation_p_flow_"+src.getZ3Node()+"_"+dest.getZ3Node(), nctx.packet);
 143
 144             //      Constraint5         there does not exist p_2, n_2, t_2 :
 145                                                         //                       send(destNode,n_2,p_2,t_2) &&
 146                                                         //                   p_2.srcAddr == p. destAddr &&
 147                                                         //                   p_2.srcPort == p.destPort &&
 148                                                         //                   p_2.destPort == p.srcPort &&
 149                                                         //                   p_2.destt == p.src &&
 150                                                         //                   t_2 < t_0
 151             this.solver.add(ctx.mkNot(ctx.mkExists(new Expr[]{p_2,n_2,t_2},
 152                                         ctx.mkAnd(
 153                                                         (BoolExpr)nctx.send.apply(dest.getZ3Node(), n_2, p_2, t_2),
 154                                                         ctx.mkEq(nctx.pf.get("src").apply(p_2), nctx.pf.get("dest").apply(p)),
 155                                                         ctx.mkEq(nctx.pf.get("src_port").apply(p_2), nctx.pf.get("dest_port").apply(p)),
 156                                                         ctx.mkEq(nctx.pf.get("dest_port").apply(p_2), nctx.pf.get("src_port").apply(p)),
 157                                                         ctx.mkEq(nctx.pf.get("dest").apply(p_2), nctx.pf.get("src").apply(p)),
 158                                                         ctx.mkLt(t_2,t_0)),1,null,null,null,null)));
 159
 160
 161             result = this.solver.check();
 162             model = null;
 163             assertions = this.solver.getAssertions();
 164             if (result == Status.SATISFIABLE){
 165                 model = this.solver.getModel();
 166             }
 167             this.solver.pop();
 168             return new IsolationResult(ctx,result, p, n_0, t_1, t_0, nctx, assertions, model);
 169         }
 170
 171
 172
 173     public IsolationResult CheckNodeTraversalProperty (NetworkObject src, NetworkObject dest, NetworkObject node){
 174                 assert(net.elements.contains(src));
 175             assert(net.elements.contains(dest));
 176             solver.push ();
 177             addConstraints();
 178
 179             Expr p = ctx.mkConst("check_isolation_p_"+src.getZ3Node()+"_"+dest.getZ3Node(), nctx.packet);
 180
 181             Expr n_0 =ctx.mkConst("check_isolation_n_0_"+src.getZ3Node()+"_"+dest.getZ3Node(), nctx.node);
 182             Expr n_1 =ctx.mkConst("check_isolation_n_1_"+src.getZ3Node()+"_"+dest.getZ3Node(), nctx.node);
 183             Expr n_2 =ctx.mkConst("check_isolation_n_1_"+src.getZ3Node()+"_"+dest.getZ3Node(), nctx.node);
 184
 185             IntExpr t_0 = ctx.mkIntConst("check_isolation_t0_"+src.getZ3Node()+"_"+dest.getZ3Node());
 186             IntExpr t_1 = ctx.mkIntConst("check_isolation_t1_"+src.getZ3Node()+"_"+dest.getZ3Node());
 187             IntExpr t_2 = ctx.mkIntConst("check_isolation_t2_"+src.getZ3Node()+"_"+dest.getZ3Node());
 188
 189         //              Constraint1             recv(n_0,destNode,p,t_0)
 190             this.solver.add((BoolExpr)nctx.recv.apply(n_0, dest.getZ3Node(), p, t_0));
 191
 192         //              Constraint2             send(srcNode,n_1,p1,t_1)
 193             this.solver.add((BoolExpr)nctx.send.apply(src.getZ3Node(), n_1, p, t_1));
 194
 195         //              Constraint3             nodeHasAddr(srcNode,p.srcAddr)
 196             this.solver.add((BoolExpr)nctx.nodeHasAddr.apply(src.getZ3Node(), nctx.pf.get("src").apply(p)));
 197
 198         //              Constraint4             p.origin == srcNode
 199             this.solver.add(ctx.mkEq(nctx.pf.get("origin").apply(p), src.getZ3Node()));
 200
 201
 202         //                      Constraint5             there does not exist n_2, t_2 : recv(n_2,node,p,t_2) && t_2 < t_0
 203             this.solver.add(ctx.mkNot(ctx.mkExists(new Expr[]{n_2,t_2},
 204                                         ctx.mkAnd(
 205                                                         (BoolExpr)nctx.recv.apply(n_2, node.getZ3Node(), p, t_2),
 206                                                         ctx.mkLt(t_2,t_0)),1,null,null,null,null)));
 207
 208         //                      Constraint 6    there does not exist n_2, t_2 : send(node,n_2,p,t_2) && t_2 < t_0
 209             this.solver.add(ctx.mkNot(ctx.mkExists(new Expr[]{n_2,t_2},
 210                                 ctx.mkAnd(
 211                                                 (BoolExpr)nctx.send.apply(node.getZ3Node(), n_2, p, t_2),
 212                                                 ctx.mkLt(t_2,t_0)),1,null,null,null,null)));
 213
 214
 215             result = this.solver.check();
 216             model = null;
 217             assertions = this.solver.getAssertions();
 218             if (result == Status.SATISFIABLE){
 219                 model = this.solver.getModel();
 220             }
 221             this.solver.pop();
 222             return new IsolationResult(ctx,result, p, n_0, t_1, t_0, nctx, assertions, model);
 223
 224     }
 225
 226     public IsolationResult CheckLinkTraversalProperty (NetworkObject src, NetworkObject dest, NetworkObject le0, NetworkObject le1){
 227                 assert(net.elements.contains(src));
 228             assert(net.elements.contains(dest));
 229             solver.push ();
 230             addConstraints();
 231
 232             Expr p = ctx.mkConst("check_isolation_p_"+src.getZ3Node()+"_"+dest.getZ3Node(), nctx.packet);
 233
 234             Expr n_0 =ctx.mkConst("check_isolation_n_0_"+src.getZ3Node()+"_"+dest.getZ3Node(), nctx.node);
 235             Expr n_1 =ctx.mkConst("check_isolation_n_1_"+src.getZ3Node()+"_"+dest.getZ3Node(), nctx.node);
 236
 237             IntExpr t_0 = ctx.mkIntConst("check_isolation_t0_"+src.getZ3Node()+"_"+dest.getZ3Node());
 238             IntExpr t_1 = ctx.mkIntConst("check_isolation_t1_"+src.getZ3Node()+"_"+dest.getZ3Node());
 239             IntExpr t_2 = ctx.mkIntConst("check_isolation_t2_"+src.getZ3Node()+"_"+dest.getZ3Node());
 240
 241         //              Constraint1             recv(n_0,destNode,p,t_0)
 242             this.solver.add((BoolExpr)nctx.recv.apply(n_0, dest.getZ3Node(), p, t_0));
 243
 244         //              Constraint2             send(srcNode,n_1,p1,t_1)
 245             this.solver.add((BoolExpr)nctx.send.apply(src.getZ3Node(), n_1, p, t_1));
 246
 247         //              Constraint3             nodeHasAddr(srcNode,p.srcAddr)
 248             this.solver.add((BoolExpr)nctx.nodeHasAddr.apply(src.getZ3Node(), nctx.pf.get("src").apply(p)));
 249
 250         //              Constraint4             p.origin == srcNode
 251             this.solver.add(ctx.mkEq(nctx.pf.get("origin").apply(p), src.getZ3Node()));
 252
 253         //                      Constraint5             ∃ t_1, t_2 :
 254                                                 //          send(linkNode0,linkNode1,p,t_1) &&
 255                                                         //          recv(linkNode0,linkNode1,p,t_2) &&
 256                                                         //          t_1 < t_0 &&
 257                                                         //          t_2 < t_0
 258             this.solver.add(ctx.mkExists(new Expr[]{t_1,t_2},
 259                                         ctx.mkAnd(
 260                                                         (BoolExpr)nctx.send.apply(le0.getZ3Node(), le1.getZ3Node(), p, t_1),
 261                                                         (BoolExpr)nctx.recv.apply(le0.getZ3Node(), le1.getZ3Node(), p, t_2),
 262                                                         ctx.mkLt(t_1,t_0),
 263                                                         ctx.mkLt(t_2,t_0)),1,null,null,null,null));
 264
 265
 266             result = this.solver.check();
 267             model = null;
 268             assertions = this.solver.getAssertions();
 269             if (result == Status.SATISFIABLE){
 270                 model = this.solver.getModel();
 271             }
 272             this.solver.pop();
 273             return new IsolationResult(ctx,result, p, n_0, t_1, t_0, nctx, assertions, model);
 274
 275     }
 276
 277    public Result CheckDataIsolationPropertyCore (NetworkObject src, NetworkObject dest){
 278                 assert(net.elements.contains(src));
 279             assert(net.elements.contains(dest));
 280             List<BoolExpr> constr = this.getConstraints();
 281             Expr p = ctx.mkConst("check_isolation_p_"+src.getZ3Node()+"_"+dest.getZ3Node(), nctx.packet);
 282
 283             Expr n_0 =ctx.mkConst("check_isolation_n_0_"+src.getZ3Node()+"_"+dest.getZ3Node(), nctx.node);
 284             IntExpr t = ctx.mkIntConst("check_isolation_t_"+src.getZ3Node()+"_"+dest.getZ3Node());
 285
 286         //              Constraint1             recv(n_0,destNode,p,t)
 287             constr.add((BoolExpr)nctx.recv.apply(n_0, dest.getZ3Node(), p, t));
 288
 289         //              Constraint2             p.origin == srcNode
 290             this.solver.add(ctx.mkEq(nctx.pf.get("origin").apply(p), src.getZ3Node()));
 291
 292             this.solver.push();
 293
 294     //             Constraint3          for each constraint( n -> constraint)
 295             ArrayList<BoolExpr> names =new ArrayList<BoolExpr>();
 296             for(BoolExpr con : constr){
 297                 BoolExpr n = ctx.mkBoolConst(""+con);
 298                 names.add(n);
 299                 this.solver.add(ctx.mkImplies(n, con));
 300             }
 301
 302             BoolExpr[] nam = new BoolExpr[names.size()];
 303             result = this.solver.check(names.toArray(nam));
 304             Result ret =null;
 305
 306             if (result == Status.SATISFIABLE){
 307                 System.out.println("SAT");
 308                 ret = new Result(ctx,this.solver.getModel());
 309             }else if(result == Status.UNSATISFIABLE){
 310                 System.out.println("unsat");
 311                 ret = new Result(ctx,this.solver.getUnsatCore());
 312             }
 313             this.solver.pop();
 314             return ret;
 315    }
 316
 317     public DataIsolationResult CheckDataIsolationProperty(NetworkObject src, NetworkObject dest){
 318         assert(net.elements.contains(src));
 319             assert(net.elements.contains(dest));
 320             solver.push ();
 321             addConstraints();
 322
 323             Expr p = ctx.mkConst("check_isolation_p_"+src.getZ3Node()+"_"+dest.getZ3Node(), nctx.packet);
 324
 325             Expr n_0 =ctx.mkConst("check_isolation_n_0_"+src.getZ3Node()+"_"+dest.getZ3Node(), nctx.node);
 326             IntExpr t = ctx.mkIntConst("check_isolation_t_"+src.getZ3Node()+"_"+dest.getZ3Node());
 327
 328         //              Constraint1             recv(n_0,destNode,p,t)
 329             this.solver.add((BoolExpr)nctx.recv.apply(n_0, dest.getZ3Node(), p, t));
 330
 331         //              Constraint2             p.origin == srcNode
 332             this.solver.add(ctx.mkEq(nctx.pf.get("origin").apply(p), src.getZ3Node()));
 333
 334             result = this.solver.check();
 335             model = null;
 336             assertions = this.solver.getAssertions();
 337             if (result == Status.SATISFIABLE){
 338                 model = this.solver.getModel();
 339             }
 340             this.solver.pop();
 341             return new DataIsolationResult(ctx,result, p, n_0, t, nctx, assertions, model);
 342     }
 343
 344
 345
 346
 347         public void addConstraints(){
 348             nctx.addConstraints(solver);
 349             net.addConstraints(solver);
 350             for (NetworkObject el : net.elements)
 351                 el.addConstraints(solver);
 352         }
 353
 354
 355          public List<BoolExpr> getConstraints(){
 356                 Solver l = ctx.mkSolver();
 357                 nctx.addConstraints(l);
 358                 net.addConstraints(l);
 359                 for (NetworkObject el : net.elements)
 360                     el.addConstraints(l);
 361                 return Arrays.asList(l.getAssertions());
 362         }
 363 }