summaryrefslogtreecommitdiffstats
path: root/setup.py
blob: a1e9b3bb2518a83ef1116fe6c0a7133d82817198 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
#!/usr/bin/env python

# Copyright (c) 2017 Orange and others.
#
# All rights reserved. This program and the accompanying materials
# are made available under the terms of the Apache License, Version 2.0
# which accompanies this distribution, and is available at
# http://www.apache.org/licenses/LICENSE-2.0

import setuptools

# In python < 2.7.4, a lazy loading of package `pbr` will break
# setuptools if some other modules registered functions in `atexit`.
# solution from: http://bugs.python.org/issue15881#msg170215
try:
    import multiprocessing  # noqa
except ImportError:
    pass

setuptools.setup(
    setup_requires=['pbr>=1.8'],
    pbr=True)
tring.Affix */ .highlight .sb { color: #dd2200; background-color: #fff0f0 } /* Literal.String.Backtick */ .highlight .sc { color: #dd2200; background-color: #fff0f0 } /* Literal.String.Char */ .highlight .dl { color: #dd2200; background-color: #fff0f0 } /* Literal.String.Delimiter */ .highlight .sd { color: #dd2200; background-color: #fff0f0 } /* Literal.String.Doc */ .highlight .s2 { color: #dd2200; background-color: #fff0f0 } /* Literal.String.Double */ .highlight .se { color: #0044dd; background-color: #fff0f0 } /* Literal.String.Escape */ .highlight .sh { color: #dd2200; background-color: #fff0f0 } /* Literal.String.Heredoc */ .highlight .si { color: #3333bb; background-color: #fff0f0 } /* Literal.String.Interpol */ .highlight .sx { color: #22bb22; background-color: #f0fff0 } /* Literal.String.Other */ .highlight .sr { color: #008800; background-color: #fff0ff } /* Literal.String.Regex */ .highlight .s1 { color: #dd2200; background-color: #fff0f0 } /* Literal.String.Single */ .highlight .ss { color: #aa6600; background-color: #fff0f0 } /* Literal.String.Symbol */ .highlight .bp { color: #003388 } /* Name.Builtin.Pseudo */ .highlight .fm { color: #0066bb; font-weight: bold } /* Name.Function.Magic */ .highlight .vc { color: #336699 } /* Name.Variable.Class */ .highlight .vg { color: #dd7700 } /* Name.Variable.Global */ .highlight .vi { color: #3333bb } /* Name.Variable.Instance */ .highlight .vm { color: #336699 } /* Name.Variable.Magic */ .highlight .il { color: #0000DD; font-weight: bold } /* Literal.Number.Integer.Long */ }
/*******************************************************************************
 * Copyright (c) 2017 Politecnico di Torino and others.
 *
 * All rights reserved. This program and the accompanying materials
 * are made available under the terms of the Apache License, Version 2.0
 * which accompanies this distribution, and is available at
 * http://www.apache.org/licenses/LICENSE-2.0
 *******************************************************************************/

package mcnet.netobjs;

import java.util.ArrayList;
import java.util.List;

import com.microsoft.z3.BoolExpr;
import com.microsoft.z3.Context;
import com.microsoft.z3.DatatypeExpr;
import com.microsoft.z3.Expr;
import com.microsoft.z3.FuncDecl;
import com.microsoft.z3.IntExpr;
import com.microsoft.z3.Solver;

import mcnet.components.NetContext;
import mcnet.components.Network;
import mcnet.components.NetworkObject;

public class PolitoVpnExit extends NetworkObject {

	List<BoolExpr> constraints = new ArrayList<BoolExpr>();
	DatatypeExpr politoVpnExit;
	FuncDecl private_addr_func;
	NetContext nctx;
	Context ctx;
	Network net;

	public PolitoVpnExit(Context ctx, Object[]... args) {
		super(ctx, args);
	}

	@Override
	public DatatypeExpr getZ3Node() {
		return politoVpnExit;
	}

	@Override
	protected void init(Context ctx, Object[]... args) {
		this.ctx = ctx;
		this.isEndHost = false;
		this.politoVpnExit = this.z3Node = ((NetworkObject)args[0][0]).getZ3Node();
		this.net = (Network)args[0][1];
        this.nctx = (NetContext)args[0][2];
	}

	@Override
	protected void addConstraints(Solver solver) {
		BoolExpr[] constr = new BoolExpr[constraints.size()];
	    solver.add(constraints.toArray(constr));
	}

	public void vpnAccessModel(DatatypeExpr vpnAccessIp, DatatypeExpr vpnExitIp) {
		Expr x = ctx.mkConst("vpn_x", nctx.node);
		Expr y = ctx.mkConst("vpn_y", nctx.node);

		Expr p_0 = ctx.mkConst("vpn_p_0", nctx.packet);
		Expr p_1 = ctx.mkConst("vpn_p_1", nctx.packet);

		IntExpr t_0 = ctx.mkIntConst("vpn_t_0");
		IntExpr t_1 = ctx.mkIntConst("vpn_t_1");

		private_addr_func = ctx.mkFuncDecl("vpn_private_addr_func", nctx.address, ctx.mkBoolSort());

		BoolExpr constraint1 = ctx.mkForall(new Expr[]{t_0, p_0, x},
				ctx.mkImplies(ctx.mkAnd(
									  (BoolExpr)nctx.send.apply(politoVpnExit, x, p_0, t_0),
									  ctx.mkEq(nctx.pf.get("inner_src").apply(p_0), nctx.am.get("null"))),
							  ctx.mkAnd(
									  (BoolExpr)private_addr_func.apply(nctx.pf.get("src").apply(p_0)),
									  ctx.mkNot((BoolExpr)nctx.pf.get("encrypted").apply(p_0)),
									  ctx.mkExists(new Expr[]{y, p_1, t_1},
											  ctx.mkAnd((BoolExpr)nctx.recv.apply(y, politoVpnExit, p_1, t_1),
													    ctx.mkLt(t_1, t_0),
													    (BoolExpr)nctx.pf.get("encrypted").apply(p_1),
													    ctx.mkEq(nctx.pf.get("src").apply(p_1), vpnAccessIp),
													    ctx.mkEq(nctx.pf.get("dest").apply(p_1), vpnExitIp),
													    ctx.mkEq(nctx.pf.get("inner_src").apply(p_1), nctx.pf.get("src").apply(p_0)),
													    ctx.mkEq(nctx.pf.get("inner_dest").apply(p_1), nctx.pf.get("dest").apply(p_0)),
													    ctx.mkEq(nctx.pf.get("origin").apply(p_1), nctx.pf.get("origin").apply(p_0)),
													    ctx.mkEq(nctx.pf.get("orig_body").apply(p_1), nctx.pf.get("orig_body").apply(p_0)),
													    ctx.mkEq(nctx.pf.get("body").apply(p_1), nctx.pf.get("body").apply(p_0)),
													    ctx.mkEq(nctx.pf.get("seq").apply(p_1), nctx.pf.get("seq").apply(p_0)),
													    ctx.mkEq(nctx.pf.get("proto").apply(p_1), nctx.pf.get("proto").apply(p_0)),
													    ctx.mkEq(nctx.pf.get("emailFrom").apply(p_1), nctx.pf.get("emailFrom").apply(p_0)),
													    ctx.mkEq(nctx.pf.get("url").apply(p_1), nctx.pf.get("url").apply(p_0)),
													    ctx.mkEq(nctx.pf.get("options").apply(p_1), nctx.pf.get("options").apply(p_0))), 1, null, null, null, null))),
			1,null,null,null,null);

		constraints.add(constraint1);

		BoolExpr constraint2 = ctx.mkForall(new Expr[]{t_0, p_0, x},
				ctx.mkImplies(ctx.mkAnd(
									  (BoolExpr)nctx.send.apply(politoVpnExit, x, p_0, t_0),
									  ctx.mkNot(ctx.mkEq(nctx.pf.get("inner_src").apply(p_0), nctx.am.get("null")))),
							  ctx.mkAnd(
									  ctx.mkEq(nctx.pf.get("src").apply(p_0), vpnExitIp),
									  ctx.mkEq(nctx.pf.get("dest").apply(p_0), vpnAccessIp),
									  (BoolExpr)private_addr_func.apply(nctx.pf.get("dest").apply(p_0)),
									  ctx.mkNot(ctx.mkEq(nctx.pf.get("inner_dest").apply(p_1), vpnExitIp)),
									  (BoolExpr)nctx.pf.get("encrypted").apply(p_0),
									  ctx.mkExists(new Expr[]{y, p_1, t_1},
											  ctx.mkAnd((BoolExpr)nctx.recv.apply(y, politoVpnExit, p_1, t_1),
													    ctx.mkLt(t_1, t_0),
													    ctx.mkNot((BoolExpr)nctx.pf.get("encrypted").apply(p_1)),
													    ctx.mkEq(nctx.pf.get("src").apply(p_1), nctx.pf.get("inner_src").apply(p_0)),
													    ctx.mkEq(nctx.pf.get("dest").apply(p_1), nctx.pf.get("inner_dest").apply(p_0)),
													    ctx.mkEq(nctx.pf.get("inner_src").apply(p_1), nctx.am.get("null")),
													    ctx.mkEq(nctx.pf.get("inner_dest").apply(p_1), nctx.am.get("null")),
													    ctx.mkEq(nctx.pf.get("origin").apply(p_1), nctx.pf.get("origin").apply(p_0)),
													    ctx.mkEq(nctx.pf.get("orig_body").apply(p_1), nctx.pf.get("orig_body").apply(p_0)),
													    ctx.mkEq(nctx.pf.get("body").apply(p_1), nctx.pf.get("body").apply(p_0)),
													    ctx.mkEq(nctx.pf.get("seq").apply(p_1), nctx.pf.get("seq").apply(p_0)),
													    ctx.mkEq(nctx.pf.get("proto").apply(p_1), nctx.pf.get("proto").apply(p_0)),
													    ctx.mkEq(nctx.pf.get("emailFrom").apply(p_1), nctx.pf.get("emailFrom").apply(p_0)),
													    ctx.mkEq(nctx.pf.get("url").apply(p_1), nctx.pf.get("url").apply(p_0)),
													    ctx.mkEq(nctx.pf.get("options").apply(p_1), nctx.pf.get("options").apply(p_0))), 1, null, null, null, null))),
				1,null,null,null,null);

		constraints.add(constraint2);
	}

	public void setInternalAddress(ArrayList<DatatypeExpr> internalAddress){
    	List<BoolExpr> constr = new ArrayList<BoolExpr>();
    	Expr n_0 = ctx.mkConst("vpn_node", nctx.address);

    	for(DatatypeExpr n : internalAddress){
    		constr.add(ctx.mkEq(n_0,n));
    	}
    	BoolExpr[] constrs = new BoolExpr[constr.size()];
    	//Constraint		private_addr_func(n_0) == or(n_0==n foreach internal address)
    	constraints.add(ctx.mkForall(new Expr[]{n_0}, ctx.mkEq(private_addr_func.apply(n_0),ctx.mkOr(constr.toArray(constrs))),1,null,null,null,null));
    }

}