Commit bed072b8 authored by Christian Müller's avatar Christian Müller

fix choice encodings in stubborn agents

parent 831cef8d
......@@ -115,8 +115,7 @@ object Encoding extends LazyLogging {
def encodeSem(sig: Signature, g: Graph[Int, LDiEdge]) = {
val impls = for (e <- g.edges.toList) yield {
// TODO: choicevar breaks as soon as we change the graph structure
val choice = if (e.may) Some(Fun(choiceVar(e.from), e.agents)) else None
val choice = e.pred.map(n => Fun(n, e.agents))
val res = for (s <- e.steps) yield {
encodeStmt(s, choice)
......
......@@ -54,8 +54,8 @@ object Main extends App with LazyLogging {
val quantfree = LTL.eliminateUniversals(res, agents)
val ltlprop = LTL.eliminatePredicates(quantfree)
write(s"${name}_size${agents.size}.ltl", ltlprop.toString())
write(s"${name}_size${agents.size}.ppltl", ltlprop.pretty())
write(s"${name}.ltl", ltlprop.toString())
write(s"${name}.ppltl", ltlprop.pretty())
logger.info(s"Written all files for $name")
}
......
......@@ -115,8 +115,8 @@ object WorkflowParser extends RegexParsers with LazyLogging {
// logics
def tt = "True" ^^^ True
def ff = "False" ^^^ False
def AND = repsep(SIMPLETERM, "∧") ^^ { case ts => And.make(ts) }
def OR = repsep(SIMPLETERM, "∨") ^^ { case ts => Or.make(ts) }
def AND = "(" ~> repsep(TERM, "∧") <~ ")" ^^ { case ts => And.make(ts) }
def OR = "(" ~> repsep(TERM, "∨") <~ ")" ^^ { case ts => Or.make(ts) }
def NEG = ("¬" | "!") ~ SIMPLETERM ^^ { case _ ~ t => Neg(t) }
// temporals
......@@ -127,7 +127,7 @@ object WorkflowParser extends RegexParsers with LazyLogging {
def FUN = VAR ~ TUPLE ^^ { case f ~ tup => Fun(f.name, tup) }
def SIMPLETERM = (tt | ff | FUN )
def TERM:Parser[Term] = (SIMPLETERM | GLOBALLY | FINALLY | "(" ~> AND <~ ")" | "(" ~> OR <~ ")" | NEG )
def TERM:Parser[Term] = (SIMPLETERM | GLOBALLY | FINALLY | AND | OR | NEG )
def ADD = TERM ~ ("→" | "->") ~ VAR ~ "+=" ~ TUPLE ^^ { case guard ~ _ ~ fun ~ _ ~ tup => Add(guard, fun.name, tup) }
def REM = TERM ~ ("→" | "->") ~ VAR ~ "-=" ~ TUPLE ^^ { case guard ~ _ ~ fun ~ _ ~ tup => Remove(guard, fun.name, tup) }
......
......@@ -27,8 +27,9 @@ case class Spec(w: Workflow, declass: List[(Fun, Term)], target: Fun, causals:Li
// TODO: check target types
// TODO: check declass arities and types (o should be an Oracle relation etc)
val ta = target.params(0)
// check declass bindings
for ((o, t) <- declass if !t.freeVars().forall(v => o.freeVars().contains(v))) {
for ((o, t) <- declass if !t.freeVars().forall(v => (o.freeVars().contains(v) || (v == ta)))) {
logger.error(s"Not all variables of the declassification condition for $o bound by the oracle")
sane = false
}
......@@ -46,6 +47,7 @@ abstract sealed class SimpleBlock extends Block {
def agents: List[Var]
def steps: List[Statement]
def may: Boolean
def pred: Option[String]
}
abstract class Statement {
......@@ -66,17 +68,20 @@ case class Remove(guard: Term, fun: String, tuple: List[Var]) extends Statement
case class ForallBlock(agents: List[Var], steps: List[Statement]) extends SimpleBlock {
val may = false
override def toString() = "forall " + agents.map(_.withType).mkString(",") + steps.mkString("\n ", ";\n ", "")
override def pred() = None
}
case class ForallMayBlock(agents: List[Var], pred: String, steps: List[Statement]) extends SimpleBlock {
case class ForallMayBlock(agents: List[Var], choice: String, steps: List[Statement]) extends SimpleBlock {
val may = true
override def toString() = "forall " + agents.map(_.withType).mkString(",") + " may (" + pred + ")" + steps.mkString("\n ", ";\n ", "")
override def pred() = Some(choice)
}
case class Loop(steps: List[Block]) extends Block {
val agents = List()
override def toString() = {
// indentation
val s = steps.map(_.toString().lines.mkString(" ", "\n ", ""))
"loop(*)\n" + s.mkString(";\n")
}
}
......@@ -70,11 +70,7 @@ object Noninterference extends LazyLogging {
val agent = spec.target.params(0)
val samechoices = Stubborn(agent, choices)
val sameoracles = for ((o,t) <- spec.declass) yield {
// Forall fv(o). (t_T1 and t_t2) -> G (o_T1 <-> o_T2)
Forall(o.freeVars().toList, Implies(And(t.in(T1), t.in(T2)), Globally(Eq(o.in(T1), o.in(T2)))))
}
val decl = And.make(sameoracles)
val decl = Declassification(spec)
val difference = Neg(Eq(spec.target.in(T1), spec.target.in(T2)))
......@@ -82,6 +78,16 @@ object Noninterference extends LazyLogging {
}
}
object Declassification extends {
def apply(spec: Spec) = {
val sameoracles = for ((o,t) <- spec.declass) yield {
// Forall fv(o). (t_T1 and t_t2) -> G (o_T1 <-> o_T2)
Forall(o.freeVars().toList, Implies(And(t.in(T1), t.in(T2)), Globally(Eq(o.in(T1), o.in(T2)))))
}
And.make(sameoracles)
}
}
object Properties {
val T1 = "t1"
......@@ -101,7 +107,9 @@ object Properties {
val choices = allchoices(spec.w) map (_.name)
val equals = nodes ++ choices
val noninter = Exists(agents, Finally(Neg(Eq(spec.target.in(T1), spec.target.in(T2)))))
val decl = Declassification(spec)
val noninter = Exists(agents, And(decl, Finally(Neg(Eq(spec.target.in(T1), spec.target.in(T2))))))
// maybe add exists t1, t2. phi?
And.make(cfg, sem.in(T1, equals), sem.in(T2, equals), noninter)
......@@ -118,7 +126,6 @@ object Properties {
val agents = spec.target freeVars() toList
// choice and node predicates are equal in both runs (stubborn)
val nodes = nodepredicates(graph) map (_.name)
val choices = allchoices(spec.w)
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment