Kinetic

pyretic/examples/gardenlib.py

@@ -0,0 +1,7 @@
+
+from pyretic.kinetic.util.rewriting import *
+
+def redirectToGardenWall():
+    client_ips = [IP('10.0.0.1'), IP('10.0.0.2'),IP('10.0.0.4'),IP('10.0.0.5'),IP('10.0.0.6'),IP('10.0.0.7'),IP('10.0.0.8')]
+    rewrite_policy = rewriteDstIPAndMAC(client_ips, '10.0.0.3')
+    return rewrite_policy

pyretic/kinetic/SETUP

@@ -0,0 +1,10 @@
+=========================
+Set $KINETICPATH 
+=========================
+
+* Write command below in Linux command line:
+$ export KINETICPATH=$HOME/pyretic/pyretic/kinetic
+
+* Put this in "~/.profile" to make it execute every time to log in.
+Log off and log in again.
+

pyretic/kinetic/apps/auth.py

@@ -0,0 +1,93 @@
+
+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 *
+
+
+#####################################################################################################
+# * App launch
+#   - pyretic.py pyretic.kinetic.apps.auth
+#
+# * 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
+#
+# * Events to allow traffic "h1 ping h2" (in "~/pyretic/pyretic/kinetic" directory)
+#   - python json_sender.py -n auth -l True --flow="{srcip=10.0.0.1}" -a 127.0.0.1 -p 50001
+#   - python json_sender.py -n auth -l True --flow="{srcip=10.0.0.2}" -a 127.0.0.1 -p 50001
+#####################################################################################################
+
+
+class auth(DynamicPolicy):
+    def __init__(self):
+
+       ### DEFINE THE LPEC FUNCTION
+
+        def lpec(f):
+            return match(srcip=f['srcip'])
+
+        ## SET UP TRANSITION FUNCTIONS
+
+        @transition
+        def authenticated(self):
+            self.case(occurred(self.event),self.event)
+
+        @transition
+        def policy(self):
+            self.case(is_true(V('authenticated')),C(identity))
+            self.default(C(drop))
+
+        ### SET UP THE FSM DESCRIPTION
+
+        self.fsm_def = FSMDef( 
+            authenticated=FSMVar(type=BoolType(), 
+                            init=False, 
+                            trans=authenticated),
+            policy=FSMVar(type=Type(Policy,{drop,identity}),
+                          init=drop,
+                          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(auth,self).__init__(fsm_pol)
+
+
+def main():
+    pol = auth()
+
+    # For NuSMV
+    smv_str = fsm_def_to_smv_model(pol.fsm_def)
+    mc = ModelChecker(smv_str,'auth')  
+
+
+    ## Add specs 
+    mc.add_spec("FAIRNESS\n  authenticated;")
+
+    ### If authentication event is true, next policy state is 'allow'
+    mc.add_spec("SPEC AG (authenticated -> AX policy=policy_1)")
+
+    ### If authentication event is false, next policy state is 'drop'
+    mc.add_spec("SPEC AG (!authenticated -> AX policy=drop)")
+
+    ### It is always possible for the policy state to go to 'allow'
+    mc.add_spec("SPEC AG (EF policy=policy_1)")
+
+    ### Policy state is 'drop' until authentication is true. 
+    mc.add_spec("SPEC A [ policy=drop U authenticated ]")
+
+    mc.save_as_smv_file()
+    mc.verify()
+
+    # Ask deployment
+    ask_deploy()
+
+    return pol >> flood()

pyretic/kinetic/apps/auth_8021x.py

@@ -0,0 +1,94 @@
+
+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 *
+
+
+#####################################################################################################
+# * App launch
+#   - pyretic.py pyretic.kinetic.apps.auth_8021x
+#
+# * 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
+#
+# * Events to allow traffic "h1 ping h2" (in "~/pyretic/pyretic/kinetic" directory)
+#   - python json_sender.py -n authenticated_1x -l True --flow="{srcip=10.0.0.1}" -a 127.0.0.1 -p 50001
+#   - python json_sender.py -n authenticated_1x -l True --flow="{srcip=10.0.0.2}" -a 127.0.0.1 -p 50001
+#####################################################################################################
+
+
+class auth_8021x(DynamicPolicy):
+    def __init__(self):
+
+       ### DEFINE THE LPEC FUNCTION
+
+        def lpec(f):
+            return match(srcip=f['srcip'])
+
+        ## SET UP TRANSITION FUNCTIONS
+
+        @transition
+        def authenticated_1x(self):
+            self.case(occurred(self.event),self.event)
+
+        @transition
+        def policy(self):
+            self.case(is_true(V('authenticated_1x')),C(identity))
+            self.default(C(drop))
+
+        ### SET UP THE FSM DESCRIPTION
+
+        self.fsm_def = FSMDef( 
+            authenticated_1x=FSMVar(type=BoolType(), 
+                            init=False, 
+                            trans=authenticated_1x),
+            policy=FSMVar(type=Type(Policy,{drop,identity}),
+                          init=drop,
+                          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(auth_8021x,self).__init__(fsm_pol)
+
+
+def main():
+    pol = auth_8021x()
+
+    # For NuSMV
+    smv_str = fsm_def_to_smv_model(pol.fsm_def)
+    mc = ModelChecker(smv_str,'auth_8021x')  
+
+
+    ## Add specs 
+    mc.add_spec("FAIRNESS\n  authenticated_1x;")
+
+    ### If authentication event is true, next policy state is 'allow'
+    mc.add_spec("SPEC AG (authenticated_1x -> AX policy=policy_1)")
+
+    ### If authentication event is false, next policy state is 'drop'
+    mc.add_spec("SPEC AG (!authenticated_1x -> AX policy=drop)")
+
+    ### It is always possible for the policy state to go to 'allow'
+    mc.add_spec("SPEC AG (EF policy=policy_1)")
+
+    ### Policy state is 'drop' until authentication is true. 
+    mc.add_spec("SPEC A [ policy=drop U authenticated_1x ]")
+
+    mc.save_as_smv_file()
+    mc.verify()
+
+    # Ask deployment
+    ask_deploy()
+
+
+    return pol >> flood()

pyretic/kinetic/apps/auth_only.py

@@ -0,0 +1,90 @@
+
+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 *
+
+
+#####################################################################################################
+# * App launch
+#   - pyretic.py pyretic.kinetic.apps.auth
+#
+# * 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
+#
+# * Events to allow traffic "h1 ping h2" (in "~/pyretic/pyretic/kinetic" directory)
+#   - python json_sender.py -n auth -l True --flow="{srcip=10.0.0.1}" -a 127.0.0.1 -p 50001
+#   - python json_sender.py -n auth -l True --flow="{srcip=10.0.0.2}" -a 127.0.0.1 -p 50001
+#####################################################################################################
+
+
+class auth_only(DynamicPolicy):
+    def __init__(self):
+
+       ### DEFINE THE LPEC FUNCTION
+
+        def lpec(f):
+            return match(srcip=f['srcip'])
+
+        ## SET UP TRANSITION FUNCTIONS
+
+        @transition
+        def authenticated(self):
+            self.case(occurred(self.event),self.event)
+
+        @transition
+        def policy(self):
+            self.case(is_true(V('authenticated')),C(identity))
+            self.default(C(drop))
+
+        ### SET UP THE FSM DESCRIPTION
+
+        self.fsm_def = FSMDef( 
+            authenticated=FSMVar(type=BoolType(), 
+                            init=False, 
+                            trans=authenticated),
+            policy=FSMVar(type=Type(Policy,{drop,identity}),
+                          init=drop,
+                          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(auth_only,self).__init__(fsm_pol)
+
+
+def main():
+    pol = auth_only()
+
+    # For NuSMV
+    smv_str = fsm_def_to_smv_model(pol.fsm_def)
+    mc = ModelChecker(smv_str,'auth_only')  
+
+
+    ## Add specs 
+    mc.add_spec("FAIRNESS\n  authenticated;")
+
+    ### If authentication event is true, next policy state is 'allow'
+    mc.add_spec("SPEC AG (authenticated -> AX policy=policy_2)")
+
+    ### If authentication event is false, next policy state is 'drop'
+    mc.add_spec("SPEC AG (!authenticated -> AX policy=policy_1)")
+
+    ### It is always possible for the policy state to go to 'allow'
+    mc.add_spec("SPEC AG (EF policy=policy_2)")
+
+    ### Policy state is 'drop' until authentication is true. 
+    mc.add_spec("SPEC A [ policy=policy_1 U authenticated ]")
+
+    mc.save_as_smv_file()
+    mc.verify()
+
+    return pol

pyretic/kinetic/apps/auth_web.py

@@ -0,0 +1,93 @@
+
+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 *
+
+
+#####################################################################################################
+# * App launch
+#   - pyretic.py pyretic.kinetic.apps.auth_web
+#
+# * 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
+#
+# * Events to allow traffic "h1 ping h2" (in "~/pyretic/pyretic/kinetic" directory)
+#   - python json_sender.py -n authenticated_web -l True --flow="{srcip=10.0.0.1}" -a 127.0.0.1 -p 50001
+#   - python json_sender.py -n authenticated_web -l True --flow="{srcip=10.0.0.2}" -a 127.0.0.1 -p 50001
+#####################################################################################################
+
+
+class auth_web(DynamicPolicy):
+    def __init__(self):
+
+       ### DEFINE THE LPEC FUNCTION
+
+        def lpec(f):
+            return match(srcip=f['srcip'])
+
+        ## SET UP TRANSITION FUNCTIONS
+
+        @transition
+        def authenticated_web(self):
+            self.case(occurred(self.event),self.event)
+
+        @transition
+        def policy(self):
+            self.case(is_true(V('authenticated_web')),C(identity))
+            self.default(C(drop))
+
+        ### SET UP THE FSM DESCRIPTION
+
+        self.fsm_def = FSMDef( 
+            authenticated_web=FSMVar(type=BoolType(), 
+                            init=False, 
+                            trans=authenticated_web),
+            policy=FSMVar(type=Type(Policy,{drop,identity}),
+                          init=drop,
+                          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(auth_web,self).__init__(fsm_pol)
+
+
+def main():
+    pol = auth_web()
+
+    # For NuSMV
+    smv_str = fsm_def_to_smv_model(pol.fsm_def)
+    mc = ModelChecker(smv_str,'auth_web')  
+
+
+    ## Add specs 
+    mc.add_spec("FAIRNESS\n  authenticated_web;")
+
+    ### If authentication event is true, next policy state is 'allow'
+    mc.add_spec("SPEC AG (authenticated_web -> AX policy=policy_1)")
+
+    ### If authentication event is false, next policy state is 'drop'
+    mc.add_spec("SPEC AG (!authenticated_web -> AX policy=drop)")
+
+    ### It is always possible for the policy state to go to 'allow'
+    mc.add_spec("SPEC AG (EF policy=policy_1)")
+
+    ### Policy state is 'drop' until authentication is true. 
+    mc.add_spec("SPEC A [ policy=drop U authenticated_web ]")
+
+    mc.save_as_smv_file()
+    mc.verify()
+
+    # Ask deployment
+    ask_deploy()
+
+    return pol >> flood()