Policy conversion

pkg/model/dfw/category.go

@@ -119,25 +119,25 @@ func (c *CategorySpec) analyzeCategory(src, dst *endpoints.VM, isIngress bool,
 	for _, rule := range rules /*c.rules*/ {
 		if rule.processedRuleCapturesPair(src, dst) /*rule.capturesPair(src, dst, isIngress)*/ {
 			switch rule.Action {
-			case actionAllow:
+			case ActionAllow:
 				addedAllowedConns := rule.Conn.Subtract(deniedConns).Subtract(jumpToAppConns)
 				allowedConns = allowedConns.Union(addedAllowedConns)
-			case actionDeny:
+			case ActionDeny:
 				addedDeniedConns := rule.Conn.Subtract(allowedConns).Subtract(jumpToAppConns)
 				deniedConns = deniedConns.Union(addedDeniedConns)
-			case actionJumpToApp:
+			case ActionJumpToApp:
 				addedJumpToAppConns := rule.Conn.Subtract(allowedConns).Subtract(deniedConns)
 				jumpToAppConns = jumpToAppConns.Union(addedJumpToAppConns)
 			}
 		}
 	}
 	switch c.defaultAction {
-	case actionNone: // no default configured for this category
+	case ActionNone: // no default configured for this category
 		nonDet = netset.AllTransports().Subtract(allowedConns).Subtract(deniedConns).Subtract(jumpToAppConns)
-	case actionAllow: // default allow
+	case ActionAllow: // default allow
 		allowedConns = netset.AllTransports().Subtract(deniedConns).Subtract(jumpToAppConns)
 		nonDet = netset.NoTransports()
-	case actionDeny: // default deny
+	case ActionDeny: // default deny
 		deniedConns = netset.AllTransports().Subtract(allowedConns).Subtract(jumpToAppConns)
 		nonDet = netset.NoTransports()
 	default:
@@ -218,7 +218,7 @@ func newEmptyCategory(c DfwCategory, d *DFW) *CategorySpec {
 	return &CategorySpec{
 		Category:       c,
 		dfwRef:         d,
-		defaultAction:  actionNone,
+		defaultAction:  ActionNone,
 		ProcessedRules: &EffectiveRules{},
 	}
 }

pkg/model/dfw/dfw.go

@@ -62,7 +62,7 @@ func (d *DFW) AllowedConnectionsIngressOrEgress(src, dst *endpoints.VM, isIngres
 			allAllowedConns).Subtract(allDeniedConns)
 	}
 
-	if d.defaultAction == actionAllow {
+	if d.defaultAction == ActionAllow {
 		// if the last category has no default, use the "global" default (todo: check where this value is configured in the api)
 		allAllowedConns = allAllowedConns.Union(allNotDeterminedConns)
 	}
@@ -151,10 +151,10 @@ func (d *DFW) AddRule(src, dst []*endpoints.VM, srcGroups, dstGroups, scopeGroup
 // NewEmptyDFW returns new DFW with global default as from input
 func NewEmptyDFW(globalDefaultAllow bool) *DFW {
 	res := &DFW{
-		defaultAction: actionDeny,
+		defaultAction: ActionDeny,
 	}
 	if globalDefaultAllow {
-		res.defaultAction = actionAllow
+		res.defaultAction = ActionAllow
 	}
 	for _, c := range categoriesList {
 		res.CategoriesSpecs = append(res.CategoriesSpecs, newEmptyCategory(c, res))
@@ -163,7 +163,7 @@ func NewEmptyDFW(globalDefaultAllow bool) *DFW {
 }
 
 func (d *DFW) GlobalDefaultAllow() bool {
-	return d.defaultAction == actionAllow
+	return d.defaultAction == ActionAllow
 }
 
 func (d *DFW) SetPathsToDisplayNames(m map[string]string) {

pkg/model/dfw/rule.go

@@ -24,34 +24,34 @@ const (
 var ingressDirections = []string{"IN", "IN_OUT"}*/
 
 const (
-	actionAllow     RuleAction = "allow"
-	actionDeny      RuleAction = "deny" // currently not differentiating between "reject" and "drop"
-	actionJumpToApp RuleAction = "jump_to_application"
-	actionNone      RuleAction = "none" // to mark that a default rule is not configured
+	ActionAllow     RuleAction = "allow"
+	ActionDeny      RuleAction = "deny" // currently not differentiating between "reject" and "drop"
+	ActionJumpToApp RuleAction = "jump_to_application"
+	ActionNone      RuleAction = "none" // to mark that a default rule is not configured
 )
 
 /*func actionFromString(input string) RuleAction {
 	switch input {
-	case string(actionAllow):
-		return actionAllow
-	case string(actionDeny):
-		return actionDeny
-	case string(actionJumpToApp):
-		return actionJumpToApp
+	case string(ActionAllow):
+		return ActionAllow
+	case string(ActionDeny):
+		return ActionDeny
+	case string(ActionJumpToApp):
+		return ActionJumpToApp
 	}
-	return actionDeny
+	return ActionDeny
 }*/
 
 func actionFromString(s string) RuleAction {
 	switch strings.ToLower(s) {
-	case string(actionAllow):
-		return actionAllow
-	case string(actionDeny), "reject", "drop": // TODO: change
-		return actionDeny
-	case string(actionJumpToApp):
-		return actionJumpToApp
+	case string(ActionAllow):
+		return ActionAllow
+	case string(ActionDeny), "reject", "drop": // TODO: change
+		return ActionDeny
+	case string(ActionJumpToApp):
+		return ActionJumpToApp
 	default:
-		return actionNone
+		return ActionNone
 	}
 }
 

pkg/symbolicexpr/symbolicPath.go

@@ -7,7 +7,7 @@ import (
 	"github.com/np-guard/vmware-analyzer/pkg/model/dfw"
 )
 
-func (path *SymbolicPath) string() string {
+func (path *SymbolicPath) String() string {
 	return path.Conn.String() + " from " + path.Src.string() + " to " + path.Dst.string()
 }
 
@@ -28,7 +28,7 @@ func (paths *SymbolicPaths) String() string {
 	}
 	res := make([]string, len(*paths))
 	for i, path := range *paths {
-		res[i] = path.string()
+		res[i] = path.String()
 	}
 	return strings.Join(res, "\n")
 }

pkg/symbolicexpr/symbolicexpr_test.go

@@ -32,9 +32,9 @@ func TestSymbolicPaths(t *testing.T) {
 		conjDst = *conjDst.add(&negateAtomic)
 	}
 	conjSymbolicPath := SymbolicPath{Src: conjSrc, Dst: conjDst, Conn: netset.AllTCPTransport()}
-	fmt.Printf("\nconjSymbolicPath:\n%v\n", conjSymbolicPath.string())
+	fmt.Printf("\nconjSymbolicPath:\n%v\n", conjSymbolicPath.String())
 	require.Equal(t, "TCP from (t1 = str1 and t2 = str2 and t3 = str3) to (t1 != str1 and t2 != str2 and t3 != str3)",
-		conjSymbolicPath.string(), "conjSymbolicPath not as expected")
+		conjSymbolicPath.String(), "conjSymbolicPath not as expected")
 	println("conjEmpty", conjEmpty.string())
 	require.Equal(t, emptySet, conjEmpty.string(), "empty conjunction not as expected")
 }
@@ -64,7 +64,7 @@ func TestComputeAllowGivenDenySingleTermEach1(t *testing.T) {
 	conjDst2 = *conjDst2.add(atomicDst2)
 	allowPath := SymbolicPath{Src: conjSrc1, Dst: conjDst1, Conn: netset.AllTransports()}
 	denyPath := SymbolicPath{Src: conjSrc2, Dst: conjDst2, Conn: netset.AllUDPTransport()}
-	fmt.Printf("allowPath is %v\ndenyPath is %v\n", allowPath.string(), denyPath.string())
+	fmt.Printf("allowPath is %v\ndenyPath is %v\n", allowPath.String(), denyPath.String())
 	allowGivenDeny := *computeAllowGivenAllowHigherDeny(allowPath, denyPath)
 	fmt.Printf("computeAllowGivenAllowHigherDeny(allowPath, denyPath) is\n%v\n", allowGivenDeny.String())
 	require.Equal(t, "All Connections from (s1 = str1 and s2 != str2) to (d1 = str1)\n"+
@@ -96,7 +96,7 @@ func TestComputeAllowGivenDenySingleTermEach2(t *testing.T) {
 	conjDst2 = *conjDst2.add(atomicDst2)
 	allowPath := SymbolicPath{Src: conjSrc1, Dst: conjDst1, Conn: netset.AllUDPTransport()}
 	denyPath := SymbolicPath{Src: conjSrc2, Dst: conjDst2, Conn: netset.AllTCPTransport()}
-	fmt.Printf("allowPath is %v\ndenyPath is %v\n", allowPath.string(), denyPath.string())
+	fmt.Printf("allowPath is %v\ndenyPath is %v\n", allowPath.String(), denyPath.String())
 	allowGivenDeny := *computeAllowGivenAllowHigherDeny(allowPath, denyPath)
 	fmt.Printf("computeAllowGivenAllowHigherDeny(allowPath, denyPath) is\n%v\n", allowGivenDeny.String())
 	// computeAllowGivenAllowHigherDeny not optimized
@@ -128,7 +128,7 @@ func TestComputeAllowGivenDenySingleTermEach3(t *testing.T) {
 	allowPath := SymbolicPath{Src: conjSrc1, Dst: conjDst1, Conn: netset.AllTCPTransport()}
 	denyPath := SymbolicPath{Src: conjSrc1, Dst: conjDst1, Conn: netset.NewTCPTransport(0, 50,
 		netp.MinPort, netp.MaxPort)}
-	fmt.Printf("allowPath is %v\ndenyPath is %v\n", allowPath.string(), denyPath.string())
+	fmt.Printf("allowPath is %v\ndenyPath is %v\n", allowPath.String(), denyPath.String())
 	allowGivenDenyPaths := *ComputeAllowGivenDenies(&SymbolicPaths{&allowPath}, &SymbolicPaths{&denyPath})
 	fmt.Printf("allowGivenDenyPaths is %v\n", allowGivenDenyPaths.String())
 	require.Equal(t, "TCP src-ports: 51-65535 from (s1 = str1) to (d1 = str1)", allowGivenDenyPaths.String(),
@@ -150,7 +150,7 @@ func TestComputeAllowGivenDenySingleTermEach4(t *testing.T) {
 	atomicDst1 := &atomicTerm{property: testDst1, toVal: "str1"}
 	conjDst1 = *conjDst1.add(atomicDst1)
 	path := SymbolicPath{Src: conjSrc1, Dst: conjDst1, Conn: netset.AllTCPTransport()}
-	fmt.Printf("allowPath is %v\ndenyPath is %v\n", path.string(), path.string())
+	fmt.Printf("allowPath is %v\ndenyPath is %v\n", path.String(), path.String())
 	allowGivenDenyPaths := *ComputeAllowGivenDenies(&SymbolicPaths{&path}, &SymbolicPaths{&path})
 	fmt.Printf("allowGivenDenyPaths is %v\n", allowGivenDenyPaths.String())
 	require.Equal(t, "empty set ", allowGivenDenyPaths.String(),
@@ -185,7 +185,7 @@ func TestComputeAllowGivenDenyThreeTermsEach(t *testing.T) {
 	denyPathNoEffect := SymbolicPath{Src: conjDeny, Dst: conjDeny, Conn: netset.AllUDPTransport()}
 	allowGivenDenyPaths := *ComputeAllowGivenDenies(&SymbolicPaths{&allowPath},
 		&SymbolicPaths{&denyPath, &denyPathNoEffect})
-	fmt.Printf("symbolicAllow is %s\nsymbolicDeny is %s\n", allowPath.string(), denyPath.string())
+	fmt.Printf("symbolicAllow is %s\nsymbolicDeny is %s\n", allowPath.String(), denyPath.String())
 	fmt.Printf("computeAllowGivenAllowHigherDeny(allowPath, denyPath) is\n%v\n", allowGivenDenyPaths.String())
 	require.Equal(t,
 		"TCP from (s1 = str1 and s2 = str2 and s3 = str3 and s1` != str1`) to (s1 = str1 and s2 = str2 and s3 = str3)\n"+
@@ -221,7 +221,7 @@ func TestComputeAllowGivenDenyAllowTautology(t *testing.T) {
 	tautologyConj := Conjunction{tautology{}}
 	allowPath := SymbolicPath{Src: tautologyConj, Dst: tautologyConj, Conn: netset.AllTransports()}
 	denyPath := SymbolicPath{Src: conjDeny, Dst: conjDeny, Conn: netset.AllUDPTransport()}
-	fmt.Printf("symbolicAllow is %s\nsymbolicDeny is %s\n", allowPath.string(), denyPath.string())
+	fmt.Printf("symbolicAllow is %s\nsymbolicDeny is %s\n", allowPath.String(), denyPath.String())
 	allowGivenDeny := *computeAllowGivenAllowHigherDeny(allowPath, denyPath)
 	fmt.Printf("computeAllowGivenAllowHigherDeny(allowPath, denyPath) is\n%v\n", allowGivenDeny.String())
 	require.Equal(t,
@@ -249,7 +249,7 @@ func TestComputeAllowGivenDenyDenyTautology(t *testing.T) {
 	tautologyConj := Conjunction{tautology{}}
 	allowPath := SymbolicPath{Src: conjAllow, Dst: conjAllow, Conn: netset.AllTransports()}
 	denyPath := SymbolicPath{Src: tautologyConj, Dst: tautologyConj, Conn: netset.AllTransports()}
-	fmt.Printf("symbolicAllow is %s\nsymbolicDeny is %s\n", allowPath.string(), denyPath.string())
+	fmt.Printf("symbolicAllow is %s\nsymbolicDeny is %s\n", allowPath.String(), denyPath.String())
 	allowGivenDeny := *computeAllowGivenAllowHigherDeny(allowPath, denyPath)
 	fmt.Printf("computeAllowGivenAllowHigherDeny(allowPath, denyPath) is\n%v\n", allowGivenDeny.String())
 	require.Equal(t, emptySet, allowGivenDeny.String(),
@@ -341,7 +341,7 @@ func TestAllowDenyOptimizeEmptyPath(t *testing.T) {
 	denyPath := SymbolicPath{Src: conjSrc1, Dst: conjDst1, Conn: netset.AllTransports()}
 	allowWithDeny := ComputeAllowGivenDenies(&SymbolicPaths{&allowPath}, &SymbolicPaths{&denyPath})
 	fmt.Printf("allow path: %v with higher priority deny path:%v is:\n%v\n\n",
-		allowPath.string(), denyPath.string(), allowWithDeny.String())
+		allowPath.String(), denyPath.String(), allowWithDeny.String())
 	require.Equal(t, "All Connections from (s1 = str1) to (d1 != str1)", allowWithDeny.String(),
 		"optimized with deny not working properly")
 }

pkg/synthesis/allowOnlyConversion.go

@@ -0,0 +1,109 @@
+package synthesis
+
+import (
+	"strings"
+
+	"github.com/np-guard/vmware-analyzer/pkg/model/dfw"
+	"github.com/np-guard/vmware-analyzer/pkg/symbolicexpr"
+)
+
+/////////////////////////////////////////////////////////////////////////////////////
+// convert symbolic rules to allow only functionality
+/////////////////////////////////////////////////////////////////////////////////////
+
+func computeAllowOnlyRulesForPolicy(categoriesSpecs []*dfw.CategorySpec,
+	categoryToPolicy map[dfw.DfwCategory]*symbolicPolicy) symbolicPolicy {
+	allowOnlyPolicy := symbolicPolicy{}
+	globalInboundDenies, globalOutboundDenies := symbolicexpr.SymbolicPaths{}, symbolicexpr.SymbolicPaths{}
+	// we go over categoriesSpecs to make sure we follow the correct order of categories
+	for _, category := range categoriesSpecs {
+		thisCategoryPolicy := categoryToPolicy[category.Category]
+		if thisCategoryPolicy == nil {
+			continue
+		}
+		inboundAllow, outboundAllow := computeAllowOnlyRulesForCategory(thisCategoryPolicy,
+			&globalInboundDenies, &globalOutboundDenies)
+		allowOnlyPolicy.inbound = append(allowOnlyPolicy.inbound, inboundAllow...)
+		allowOnlyPolicy.outbound = append(allowOnlyPolicy.outbound, outboundAllow...)
+	}
+	return allowOnlyPolicy
+}
+
+// gets here only if policy is not nil
+func computeAllowOnlyRulesForCategory(originalPolicy *symbolicPolicy, globalInboundDenies,
+	globalOutboundDenies *symbolicexpr.SymbolicPaths) (inboundAllowOnly, outboundAllowOnly []*symbolicRule) {
+	inboundAllowOnly = computeAllowOnlyInboundOrOutbound(originalPolicy.inbound, globalInboundDenies)
+	outboundAllowOnly = computeAllowOnlyInboundOrOutbound(originalPolicy.outbound, globalOutboundDenies)
+	return
+}
+
+func computeAllowOnlyInboundOrOutbound(originalRules []*symbolicRule, globalDenies *symbolicexpr.SymbolicPaths) []*symbolicRule {
+	if originalRules == nil {
+		return nil
+	}
+	newAllows, newDenies := computeAllowOnlyForCategory(&originalRules, globalDenies)
+	*globalDenies = append(*globalDenies, *newDenies...)
+	return newAllows
+}
+
+// computes allow only rules, using the following algorithm:
+// For each category, in order:
+// Initialization:
+//
+//	category_passes = empty set
+//
+// For each rule, in order
+//
+//	case pass:
+//		category_passes = category_passes  or rule
+//	case deny:
+//		new_denies = merge(category_passes, deny_rule)
+//		global_denies = global_denies  union new_denies
+//	case allow:
+//		new_allow = merge(global_denies or category_passes, allow_rule)
+//		global_allows = global_allows  or new_allows
+//	Output: global_allows
+func computeAllowOnlyForCategory(inboundOrOutbound *[]*symbolicRule,
+	globalDenies *symbolicexpr.SymbolicPaths) (allowRule []*symbolicRule, denyPaths *symbolicexpr.SymbolicPaths) {
+	allowOnlyRules := []*symbolicRule{}
+	categoryPasses := symbolicexpr.SymbolicPaths{}
+	newGlobalDenies := symbolicexpr.SymbolicPaths{}
+	copy(newGlobalDenies, *globalDenies)
+	for _, rule := range *inboundOrOutbound {
+		switch rule.origRule.Action {
+		case dfw.ActionJumpToApp:
+			categoryPasses = append(categoryPasses, *rule.origSymbolicPaths...)
+		case dfw.ActionDeny:
+			newSymbolicPaths := symbolicexpr.ComputeAllowGivenDenies(rule.origSymbolicPaths, &categoryPasses)
+			newGlobalDenies = append(newGlobalDenies, *newSymbolicPaths...)
+		case dfw.ActionAllow:
+			symbolicDeniesAndPasses := symbolicexpr.SymbolicPaths{}
+			symbolicDeniesAndPasses = append(symbolicDeniesAndPasses, newGlobalDenies...)
+			symbolicDeniesAndPasses = append(symbolicDeniesAndPasses, categoryPasses...)
+			newSymbolicPaths := symbolicexpr.ComputeAllowGivenDenies(rule.origSymbolicPaths, &symbolicDeniesAndPasses)
+			newRule := &symbolicRule{origRule: rule.origRule, origRuleCategory: rule.origRuleCategory,
+				origSymbolicPaths: rule.origSymbolicPaths, allowOnlyRulePaths: *newSymbolicPaths}
+			allowOnlyRules = append(allowOnlyRules, newRule)
+		}
+	}
+	return allowOnlyRules, &newGlobalDenies
+}
+
+func strAllowOnlyPolicy(policy *symbolicPolicy) string {
+	return "Allow Only Rules\n~~~~~~~~~~~~~~~~~\ninbound rules\n" +
+		strAllowOnlyPathsOfRules(policy.inbound) + "\noutbound rules\n" +
+		strAllowOnlyPathsOfRules(policy.outbound)
+}
+
+func strAllowOnlyPathsOfRules(rules []*symbolicRule) string {
+	res := []string{}
+	for _, rule := range rules {
+		if rule.allowOnlyRulePaths == nil {
+			continue
+		}
+		for _, path := range rule.allowOnlyRulePaths {
+			res = append(res, "\t"+path.String())
+		}
+	}
+	return strings.Join(res, "\n")
+}

pkg/synthesis/symbolicPolicy.go → pkg/synthesis/preProcessing.go

@@ -8,6 +8,10 @@ import (
 	"github.com/np-guard/vmware-analyzer/pkg/symbolicexpr"
 )
 
+/////////////////////////////////////////////////////////////////////////////////////
+// preprocessing related functionality
+/////////////////////////////////////////////////////////////////////////////////////
+
 // preProcessing: convert policy from spec to symbolicPolicy struct
 func preProcessing(categoriesSpecs []*dfw.CategorySpec) (categoryToPolicy map[dfw.DfwCategory]*symbolicPolicy) {
 	categoryToPolicy = map[dfw.DfwCategory]*symbolicPolicy{}

pkg/synthesis/synthesis.go

@@ -7,15 +7,15 @@ import (
 	"github.com/np-guard/vmware-analyzer/pkg/model"
 )
 
-func NSXToAbstractModelSynthesis(recourses *collector.ResourcesContainerModel, params model.OutputParameters) (string, error) {
-	_ = params
+func NSXToAbstractModelSynthesis(recourses *collector.ResourcesContainerModel) (*symbolicPolicy, error) {
 	parser := model.NewNSXConfigParserFromResourcesContainer(recourses)
 	err := parser.RunParser()
 	if err != nil {
-		return "", err
+		return nil, err
 	}
 	config := parser.GetConfig()
 	categoryToPolicy := preProcessing(config.Fw.CategoriesSpecs)
 	fmt.Println(stringCategoryToSymbolicPolicy(categoryToPolicy))
-	return "", nil
+	allowOnlyPolicy := computeAllowOnlyRulesForPolicy(config.Fw.CategoriesSpecs, categoryToPolicy)
+	return &allowOnlyPolicy, nil
 }