Adding connection to symblic presentation, with relevant optimzations (…

…#100)

pkg/model/dfw/category.go

@@ -120,13 +120,13 @@ func (c *CategorySpec) analyzeCategory(src, dst *endpoints.VM, isIngress bool,
 		if rule.processedRuleCapturesPair(src, dst) /*rule.capturesPair(src, dst, isIngress)*/ {
 			switch rule.Action {
 			case actionAllow:
-				addedAllowedConns := rule.conn.Subtract(deniedConns).Subtract(jumpToAppConns)
+				addedAllowedConns := rule.Conn.Subtract(deniedConns).Subtract(jumpToAppConns)
 				allowedConns = allowedConns.Union(addedAllowedConns)
 			case actionDeny:
-				addedDeniedConns := rule.conn.Subtract(allowedConns).Subtract(jumpToAppConns)
+				addedDeniedConns := rule.Conn.Subtract(allowedConns).Subtract(jumpToAppConns)
 				deniedConns = deniedConns.Union(addedDeniedConns)
 			case actionJumpToApp:
-				addedJumpToAppConns := rule.conn.Subtract(allowedConns).Subtract(deniedConns)
+				addedJumpToAppConns := rule.Conn.Subtract(allowedConns).Subtract(deniedConns)
 				jumpToAppConns = jumpToAppConns.Union(addedJumpToAppConns)
 			}
 		}
@@ -190,7 +190,7 @@ func (c *CategorySpec) addRule(src, dst []*endpoints.VM, srcGroups, dstGroups, s
 		IsAllSrcGroups:     isAllSrcGroup,
 		DstGroups:          dstGroups,
 		IsAllDstGroups:     isAllDstGroup,
-		conn:               conn,
+		Conn:               conn,
 		Action:             actionFromString(action),
 		direction:          direction,
 		ruleID:             ruleID,

pkg/model/dfw/dfw.go

@@ -142,7 +142,7 @@ func (d *DFW) AddRule(src, dst []*endpoints.VM, srcGroups, dstGroups, scopeGroup
 	newRule := &FwRule{
 		srcVMs: src,
 		dstVMs: dst,
-		conn:   netset.All(), // todo: change
+		Conn:   netset.All(), // todo: change
 		Action: actionFromString(actionStr),
 	}
 	categoryObj.rules = append(categoryObj.rules, newRule)

pkg/model/dfw/rule.go

@@ -67,7 +67,7 @@ type FwRule struct {
 	IsAllDstGroups bool
 	// Scope implies additional condition on any Src and any Dst; will be added in one of the last stages
 	ScopeGroups        []*collector.Group
-	conn               *netset.TransportSet
+	Conn               *netset.TransportSet
 	Action             RuleAction
 	direction          string //	"IN","OUT",	"IN_OUT"
 	origRuleObj        *collector.Rule
@@ -86,7 +86,7 @@ func (f *FwRule) effectiveRules() (inbound, outbound *FwRule) {
 		logging.Debugf("rule %d has no effective inbound/outbound component, since its scope component is empty", f.ruleID)
 		return nil, nil
 	}
-	if f.conn.IsEmpty() {
+	if f.Conn.IsEmpty() {
 		logging.Debugf("rule %d has no effective inbound/outbound component, since its traffic attributes are empty", f.ruleID)
 		return nil, nil
 	}
@@ -122,7 +122,7 @@ func (f *FwRule) getInboundRule() *FwRule {
 		IsAllSrcGroups: f.IsAllSrcGroups,
 		IsAllDstGroups: f.IsAllDstGroups,
 		ScopeGroups:    f.ScopeGroups,
-		conn:           f.conn,
+		Conn:           f.Conn,
 		Action:         f.Action,
 		direction:      string(nsx.RuleDirectionIN),
 		origRuleObj:    f.origRuleObj,
@@ -161,7 +161,7 @@ func (f *FwRule) getOutboundRule() *FwRule {
 		IsAllSrcGroups: f.IsAllSrcGroups,
 		IsAllDstGroups: f.IsAllDstGroups,
 		ScopeGroups:    f.ScopeGroups,
-		conn:           f.conn,
+		Conn:           f.Conn,
 		Action:         f.Action,
 		direction:      string(nsx.RuleDirectionOUT),
 		origRuleObj:    f.origRuleObj,
@@ -200,12 +200,12 @@ func vmsString(vms []*endpoints.VM) string {
 // groups are interpreted to VM members in this representation
 func (f *FwRule) string() string {
 	return fmt.Sprintf("ruleID: %d, src: %s, dst: %s, conn: %s, action: %s, direction: %s, scope: %s, sec-policy: %s",
-		f.ruleID, vmsString(f.srcVMs), vmsString(f.dstVMs), f.conn.String(), string(f.Action), f.direction, vmsString(f.scope), f.secPolicyName)
+		f.ruleID, vmsString(f.srcVMs), vmsString(f.dstVMs), f.Conn.String(), string(f.Action), f.direction, vmsString(f.scope), f.secPolicyName)
 }
 
 func (f *FwRule) effectiveRuleStr() string {
 	return fmt.Sprintf("ruleID: %d, src: %s, dst: %s, conn: %s, action: %s, direction: %s, sec-policy: %s",
-		f.ruleID, vmsString(f.srcVMs), vmsString(f.dstVMs), f.conn.String(), string(f.Action), f.direction, f.secPolicyName)
+		f.ruleID, vmsString(f.srcVMs), vmsString(f.dstVMs), f.Conn.String(), string(f.Action), f.direction, f.secPolicyName)
 }
 
 func getDefaultRuleScope(r *collector.FirewallRule) string {
@@ -253,7 +253,7 @@ func getRulesFormattedHeaderLine() string {
 		"src",
 		"dst",
 		"conn",
-		"Action",
+		"action",
 		"direction",
 		"scope",
 		"sec-policy",

pkg/symbolicexpr/conjunction.go

@@ -18,6 +18,9 @@ func (c *Conjunction) string() string {
 }
 
 func (c *Conjunction) add(atomic *atomicTerm) *Conjunction {
+	if c.contains(atomic) {
+		return c
+	}
 	res := append(*c, atomic)
 	return &res
 }
@@ -35,7 +38,26 @@ func (c *Conjunction) isTautology() bool {
 	return false
 }
 
-// checks whether the Conjunction is empty: either syntactically, or contains an atomicTerm and its negation
+func (c *Conjunction) removeTautology() Conjunction {
+	if len(*c) <= 1 {
+		return *c
+	}
+	newC := Conjunction{}
+	tautologyRemoved := false
+	for _, atom := range *c {
+		if !atom.isTautology() {
+			newC = append(newC, atom)
+		} else {
+			tautologyRemoved = true
+		}
+	}
+	if len(newC) == 0 && tautologyRemoved {
+		return Conjunction{tautology{}}
+	}
+	return newC
+}
+
+// checks whether the conjunction is empty: either syntactically, or contains an atomicTerm and its negation
 func (c *Conjunction) isEmptySet() bool {
 	if len(*c) == 0 {
 		return true
@@ -51,3 +73,30 @@ func (c *Conjunction) isEmptySet() bool {
 	}
 	return false
 }
+
+// checks whether conjunction other is disjoint to conjunction c
+// this is the case if there's a term in c and its contradiction in other
+// we will later add hints
+func (c *Conjunction) disjoint(other *Conjunction) bool {
+	if len(*c) == 0 || len(*other) == 0 {
+		return false
+	}
+	if other.isTautology() || c.isTautology() {
+		return false
+	}
+	for _, atomicTerm := range *other {
+		if c.contains(atomicTerm.negate()) {
+			return true
+		}
+	}
+	return false
+}
+
+func (c *Conjunction) contains(atom atomic) bool {
+	for _, atomicTerm := range *c {
+		if atomicTerm.string() == (atom).string() {
+			return true
+		}
+	}
+	return false
+}

pkg/symbolicexpr/model.go

@@ -1,5 +1,7 @@
 package symbolicexpr
 
+import "github.com/np-guard/models/pkg/netset"
+
 // the package implements a symbolic expression of enabled paths from symbolic src to symbolic dst, expressed as CNF
 
 // Virtual machines' properties used in atomic group expr, e.g. group = Gryffindor, tag = "backend"
@@ -37,9 +39,9 @@ type Conjunction []atomic
 
 // SymbolicPath all path from a Src VM satisfying Src to Dst VM satisfying Dst
 type SymbolicPath struct {
-	Src Conjunction
-	Dst Conjunction
-	// ToDo: add Conn
+	Src  Conjunction
+	Dst  Conjunction
+	Conn *netset.TransportSet
 }
 
 type SymbolicPaths []*SymbolicPath

pkg/symbolicexpr/symbolicPath.go

@@ -8,12 +8,18 @@ import (
 )
 
 func (path *SymbolicPath) string() string {
-	return path.Src.string() + " to " + path.Dst.string()
+	return path.Conn.String() + " from " + path.Src.string() + " to " + path.Dst.string()
 }
 
 // if the source or destination is empty then so is the entire path
 func (path *SymbolicPath) isEmpty() bool {
-	return path.Src.isEmptySet() || path.Dst.isEmptySet()
+	return path.Conn.IsEmpty() || path.Src.isEmptySet() || path.Dst.isEmptySet()
+}
+
+// checks whether paths are disjoint. This is the case when one of the path's components (src, dst, conn) are disjoint
+func (path *SymbolicPath) disJointPaths(other *SymbolicPath) bool {
+	return path.Conn.Intersect(other.Conn).IsEmpty() || path.Src.disjoint(&other.Src) ||
+		path.Dst.disjoint(&other.Dst)
 }
 
 func (paths *SymbolicPaths) String() string {
@@ -37,6 +43,17 @@ func (paths *SymbolicPaths) removeEmpty() *SymbolicPaths {
 	return &newPaths
 }
 
+func (paths *SymbolicPaths) removeTautology() *SymbolicPaths {
+	newPaths := SymbolicPaths{}
+	for _, path := range *paths {
+		if !path.isEmpty() {
+			newPath := &SymbolicPath{Src: path.Src.removeTautology(), Dst: path.Dst.removeTautology(), Conn: path.Conn}
+			newPaths = append(newPaths, newPath)
+		}
+	}
+	return &newPaths
+}
+
 // ComputeAllowGivenDenies converts a set of symbolic allow and deny paths (given as type SymbolicPaths)
 // the resulting allow paths in SymbolicPaths
 // The motivation here is to unroll allow rule given higher priority deny rule
@@ -51,9 +68,19 @@ func ComputeAllowGivenDenies(allowPaths, denyPaths *SymbolicPaths) *SymbolicPath
 	}
 	res := SymbolicPaths{}
 	for _, allowPath := range *allowPaths {
+		relevantDenyPaths := SymbolicPaths{}
+		for _, denyPath := range *denyPaths {
+			if !allowPath.disJointPaths(denyPath) {
+				relevantDenyPaths = append(relevantDenyPaths, denyPath)
+			}
+		}
+		if len(relevantDenyPaths) == 0 { // the denys paths are not relevant for this allow. This allow path remains as is
+			res = append(res, allowPath)
+			continue
+		}
 		var computedAllowPaths, newComputedAllowPaths SymbolicPaths
 		newComputedAllowPaths = SymbolicPaths{allowPath}
-		for _, denyPath := range *denyPaths {
+		for _, denyPath := range relevantDenyPaths {
 			computedAllowPaths = newComputedAllowPaths
 			newComputedAllowPaths = SymbolicPaths{}
 			for _, computedAllow := range computedAllowPaths {
@@ -71,52 +98,51 @@ func ComputeAllowGivenDenies(allowPaths, denyPaths *SymbolicPaths) *SymbolicPath
 // algorithm described in README of symbolicexpr
 func computeAllowGivenAllowHigherDeny(allowPath, denyPath SymbolicPath) *SymbolicPaths {
 	resAllowPaths := SymbolicPaths{}
-	// in case deny path is open from both ends - empty set of allow paths, as will be the result
-	// assumption: if more than one term, then none is tautology
 	for _, srcAtom := range denyPath.Src {
 		if !srcAtom.isTautology() {
 			srcAtomNegate := srcAtom.negate().(atomicTerm)
-			if allowPath.Src.isTautology() {
-				resAllowPaths = append(resAllowPaths, &SymbolicPath{Conjunction{&srcAtomNegate}, allowPath.Dst})
-			} else {
-				resAllowPaths = append(resAllowPaths, &SymbolicPath{*allowPath.Src.copy().add(&srcAtomNegate), allowPath.Dst})
-			}
+			resAllowPaths = append(resAllowPaths, &SymbolicPath{Src: *allowPath.Src.copy().add(&srcAtomNegate),
+				Dst: allowPath.Dst, Conn: allowPath.Conn})
 		}
 	}
 	for _, dstAtom := range denyPath.Dst {
 		if !dstAtom.isTautology() {
 			dstAtomNegate := dstAtom.negate().(atomicTerm)
-			if allowPath.Dst.isTautology() {
-				resAllowPaths = append(resAllowPaths, &SymbolicPath{allowPath.Src, Conjunction{&dstAtomNegate}})
-			} else {
-				resAllowPaths = append(resAllowPaths, &SymbolicPath{allowPath.Src, *allowPath.Dst.copy().add(&dstAtomNegate)})
-			}
+			resAllowPaths = append(resAllowPaths, &SymbolicPath{Src: allowPath.Src, Dst: *allowPath.Dst.copy().add(&dstAtomNegate),
+				Conn: allowPath.Conn})
 		}
 	}
-	return &resAllowPaths
+	if !denyPath.Conn.IsAll() { // Connection of deny path is not tautology
+		resAllowPaths = append(resAllowPaths, &SymbolicPath{Src: allowPath.Src, Dst: allowPath.Dst,
+			Conn: allowPath.Conn.Subtract(denyPath.Conn)})
+	}
+	return resAllowPaths.removeEmpty().removeTautology()
 }
 
-// ConvertFWRuleToSymbolicPaths given a rule, converts its src, dst and conn to SymbolicPaths
+// ConvertFWRuleToSymbolicPaths given a rule, converts its src, dst and Conn to SymbolicPaths
 func ConvertFWRuleToSymbolicPaths(rule *dfw.FwRule) *SymbolicPaths {
 	resSymbolicPaths := SymbolicPaths{}
 	tarmAny := Conjunction{tautology{}}
 	srcTerms := getAtomicTermsForGroups(rule.SrcGroups)
 	dstTerms := getAtomicTermsForGroups(rule.DstGroups)
 	switch {
 	case rule.IsAllSrcGroups && rule.IsAllDstGroups:
-		resSymbolicPaths = append(resSymbolicPaths, &SymbolicPath{tarmAny, tarmAny})
+		resSymbolicPaths = append(resSymbolicPaths, &SymbolicPath{Src: tarmAny, Dst: tarmAny, Conn: rule.Conn})
 	case rule.IsAllSrcGroups:
 		for _, dstTerm := range dstTerms {
-			resSymbolicPaths = append(resSymbolicPaths, &SymbolicPath{tarmAny, Conjunction{dstTerm}})
+			resSymbolicPaths = append(resSymbolicPaths, &SymbolicPath{Src: tarmAny, Dst: Conjunction{dstTerm},
+				Conn: rule.Conn})
 		}
 	case rule.IsAllDstGroups:
 		for _, srcTerm := range srcTerms {
-			resSymbolicPaths = append(resSymbolicPaths, &SymbolicPath{Conjunction{srcTerm}, tarmAny})
+			resSymbolicPaths = append(resSymbolicPaths, &SymbolicPath{Src: Conjunction{srcTerm}, Dst: tarmAny,
+				Conn: rule.Conn})
 		}
 	default:
 		for _, srcTerm := range srcTerms {
 			for _, dstTerm := range dstTerms {
-				resSymbolicPaths = append(resSymbolicPaths, &SymbolicPath{Conjunction{srcTerm}, Conjunction{dstTerm}})
+				resSymbolicPaths = append(resSymbolicPaths, &SymbolicPath{Src: Conjunction{srcTerm},
+					Dst: Conjunction{dstTerm}, Conn: rule.Conn})
 			}
 		}
 	}