-
Notifications
You must be signed in to change notification settings - Fork 9
/
Copy pathgardenwall.py
137 lines (106 loc) · 4.34 KB
/
gardenwall.py
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
#!/usr/bin/env python
'''
Coursera:
- Software Defined Networking (SDN) course
-- Module 8 Programming Assignment
Professor: Nick Feamster
Teaching Assistant: Arpit Gupta
'''
from pyretic.lib.corelib import *
from pyretic.lib.std import *
from pyretic.kinetic.fsm_policy import *
from pyretic.kinetic.drivers.json_event import JSONEvent
from pyretic.kinetic.smv.model_checker import *
from pyretic.kinetic.util.rewriting import *
from pyretic.kinetic.apps.mac_learner import *
#####################################################################################################
# Author: Hyojoon Kim
# * App launch
# - pyretic.py pyretic.kinetic.apps.gardenwall
#
# * Mininet Generation (in "~/pyretic/pyretic/kinetic" directory)
# - sudo mn --controller=remote,ip=127.0.0.1 --mac --arp --switch ovsk --link=tc --topo=single,3
#
# * Start ping from h1 to h2
# - mininet> h1 ping h2
#
# * Send Event to block traffic "h1 ping h2" (in "~/pyretic/pyretic/kinetic" directory)
# - python json_sender.py -n infected -l True --flow="{srcip=10.0.0.1}" -a 127.0.0.1 -p 50001
#
# * Now, make h1's flow not be affected by IDS infection event(in "~/pyretic/pyretic/kinetic" directory)
# h1's traffic will be forwarded to 10.0.0.3.
# - python json_sender.py -n exempt -l True --flow="{srcip=10.0.0.1}" -a 127.0.0.1 -p 50001
#
# * Events to now allfow traffic again (in "~/pyretic/pyretic/kinetic" directory)
# - python json_sender.py -n infected -l False --flow="{srcip=10.0.0.1}" -a 127.0.0.1 -p 50001
#####################################################################################################
class gardenwall(DynamicPolicy):
def __init__(self):
# Garden Wall
def redirectToGardenWall():
client_ips = [IP('10.0.0.1'), IP('10.0.0.2')]
rewrite_policy = rewriteDstIPAndMAC(client_ips, '10.0.0.3')
return rewrite_policy
### DEFINE THE LPEC FUNCTION
def lpec(f):
# Your logic here
# return match =
return match(srcip=f['srcip'])
## SET UP TRANSITION FUNCTIONS
@transition
def exempt(self):
self.case(occurred(self.event),self.event)
@transition
def infected(self):
self.case(occurred(self.event),self.event)
@transition
def policy(self):
# If exempt, redirect to gardenwall.
# - rewrite dstip to 10.0.0.3
self.case(test_and_true(V('exempt'),V('infected')), C(redirectToGardenWall()))
# If infected, drop
# Your logic here
self.case(is_true(V('infected')), C(drop))
# Else, identity
self.default(C(identity))
### SET UP THE FSM DESCRIPTION
self.fsm_def = FSMDef(
infected=FSMVar(type=BoolType(),
init=False,
trans=infected),
# Your logic here
# exempt =
exempt=FSMVar(type=BoolType(),
init=False,
trans=exempt),
# policy =
policy=FSMVar(type=Type(Policy,{drop, identity, redirectToGardenWall()}),
init=identity,
trans=policy)
)
### SET UP POLICY AND EVENT STREAMS
fsm_pol = FSMPolicy(lpec,self.fsm_def)
json_event = JSONEvent()
json_event.register_callback(fsm_pol.event_handler)
super(gardenwall,self).__init__(fsm_pol)
def main():
pol = gardenwall()
# For NuSMV
smv_str = fsm_def_to_smv_model(pol.fsm_def)
mc = ModelChecker(smv_str,'gardenwall')
## Add specs
mc.add_spec("FAIRNESS\n infected;")
mc.add_spec("FAIRNESS\n exempt;")
# Now, traffic is dropped only when exempt is false and infected is true
mc.add_spec("SPEC AG (infected & !exempt -> AX policy=policy_2)")
# If exempt is true, next policy state to redirect to gardenwall, even if infected
mc.add_spec("SPEC AG (infected & exempt -> AX policy=policy_1)")
# If infected is false, next policy state is always 'allow'
mc.add_spec("SPEC AG (!infected -> AX policy=policy_3)")
### Policy state is 'allow' until infected is true.
mc.add_spec("SPEC A [ policy=policy_3 U infected ]")
# Save NuSMV file
mc.save_as_smv_file()
# Verify
mc.verify()
return pol >> mac_learner()