initial upload for all code files

ROBINADC · Feb 17, 2021 · fa8447a · fa8447a
commit fa8447a
Show file tree

Hide file tree

Showing 11 changed files with 939 additions and 0 deletions.
diff --git a/case-1-misc.maude b/case-1-misc.maude
@@ -0,0 +1,38 @@
+sload modules/output
+
+mod CASE-1-MISC is
+    pr OUTPUT .
+
+    op ns : -> Set{Node} .
+    eq ns = node('a), node('fw), node('sw), node('b), node('c) .
+
+    op es : -> Set{Edge} .
+    eq es = edge(node('a), node('fw)), edge(node('fw), node('sw)), edge(node('sw), node('b)), edge(node('sw), node('c)) .
+
+    op t : -> Topology .
+    eq t = topology(ns, es) .
+
+    op rn : -> FlowTableNetwork .
+    eq rn = ftn(t, rf) .
+
+    op path : -> Path .
+    eq path = node('a) ; node('fw) ; node('sw) ; node('b) . --- no path existence and correctness guarantee
+
+    op rf : -> RuleFunction .
+    eq rf(node('a)) = forward('fw) .
+    eq rf(node('fw)) = (if ('a -> 'b) then drop else skip) ; forward('sw) . --- reformat the rules in firewall from "if ('a -> 'b) then drop else forward('sw)"
+    eq rf(node('sw)) = (if ('a -> 'c) then upDst('b) else skip) ; (if ('a -> 'b) then forward('b) else skip) ; drop . --- use drop to prevent packet stranded
+    eq rf(N:Node) = skip [owise] . --- all other nodes have rule "skip" representing no rule
+
+    op pks : -> List{Packet} .
+    eq pks = packet('a, 'c, "SSH", 'a) .
+
+    op target-pk : -> Packet .
+    eq target-pk = packet('a, 'b, "SSH", 'b) .
+endm
+
+*** output
+
+--- search out[rn](path, pks) =>* P:Packet such that P:Packet == target-pk .
+--- search out[rn](path, pks) =>* P:Packet such that P:Packet == packet('a, 'c, "SSH", 'fw) . --- packet does not stop
+--- rew out[rn](path, pks) .
diff --git a/case-1.maude b/case-1.maude
@@ -0,0 +1,79 @@
+sload modules/analysis
+
+--- A cognitive case
+--- From (Zhao et al, 2018)
+mod CASE-1 is
+    pr ANALYSIS .
+
+    op ns : -> Set{Node} .
+    eq ns = node('a), node('fw), node('sw), node('b), node('c) .
+
+    op es : -> Set{Edge} .
+    eq es = edge(node('a), node('fw)), edge(node('fw), node('sw)), edge(node('sw), node('b)), edge(node('sw), node('c)) .
+
+    op t : -> Topology .
+    eq t = topology(ns, es) .
+
+    op rf : -> RuleFunction .
+    eq rf(node('a)) = forward('fw) .
+    eq rf(node('fw)) = (if ('a -> 'b) then drop else skip) ; forward('sw) . --- reformat the rules in firewall from "if ('a -> 'b) then drop else forward('sw)"
+    eq rf(node('sw)) = (if ('a -> 'c) then upDst('b) else skip) ; (if ('a -> 'b) then forward('b) else skip) ; drop . --- use drop to prevent packet stranded
+    eq rf(N:Node) = skip [owise] . --- all other nodes have rule "skip" representing no rule
+
+    op pk : -> Packet .
+    eq pk = packet('a, 'c, "SSH", 'a) .
+
+    op target-pk : -> Packet .
+    eq target-pk = packet('a, 'b, "SSH", 'b) .
+endm
+
+
+*** analysis
+
+--- NETWORK
+
+--- rew [t, rf](pk) .
+--- search [t, rf](pk) =>* P:Packet such that P:Packet == target-pk .
+--- show path labels 12 .
+
+--- rew [t, rf](fault-packet) .
+
+--- rew [t, rf](packet('a, 'b, "SSH", 'a)) .
+--- search [t, rf](packet('a, 'b, "SSH", 'a)) =>* P:Packet such that P:Packet == null-packet .
+--- show path labels 8 .
+
+--- rew [t, rf](packet('c, 'd, "SSH", 'sw)) .
+--- rew [1] [t, rf](packet('a, 'b, "SSH", 'fw)) .
+
+--- NETWORK-PREDS
+
+--- red [t, rf](packet('a, 'b, "SSH", 'a)) |= conflict(t, rf) . --- middle state, false
+--- red packet('a, 'b, "SSH", 'b) |= conflict(t, rf) . --- true
+--- red null-packet |= conflict(t, rf) . --- false
+
+--- red packet('a, 'b, "SSH", 'b) violates ns with rf .
+--- red packet('a, 'b, "SSH", 'b) violates (node('a), node('sw), node('b), node('c)) with rf .
+--- red null-packet violates ns with rf .
+
+--- red packet('a, 'b, "SSH", 'b) violates node('a) with rf . --- false
+--- red packet('a, 'b, "SSH", 'b) violates node('fw) with rf . --- true
+--- red packet('a, 'b, "SSH", 'b) violates node('fw-dummy) with rf . --- false
+
+--- red packet('a, 'b, "SSH", 'b) violates -/-> 'b ; upDst('a) .
+--- red packet('a, 'b, "SSH", 'b) violates upDst('a) .
+--- red packet('a, 'b, "SSH", 'b) violates upDst('a) ; skip ; 'a -/-> . --- true
+--- red packet('a, 'b, "SSH", 'b) violates 'b -/-> ; 'c -/-> . --- false
+--- red packet('a, 'b, "SSH", 'b) violates ["UDP"]-/-> ; 'a -/-> ; 'c -/-> . --- true
+--- red packet('a, 'b, "SSH", 'b) violates upDst('c) ; drop . --- false
+
+--- red packet('a, 'b, "SSH", 'b) violates 'a -/->  . --- true
+--- red packet('a, 'b, "UDP", 'b) violates ["UDP"]-/-> . --- true
+--- red null-packet violates 'a -/-> 'c . --- false
+--- red null-packet violates ["UDP"]-/-> . --- false
+
+--- NETWORK-CHECK
+
+--- red modelCheck(
+---     [t, rf](pk),
+---     [] ~ conflict(t, rf)
+--- ) .
diff --git a/case-2.maude b/case-2.maude
@@ -0,0 +1,47 @@
+sload modules/analysis
+
+--- A moderate case with standalone firewalls
+mod CASE-2 is
+    pr ANALYSIS .
+
+    op ns : -> Set{Node} .
+    eq ns = node('a), node('b), node('y), node('z), node('sw-1), node('sw-2), node('sw-m), node('fw-1), node('fw-2) .
+
+    op es : -> Set{Edge} .
+    eq es = 
+        edge(node('a), node('sw-1)), edge(node('b), node('sw-1)), edge(node('sw-1), node('fw-1)), 
+        edge(node('fw-1), node('sw-m)), edge(node('sw-m), node('fw-2)), 
+        edge(node('fw-2), node('sw-2)), edge(node('sw-2), node('y)), edge(node('sw-2), node('z)) .
+
+    op t : -> Topology .
+    eq t = topology(ns, es) .
+
+    op rf : -> RuleFunction .
+    eq rf(node('fw-1)) = ('a -/->) ; forward('sw-m) .
+    eq rf(node('fw-2)) = (-/-> 'z) ; forward('sw-2) .
+    --- eq rf(node('fw-2)) = (-/-> 'z) ; (-/-> 'y) ; forward('sw-2) . --- If we also block the packet sent to 'y ...
+    eq rf(node('sw-m)) = forward('fw-2) .
+
+    eq rf(node('a)) = forward('sw-1) .
+    eq rf(node('sw-1)) = (if 'a -> 'z then forward('b)) ; forward('fw-1) .
+    eq rf(node('b)) = (if 'a -> 'z then upSrc('b) ; upDst('y)) ; forward('sw-1) .
+    eq rf(node('sw-2)) = (if assertDst('z) then forward('z)) ; (if assertDst('y) then forward('y)) ; drop .
+    eq rf(node('y)) = (if 'b -> 'y then upSrc('a) ; upDst('z)) ; forward('sw-2) .
+
+    eq rf(N:Node) = skip [owise] .
+
+    op pk : -> Packet .
+    eq pk = packet('a, 'z, "SSH", 'a) .
+
+endm
+
+--- rew [t, rf](packet('a, 'z, "SSH", 'a)) .
+
+--- search [t, rf](packet('a, 'z, "SSH", 'a)) =>* P:Packet such that P:Packet == packet('a, 'z, "SSH", 'z) .
+
+--- red modelCheck(
+---     [t, rf](pk),
+---     [] ~ conflict(t, rf)
+--- ) .
+
+
diff --git a/case-3.maude b/case-3.maude
@@ -0,0 +1,34 @@
+sload modules/analysis
+
+--- A case with centralized controller
+--- From (Zhang et al, 2017)
+mod CASE-3 is
+    pr ANALYSIS-V2 .
+
+    op ns : -> Set{Node} .
+    eq ns = node('a), node('b), node('c), node('d), node('sw-1), node('sw-2), node('sw-3) .
+
+    op es : -> Set{Edge} .
+    eq es = 
+        edge(node('a), node('sw-1)), edge(node('d), node('sw-1)),
+        edge(node('sw-1), node('sw-2)), edge(node('sw-2), node('sw-3)), 
+        edge(node('c), node('sw-3)), edge(node('b), node('sw-3)) .
+
+    op t : -> Topology .
+    eq t = topology(ns, es) .
+
+    op rf : -> RuleFunction .
+    eq rf(node('sw-1)) = ('a -/-> 'c) ; (if 'a -> 'b then upSrc('d)) ; forward('sw-2) .
+    eq rf(node('sw-2)) = ('a -/-> 'c) ; (if 'd -> 'b then upDst('c)) ; forward('sw-3) .
+    eq rf(node('sw-3)) = ('a -/-> 'c) ; (if 'd -> 'c then upSrc('a)) ; forward('c) . --- add upSrc('a) to correspond to the Theorem 4.2
+    eq rf(node('a)) = forward('sw-1) .
+
+    eq rf(N:Node) = skip [owise] .
+endm
+
+--- rew [t, rf](packet('a, 'b, "SSH", 'a)) . --- initial destination is set to 'b
+
+--- red modelCheck(
+---     [t, rf](packet('a, 'b, "SSH", 'a)),
+---     [] ~ conflict(t, rf)
+--- ) .
diff --git a/debug.maude b/debug.maude
@@ -0,0 +1,116 @@
+sload modules/output
+
+mod DEBUG is
+    pr OUTPUT .
+
+    op initial-nodes : -> Set{Node} .
+    eq initial-nodes = node('a), node('fw), node('sw), node('b), node('c) .
+
+    op initial-edges : -> Set{Edge} .
+    eq initial-edges = edge(node('a), node('fw)), edge(node('fw), node('sw)), edge(node('sw), node('b)), edge(node('sw), node('c)) .
+
+    op initial-topology : -> Topology .
+    eq initial-topology = topology(initial-nodes, initial-edges) .
+
+    op rf : -> RuleFunction .
+    eq rf(node('a)) = forward('fw) .
+    eq rf(node('fw)) = ('a -/-> 'b) ; (["UDP"]-/->) ; forward('sw) .
+    eq rf(node('sw)) = (if ('a -> 'c) then upDst('b) else skip) ; (if ('a -> 'b) then forward('b) else drop) .
+    eq rf(N:Node) = skip [owise] . --- need to specify no rule in other nodes
+endm
+
+*** base.maude
+--- red 'a == 'b .
+--- red (node('a), node('b), node('c)) \ node('b) .
+
+*** packet.maude
+--- red in PACKET-LIST : occurs(packet('a, 'fw, "SSH", 'b), (packet('a, 'fw, "SSH", 'b) packet('a, 'fw, "SSH", 'c))) .
+--- red in PACKET-LIST : getDst(packet('a, 'fw, "SSH", 'b)) .
+
+*** topology.maude
+--- red in NODE-SET : node('a) in (node('a), node('b)) .
+--- red in EDGE-SET : edge(node('fw), node('a)) in (edge(node('a), node('fw)), edge(node('fw), node('sw))) .
+--- red node('b) isEndpointOf edge(node('a), node('b)) .
+--- red adjacent[getEdgeSet(initial-topology)](node('sw)) .
+--- red node('a) in initial-topology .
+--- red edge(node('a), node('fw)) in initial-topology .
+--- red edge(node('fw), node('a)) in initial-topology .
+
+--- red node('a) :: FwNode .
+--- red node('fw1) :: FwNode .
+
+*** semantics.maude
+--- BOOL-EXPR
+--- red assertSrc('a)(packet('a, 'b, "UDP", 'c)) .
+--- red assertTyp("SSH")(packet('a, 'b, "SSH", 'c)) .
+--- red assertTyp("SSH")(packet('a, 'b, "UDP", 'c)) .
+--- red (assertSrc('a) and assertDst('b))(packet('a, 'b, "UDP", 'c)) .
+--- red (assertSrc('a) and assertDst('b) and assertTyp("TCP"))(packet('a, 'b, "UDP", 'c)) .
+--- red (assertSrc('t) or assertDst('b))(packet('a, 'b, "UDP", 'c)) .
+--- red ('a -> 'b)(packet('a, 'b, "UDP", 'c)) .
+--- red skip + skip + skip .
+--- red skip + error == error + skip . --- [TBD]
+
+--- RULE
+--- rew initial-topology |- state(upSrc('a), packet('b, 'c, "SSH", 'd), 'c) .
+--- rew initial-topology |- state(forward('a), null-packet, 'a) .
+--- rew initial-topology |- state(forward('a), fault-packet, 'a) .
+--- rew initial-topology |- state(skip, packet('a, 'b, "SSH", 'a), 'a) .
+--- rew initial-topology |- state(drop, packet('a, 'b, "SSH", 'a), 'a) .
+--- rew initial-topology |- state(error, packet('a, 'b, "SSH", 'a), 'a) .
+
+--- rew initial-topology |- state(filter(assertTyp("SSH")), packet('a, 'b, "SSH", 'a), 'a) .
+--- rew initial-topology |- state(filter(assertSrc('t)), packet('a, 'b, "SSH", 'a), 'a) .
+--- rew initial-topology |- state(upSrc('d), packet('a, 'b, "SSH", 'c), 'c) .
+--- rew initial-topology |- state(upDst('d), packet('a, 'b, "SSH", 'c), 'c) .
+--- rew initial-topology |- state(forward('fw), packet('a, 'b, "SSH", 'a), 'a) .
+--- rew initial-topology |- state(forward('sw), packet('a, 'b, "SSH", 'a), 'a) .
+
+--- rew initial-topology |- state(upSrc('t); forward('fw), packet('a, 'b, "SSH", 'a), 'a) .
+--- rew initial-topology |- state(upSrc('t) + upSrc('x), packet('a, 'b, "SSH", 'a), 'a) .
+--- rew initial-topology |- state(if assertTyp("UDP") then drop else forward('fw), packet('a, 'b, "UDP", 'a), 'a) .
+--- rew initial-topology |- state(if assertTyp("UDP") then drop else forward('fw), packet('a, 'b, "TCP", 'a), 'a) .
+--- rew initial-topology |- state(while assertSrc('t) do forward('fw) | 3, packet('a, 'b, "TCP", 'a), 'a) .
+--- rew initial-topology |- state(while assertLoc('a) do forward('fw) | 3, packet('a, 'b, "TCP", 'a), 'a) .
+--- search [1] initial-topology |- state(while assertLoc('a) do forward('fw) | 3, packet('a, 'b, "TCP", 'a), 'a) =>! P:Packet
+--- such that P:Packet == packet('a, 'b, "TCP", 'fw) .
+
+--- SeqRule
+--- red skip ; drop :: SeqRule .
+--- red skip ; skip ; skip :: SeqRule . --- true
+--- red skip + (skip ; skip) :: SeqRule . --- false
+
+--- BlockRule
+--- red 'a -/-> :: BlockRule .
+--- red if assertTyp("UDP") then drop else skip :: BlockRule .
+--- red if 'x -> 'y then drop :: BlockRule .
+--- rew initial-topology |- state('a -/-> 'c, packet('a, 'c, "SSH", 'a), 'a) .
+--- rew initial-topology |- state('a -/->, packet('a, 'c, "SSH", 'a), 'a) .
+--- rew initial-topology |- state(-/-> 'b, packet('a, 'c, "SSH", 'a), 'a) .
+--- rew initial-topology |- state(["UDP"]-/->, packet('a, 'c, "UDP", 'a), 'a) .
+
+--- SEMANTICS
+--- rew $sem[forward('fw); initial-topology, 'a](packet('a,'b,"SSH",'a)) .
+--- rew sem[forward('fw); initial-topology, 'a](packet('a,'b,"SSH",'a) packet('a,'c,"TCP",'a)) .
+
+
+*** output.maude
+
+--- red getTopology(ftn(initial-topology, rf)) .
+--- red node('a) ; nil .
+--- red node('a) ; node('fw) ; node('sw) ; node('b) :: Path .
+
+--- A full path
+--- rew out[ftn(initial-topology, rf)](node('a) ; node('fw) ; node('sw) ; node('b), packet('a, 'c, "SSH", 'a)) .
+--- search out[ftn(initial-topology, rf)](node('a) ; node('fw) ; node('sw) ; node('b), packet('a, 'c, "SSH", 'a)) =>* 
+--- P:Packet PL:List{Packet} such that P:Packet == packet('a, 'b, "SSH", 'b) .
+
+--- Test Choice
+--- search sem[forward('b) + forward('c) + forward('d) ; initial-topology , 'sw](packet('t, 'tt, "SSH", 'sw)) =>*
+--- P:Packet such that P:Packet == packet('t, 'tt, "SSH", 'c) .
+
+--- Case that the path is formed of one node
+--- rew out[ftn(initial-topology, rf)](node('a), packet('a, 'c, "SSH", 'a)) .
+
+--- Case with multiple packets
+--- rew out[ftn(initial-topology, rf)](node('a) ; node('fw) ; node('sw) ; node('b), packet('a, 'c, "SSH", 'a) packet('a, 'c, "UDP", 'a)) .
diff --git a/interface.maude b/interface.maude
@@ -0,0 +1,17 @@
+sload modules/analysis
+
+mod ICASE is
+    pr ANALYSIS .
+
+    op ns : -> Set{Node} .
+    op es : -> Set{Edge} .
+    op t : -> Topology .
+    eq t = topology(ns, es) .
+    op rf : -> RuleFunction .
+    op pk : -> Packet .
+endm
+
+red modelCheck(
+    [t, rf](pk),
+    [] ~ conflict(t, rf)
+) .