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

fix specs, add declass

parent 425a4261
Workflow
forallmay x:A,p:P
True -> Conf += (x,p)
True Conf += (x,p)
forallmay x:A,p:P
!Conf(x,p) -> Ass += (x,p)
!Conf(x,p) Ass += (x,p)
forallmay x:A,p:P,r:R
(Ass(x,p) ∧ O(x,p,r)) -> Review += (x,p,r)
(Ass(x,p) ∧ O(x,p,r)) Review += (x,p,r)
loop {
forall xa:A,xb:A,p:P,r:R (A(xa,p) ∧ Review(xb,p,r)) -> Read += (xa,xb,p,r)
forallmay x:A,p:P,r:R (A(x,p) ∧ O(x,p,r)) -> Review += (x,p,r)
forall xa:A,xb:A,p:P,r:R (A(xa,p) ∧ Review(xb,p,r)) Read += (xa,xb,p,r)
forallmay x:A,p:P,r:R (A(x,p) ∧ O(x,p,r)) Review += (x,p,r)
}
Declassify
O(x:A,p:P,r:R): G ¬ Conf(x:A,p:P)
Target
Read(xa:A, xb:A, p:P, r:R)
......
......@@ -13,7 +13,7 @@ loop {
Declassify
¬ Conf(xa,p)
O(x:A,p:P,r:R): G ¬ Conf(x:A,p:P)
Target
......
......@@ -5,13 +5,13 @@ forallmay x:X,p:P
forallmay x:X,p:P
!Conf(x,p) -> Ass += (x,p)
forall x:X,p:P,r:R
(Ass(x,p) ∧ O(p,r)) -> Read += (x,p,r)
(Ass(x,p) ∧ O(x,p,r)) -> Read += (x,p,r)
forallmay y:X,x:X,p:P
(Ass(x,p) ∧ Ass(y,p)) -> Comm += (x,y,p)
Declassify
¬ Conf(x:X,p:P)
O(x:X,p:P,r:R): G ¬ Conf(x:A,p:P)
Target
......
sbt.version=0.13.15
......@@ -19,17 +19,24 @@ object ExampleWorkflows extends LazyLogging {
val s = Source.fromFile(f).mkString
val spec = WorkflowParser.parseSpec(s)
logger.info(s"Parsing file $f")
// drop file ending
val name = f.getName.replace(ENDING, "")
if (!spec.successful) {
logger.error(s"Parsing of $f unsuccessful: $spec")
name -> None
} else {
name -> Some(spec.get)
if (!spec.get.checkSanity()) {
logger.error(s"Sanity check of $f failed. Skipping file.")
name -> None
} else {
name -> Some(spec.get)
}
}
}) toMap
// filter out all empty specs
// filter out all empty specs and those that are not sane
for ((k, v) <- examples if (v.isDefined)) yield {
(k, v.get)
}
......
......@@ -112,23 +112,31 @@ object WorkflowParser extends RegexParsers with LazyLogging {
def VAR = IDENT ^^ { str => Var(str) }
def TYPEDVAR = IDENT ~ ((":" ~> IDENT)?) ^^ { case str ~ typ => if (typ.isDefined) Var(str, typ.get) else Var(str) }
// 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 NEG = ("¬" | "!") ~ SIMPLETERM ^^ { case _ ~ t => Neg(t) }
// temporals
def GLOBALLY = ("G" | "☐") ~> TERM ^^ { case t => Globally(t) }
def FINALLY = ("F" | "♢") ~> TERM ^^ { case t => Finally(t) }
def TUPLE = "(" ~> repsep(TYPEDVAR, ",") <~ ")"
def FUN = VAR ~ TUPLE ^^ { case f ~ tup => Fun(f.name, tup) }
def SIMPLETERM = (tt | ff | FUN )
def TERM:Parser[Term] = (SIMPLETERM | "(" ~> 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) }
def STMT = ADD | REM
// TODO: There could be several - one per Oracle
def DECLASS = (FUN <~ ":") ~ TERM ^^ { case f ~ t => (f,t) }
def BLOCK = "forall" ~> ("may"?) ~ repsep(TYPEDVAR, ",") ~ (STMT+) ^? ({
// all free variables contained
case may ~ vars ~ stmts if validblock(vars, stmts) => {
......@@ -153,10 +161,10 @@ object WorkflowParser extends RegexParsers with LazyLogging {
def SPEC =
"Workflow" ~! WORKFLOW ~
(("Declassify" ~> TERM)?) ~
(("Declassify" ~> DECLASS)?) ~
("Target" ~> FUN) ~
(("Causality" ~> repsep(TYPEDVAR, ","))?) ^^ {
case _ ~ w ~ decl ~ tar ~ causals => Spec(w, decl.getOrElse(True), tar, causals.getOrElse(List()))
case _ ~ w ~ decl ~ tar ~ causals => Spec(w, decl.toList, tar, causals.getOrElse(List()))
}
def parseWorkflow(s: String) = parseAll(WORKFLOW, s)
......
package de.tum.workflows.blocks
import de.tum.workflows.foltl.FOLTL._
import com.typesafe.scalalogging.LazyLogging
case class Signature(oracles: Set[Fun], preds: Set[Fun])
object Signature {
......@@ -14,13 +15,29 @@ object Workflow {
val EMPTY = Workflow(Signature.EMPTY, List())
}
case class Spec(w: Workflow, declass: Term, target: Fun, causals:List[Var]) {
case class Spec(w: Workflow, declass: List[(Fun, Term)], target: Fun, causals:List[Var]) extends LazyLogging {
override def toString = {
s"Spec\nWorkflow:\n$w\nDeclass:$declass\nTarget:$target"
}
def checkSanity() = {
var sane = true
// TODO: check all types
// TODO: check target types
// TODO: check declass arities and types (o should be an Oracle relation etc)
// check declass bindings
for ((o, t) <- declass if !t.freeVars().forall(v => o.freeVars().contains(v))) {
logger.error(s"Not all variables of the declassification condition for $o bound by the oracle")
sane = false
}
sane
}
}
object Spec {
val EMPTY = Spec(Workflow.EMPTY, True, Fun("NOTHING", List()), List())
val EMPTY = Spec(Workflow.EMPTY, List(), Fun("NOTHING", List()), List())
}
abstract sealed class Block
......
......@@ -66,23 +66,19 @@ object Causal {
object Noninterference extends LazyLogging {
def apply(choices: Set[Fun], spec:Spec) = {
if (!spec.declass.freeVars().forall(spec.target.params.contains(_))) {
logger.error("Not all variables of the declassification condition bound by the target")
}
val agent = spec.target.params(0)
val samechoices = Stubborn(agent, choices)
// TODO: declassification binding?
// val sameoracles = for (o <- oracles) yield {
// Forall(o.params, Eq(o.in(t1), o.in(t2)))
// }
// val decl = Or(Neg(declass.in(t1)), And.make(sameoracles toList))
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 difference = Neg(Eq(spec.target.in(T1), spec.target.in(T2)))
Exists(agent, And(samechoices, Finally(Exists(spec.target.params.drop(1), difference))))
Exists(agent, And.make(samechoices, decl, Finally(Exists(spec.target.params.drop(1), difference))))
}
}
......
......@@ -82,7 +82,7 @@ class EncodingTest extends FlatSpec {
val choices = Set(Fun("choice0", List("x", "y")))
val Rab = Fun("R", List("a", "b"))
val s = Spec(Workflow.EMPTY, True, Rab, List())
val s = Spec(Workflow.EMPTY, List(), Rab, List())
val nonint = Noninterference(choices, s)
......@@ -100,7 +100,7 @@ class EncodingTest extends FlatSpec {
choices should be (Set(Fun("choice0", List("x", "s"))))
val ce = Fun("R", List("ax", "as"))
val s = Spec(Workflow.EMPTY, True, ce, List())
val s = Spec(Workflow.EMPTY, List(), ce, List())
val noninter = Noninterference(choices, s)
noninter should be (
......@@ -108,7 +108,7 @@ class EncodingTest extends FlatSpec {
Stubborn("ax", choices),
Finally(Exists("as", Neg(Eq(ce.in(T1), ce.in(T2))))))))
val s2 = Spec(w, True, Fun("R", List("ax", "as")), List())
val s2 = Spec(w, List(), Fun("R", List("ax", "as")), List())
val prop = Properties.noninterStubborn(s2)
val (agents, res) = LTL.eliminateExistentials(prop)
......
......@@ -6,6 +6,7 @@ import org.scalatest.Inspectors._
import de.tum.workflows.WorkflowParser
import de.tum.workflows.blocks._
import de.tum.workflows.blocks
import de.tum.workflows.Implicits._
import de.tum.workflows.foltl.FOLTL._
import com.typesafe.scalalogging.LazyLogging
......@@ -34,7 +35,7 @@ class ParserTest extends FlatSpec {
}
}
def testSpecResult(s: String, wf: Workflow, declass: Term, tar: Term) {
def testSpecResult(s: String, spec:blocks.Spec) {
val parsed = WorkflowParser.parseSpec(s)
if (!parsed.successful) {
......@@ -44,13 +45,13 @@ class ParserTest extends FlatSpec {
parsed.successful should be(true)
val pwf = parsed.get.w
pwf.sig should be(wf.sig)
if (!wf.steps.isEmpty) {
pwf.steps should be(wf.steps)
pwf.sig should be(spec.w.sig)
if (!spec.w.steps.isEmpty) {
pwf.steps should be(spec.w.steps)
}
parsed.get.declass should be(declass)
parsed.get.target should be(tar)
parsed.get.declass should be(spec.declass)
parsed.get.target should be(spec.target)
}
"Workflow Parser" should "parse a single may block" in {
......@@ -187,7 +188,7 @@ class ParserTest extends FlatSpec {
val t = Fun("R", List("x", "s"))
testSpecResult(s, w, True, t)
testSpecResult(s, Spec(w, List(), t, List()))
}
it should "parse simpleNochoice with declassification" in {
......@@ -199,7 +200,7 @@ class ParserTest extends FlatSpec {
Declassify
O(x)
O(x): True
Target
......@@ -213,6 +214,6 @@ class ParserTest extends FlatSpec {
val t = Fun("R", List("x", "s"))
testSpecResult(s, w, Fun("O", List("x")), t)
testSpecResult(s, Spec(w, List((Fun("O", List("x")), True)), t, List()))
}
}
\ No newline at end of file
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