Skip to content

Handling cycle in bound graph and fixing issue with policy assignment to val defs #1

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
aakash-mishra wants to merge 1 commit into
base: main
Choose a base branch
from
Open

Handling cycle in bound graph and fixing issue with policy assignment to val defs #1

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
5 changes: 3 additions & 2 deletions flowframe-plugin/src/main/scala/com/facebook/flowframe/CheckLabels.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -334,9 +334,10 @@ abstract class CheckLabels[T <: PolicyLang] extends PluginComponent with SparkSi
if (!t.hasAttachment[PolicyStruct]) {
// assume that the definition annotation overrides the type annotation
// if neither exist, resort to a default policy (generate a solver variable)
val defAnnOpt = getPolicyStruct(t.symbol, withDefault=false)
val defAnn = getPolicyStruct(t.symbol, withDefault=false).getOrElse { defaultPolicyStruct(t.symbol) }
val tptAnnOpt = getPolicyStruct(t.tpt.symbol, withDefault=false)
val pol = defAnnOpt.orElse(tptAnnOpt).getOrElse { defaultPolicyStruct(t.symbol) }

val pol = if (tptAnnOpt.isDefined) defAnn.join(tptAnnOpt.get) else defAnn
// val pol = defAnnOpt.getOrElse { defaultPolicyStruct(t.symbol) }

t.symbol.updateAttachment[PolicyStruct](pol)
Expand Down
5 changes: 3 additions & 2 deletions flowframe-plugin/src/main/scala/com/facebook/flowframe/Policies.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -121,11 +121,12 @@ trait Policies[T <: PolicyLang] {
override def subst(substMap: Map[AbstractPolicy, PolicyExpr], seen: Set[PolicyExpr] = Set.empty)
(implicit lattice: SecLattice): PolicyExpr = {
substMap.get(this) match {
// case Some(sub) if seen.contains(sub) =>
case Some(sub) if seen.contains(sub) =>
// // if there is a cycle in the bound graph, then apply cycleOp to the cycle. Typically this is a meet or join
// // 1) all policies in the cycle are equivalent, and 2) for GLB, this parameter flows to anything
// // we can prove at least one of these policies flows to
// lattice.simplify(seen.foldLeft(sub)((acc, p) => cycleOp(lattice)(acc, p)))
throw new InternalError("Found cycle in bound graph " + seen.toString())
// lattice.simplify(seen.foldLeft(sub)((acc, p) => cycleOp(lattice)(acc, p)))

case Some(sub) =>
// only recurse if we haven't seen this bound before
Expand Down
7 changes: 5 additions & 2 deletions flowframe-plugin/src/main/scala/com/facebook/flowframe/Solvers.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -44,8 +44,11 @@ trait Solvers[T <: PolicyLang] extends Constraints[T] {
}

// TODO: isn't this a LUBSolver?
class GLBSolver(lattice: SecLattice) {

class GLBSolver(val lattice: SecLattice) {
// val lattice = _lattice
// def lattice() = {
//
// }
import Status._

/**
Expand Down