1 /*******************************************************************************
2 * Copyright (c) 2017 Politecnico di Torino and others.
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;
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;
26 /**Various checks for specific properties in the network.
30 public class Checker {
36 ArrayList<BoolExpr> constraints;
37 public BoolExpr [] assertions;
42 public Checker(Context context,NetContext nctx,Network network){
46 this.solver = ctx.mkSolver();
47 this.constraints = new ArrayList<BoolExpr>();
50 /**Resets the constraints
53 public void clearState (){
55 this.constraints = new ArrayList<BoolExpr>();
58 /**Checks whether the source provided can reach the destination
64 public IsolationResult checkIsolationProperty (NetworkObject src, NetworkObject dest){
65 assert(net.elements.contains(src));
66 assert(net.elements.contains(dest));
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());
78 // Constraint1recv(n_0,destNode,p0,t_0)
79 this.solver.add((BoolExpr)nctx.recv.apply(n_0, dest.getZ3Node(), p0, t_0));
81 // Constraint2send(srcNode,n_1,p1,t_1)
82 this.solver.add((BoolExpr)nctx.send.apply(src.getZ3Node(), n_1, p1, t_1));
84 // Constraint3nodeHasAddr(srcNode,p1.srcAddr)
85 this.solver.add((BoolExpr)nctx.nodeHasAddr.apply(src.getZ3Node(), nctx.pf.get("src").apply(p1)));
88 // Constraint4p1.origin == srcNode
89 this.solver.add(ctx.mkEq(nctx.pf.get("origin").apply(p1), src.getZ3Node()));
91 // Constraint5nodeHasAddr(destNode,p1.destAddr)
92 this.solver.add((BoolExpr)nctx.nodeHasAddr.apply(dest.getZ3Node(), nctx.pf.get("dest").apply(p1)));
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))
100 // Constraint6p1.origin == p0.origin
101 this.solver.add(ctx.mkEq(nctx.pf.get("origin").apply(p1),nctx.pf.get("origin").apply(p0)));
103 // Constraint7nodeHasAddr(destNode, p0.destAddr)
104 this.solver.add((BoolExpr)nctx.nodeHasAddr.apply(dest.getZ3Node(), nctx.pf.get("dest").apply(p0)));
106 result = this.solver.check();
108 assertions = this.solver.getAssertions();
109 if (result == Status.SATISFIABLE){
110 model = this.solver.getModel();
113 return new IsolationResult(ctx,result, p0, n_0, t_1, t_0, nctx, assertions, model);
118 /*public IsolationResult CheckIsolationFlowProperty (NetworkObject src, NetworkObject dest){
119 assert(net.elements.contains(src));
120 assert(net.elements.contains(dest));
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);
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());
133 // Constraint1recv(n_0,destNode,p,t_0)
134 this.solver.add((BoolExpr)nctx.recv.apply(n_0, dest.getZ3Node(), p, t_0));
136 // Constraint2send(srcNode,n_1,p1,t_1)
137 this.solver.add((BoolExpr)nctx.send.apply(src.getZ3Node(), n_1, p, t_1));
139 // Constraint3nodeHasAddr(srcNode,p.srcAddr)
140 this.solver.add((BoolExpr)nctx.nodeHasAddr.apply(src.getZ3Node(), nctx.pf.get("src").apply(p)));
142 // Constraint4p.origin == srcNode
143 this.solver.add(ctx.mkEq(nctx.pf.get("origin").apply(p), src.getZ3Node()));
146 Expr p_2 = ctx.mkConst("check_isolation_p_flow_"+src.getZ3Node()+"_"+dest.getZ3Node(), nctx.packet);
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 &&
155 this.solver.add(ctx.mkNot(ctx.mkExists(new Expr[]{p_2,n_2,t_2},
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},
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))));
172 result = this.solver.check();
174 assertions = this.solver.getAssertions();
175 if (result == Status.SATISFIABLE){
176 model = this.solver.getModel();
179 return new IsolationResult(ctx,result, p, n_0, t_1, t_0, nctx, assertions, model);
184 public IsolationResult CheckNodeTraversalProperty (NetworkObject src, NetworkObject dest, NetworkObject node){
185 assert(net.elements.contains(src));
186 assert(net.elements.contains(dest));
190 Expr p = ctx.mkConst("check_isolation_p_"+src.getZ3Node()+"_"+dest.getZ3Node(), nctx.packet);
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);
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());
200 // Constraint1recv(n_0,destNode,p,t_0)
201 this.solver.add((BoolExpr)nctx.recv.apply(n_0, dest.getZ3Node(), p, t_0));
203 // Constraint2send(srcNode,n_1,p1,t_1)
204 this.solver.add((BoolExpr)nctx.send.apply(src.getZ3Node(), n_1, p, t_1));
206 // Constraint3nodeHasAddr(srcNode,p.srcAddr)
207 this.solver.add((BoolExpr)nctx.nodeHasAddr.apply(src.getZ3Node(), nctx.pf.get("src").apply(p)));
209 // Constraint4p.origin == srcNode
210 this.solver.add(ctx.mkEq(nctx.pf.get("origin").apply(p), src.getZ3Node()));
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},
216 (BoolExpr)nctx.recv.apply(n_2, node.getZ3Node(), p, t_2),
217 ctx.mkLt(t_2,t_0)),1,null,null,null,null)));
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},
222 (BoolExpr)nctx.send.apply(node.getZ3Node(), n_2, p, t_2),
223 ctx.mkLt(t_2,t_0)),1,null,null,null,null)));
226 result = this.solver.check();
228 assertions = this.solver.getAssertions();
229 if (result == Status.SATISFIABLE){
230 model = this.solver.getModel();
233 return new IsolationResult(ctx,result, p, n_0, t_1, t_0, nctx, assertions, model);
237 public IsolationResult CheckLinkTraversalProperty (NetworkObject src, NetworkObject dest, NetworkObject le0, NetworkObject le1){
238 assert(net.elements.contains(src));
239 assert(net.elements.contains(dest));
243 Expr p = ctx.mkConst("check_isolation_p_"+src.getZ3Node()+"_"+dest.getZ3Node(), nctx.packet);
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);
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());
252 // Constraint1recv(n_0,destNode,p,t_0)
253 this.solver.add((BoolExpr)nctx.recv.apply(n_0, dest.getZ3Node(), p, t_0));
255 // Constraint2send(srcNode,n_1,p,t_1)
256 this.solver.add((BoolExpr)nctx.send.apply(src.getZ3Node(), n_1, p, t_1));
258 // Constraint3nodeHasAddr(srcNode,p.srcAddr)
259 this.solver.add((BoolExpr)nctx.nodeHasAddr.apply(src.getZ3Node(), nctx.pf.get("src").apply(p)));
261 // Constraint4p.origin == srcNode
262 this.solver.add(ctx.mkEq(nctx.pf.get("origin").apply(p), src.getZ3Node()));
264 //Constraint5∃ t_1, t_2 :
265 // send(linkNode0,linkNode1,p,t_1) &&
266 // recv(linkNode0,linkNode1,p,t_2) &&
269 this.solver.add(ctx.mkExists(new Expr[]{t_1,t_2},
271 (BoolExpr)nctx.send.apply(le0.getZ3Node(), le1.getZ3Node(), p, t_1),
272 (BoolExpr)nctx.recv.apply(le0.getZ3Node(), le1.getZ3Node(), p, t_2),
274 ctx.mkLt(t_2,t_0)),1,null,null,null,null));
277 result = this.solver.check();
279 assertions = this.solver.getAssertions();
280 if (result == Status.SATISFIABLE){
281 model = this.solver.getModel();
284 return new IsolationResult(ctx,result, p, n_0, t_1, t_0, nctx, assertions, model);
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());
293 Expr p = ctx.mkConst("check_isolation_p_"+src.getZ3Node()+"_"+dest.getZ3Node(), nctx.packet);
295 Expr n_0 =ctx.mkConst("check_isolation_n_0_"+src.getZ3Node()+"_"+dest.getZ3Node(), nctx.node);
297 IntExpr t = ctx.mkIntConst("check_isolation_t_"+src.getZ3Node()+"_"+dest.getZ3Node());
299 // Constraint1recv(n_0,destNode,p,t)
300 constr.add((BoolExpr)nctx.recv.apply(n_0, dest.getZ3Node(), p, t));
303 // Constraint2p.origin == srcNode
304 this.solver.add(ctx.mkEq(nctx.pf.get("origin").apply(p), src.getZ3Node()));
308 // Constraint3for each constraint( n -> constraint)
309 ArrayList<BoolExpr> names =new ArrayList<BoolExpr>();
310 for(BoolExpr con : constr){
311 BoolExpr n = ctx.mkBoolConst(""+con);
313 this.solver.add(ctx.mkImplies(n, con));
316 BoolExpr[] nam = new BoolExpr[names.size()];
317 result = this.solver.check(names.toArray(nam));
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());
331 public DataIsolationResult CheckDataIsolationProperty(NetworkObject src, NetworkObject dest){
332 assert(net.elements.contains(src));
333 assert(net.elements.contains(dest));
337 Expr p = ctx.mkConst("check_isolation_p_"+src.getZ3Node()+"_"+dest.getZ3Node(), nctx.packet);
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());
342 // Constraint1recv(n_0,destNode,p,t)
343 this.solver.add((BoolExpr)nctx.recv.apply(n_0, dest.getZ3Node(), p, t));
345 // Constraint2p.origin == srcNode
346 this.solver.add(ctx.mkEq(nctx.pf.get("origin").apply(p), src.getZ3Node()));
348 result = this.solver.check();
350 assertions = this.solver.getAssertions();
351 if (result == Status.SATISFIABLE){
352 model = this.solver.getModel();
355 return new DataIsolationResult(ctx,result, p, n_0, t, nctx, assertions, model);
361 public void addConstraints(){
362 nctx.addConstraints(solver);
363 net.addConstraints(solver);
364 for (NetworkObject el : net.elements)
365 el.addConstraints(solver);
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());