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