Merge branch 'master' of versioncontrolseidl.in.tum.de:mueller/loopingworkflows

README.md

 # Looping Workflows
 
-Scala Implementation of the workflow language with loops.
+Scala Implementation of the workflow language with loops published in CSF '17.
+
+## Parser 
 There is a working parser that can read the ``*.spec`` files in ``/examples``.
 
 Workflows can also be specified directly in Scala by instantiating case classes.
@@ -14,7 +16,7 @@ To get sbt to build the project properly, you have to add the Supersafe Compiler
 
 ## Example File Format
 
-A readable example can be found at ``/examples/easychair.spec``.
+A readable example can be found at ``/examples/conference.spec``.
 The example file format consists of the following blocks:
 
 ```
@@ -24,6 +26,15 @@ Workflow
 # If types are omitted, everything is of type T, types can be given while binding the variables with the forall x:X
 # Please use forallmay x:X,y:Y instead of forall x:X,y:Y may (because of easier parsing)
 
+Declassify
+
+# optional block
+# Declassification conditions for all Oracles.
+# Specify with types.
+# Use the first agent of the target as noninterference agent.
+# These are state-based, so will be evaluated on every state to find violations.
+# Currently, no temporal operators here are supported.
+
 Target
 
 # the relation where the noninterference counterexample should be found. Make sure the types match. 

src/main/scala/de/tum/workflows/Preconditions.scala

@@ -48,28 +48,4 @@ object Preconditions extends LazyLogging {
     }
   }
 
-  def weakestPreconditionWithInformedness(f: Formula, b: SimpleBlock) = {
-
-    val wp = weakestPrecondition(f, b)
-
-    val PRED = "__inf__"
-    val agent = "_i_"
-
-    if (b.may) {
-
-      val updates = b.steps.map(s => {
-        val frees = s.guard.freeVars() -- Set(s.tuple.head)
-
-        s match {
-          case Add(_, _, _) => {
-            Or(Fun(s.fun, s.tuple), Exists(frees.toList, guard)).simplify()
-          }
-          case Remove(_, _, _) => {
-            And(Fun(s.fun, s.tuple), Forall(frees.toList, Neg(guard))).simplify()
-          }
-        }
-      })
-    }
-
-  }
 }
\ No newline at end of file

src/main/scala/de/tum/workflows/toz3/InvariantChecker.scala

@@ -49,7 +49,7 @@ object InvariantChecker extends LazyLogging {
     val graph = Encoding.toGraph(w)
     
     val msg = new StringBuilder()
-    msg ++= s"Trying to prove safe with invariant:\n${inv.pretty()}"
+    msg ++= s"Trying to prove safe with invariant:\n\n${inv.pretty()}\n\n"
     
     // Check all edges 
     val list = for (e <- graph.edges) yield {
@@ -70,7 +70,7 @@ object InvariantChecker extends LazyLogging {
       
       val res = checkOnZ3(tocheck)
       if (res != Status.UNSATISFIABLE) {
-        msg ++= s"Possibly unsafe: Block\n${e.label}\nmay not uphold invariant."
+        msg ++= s"Possibly unsafe: Block\n\n${e.label}\n\nmay not uphold invariant.\n"
         logger.info(s"Could not prove invariant $inv")
         logger.info(s"Z3 status $res")
         logger.info(s"Block ${e.label} may not uphold it")
@@ -80,7 +80,7 @@ object InvariantChecker extends LazyLogging {
     
     val safe = list.reduceLeft(_ && _)
     if (safe) {
-      msg ++= s"Proven safe."
+      msg ++= s"Proven safe.\n"
       logger.info(s"Workflow $w\n proven safe for invariant:\n${inv.pretty()}")
     }
     (safe, msg)
@@ -104,6 +104,6 @@ object InvariantChecker extends LazyLogging {
       Forall(quant, genEq(r, agent::quant))
     })
     
-    Forall(agent, Implies(premise, conclusion))
+    Forall(agent, Implies(premise, conclusion)).simplify()
   }
 }
\ No newline at end of file

src/test/scala/de/tum/workflows/ltl/tests/InvariantTest.scala

@@ -25,8 +25,8 @@ class InvariantTest extends FlatSpec {
     safe should be(true)
   }
 
-  it should "prove fail to prove unsafe workflows safe" in {
-
+  it should "fail to prove unsafe workflows safe" in {
+    
     val wf = ExampleWorkflows.parseExample("tests/simpleChoice").get.w
 
     val inv = Forall(List("a", "b"), Eq(Fun("R", Some("t1"), List("a", "b")), Fun("R", Some("t2"), List("a", "b"))))
@@ -40,16 +40,38 @@ class InvariantTest extends FlatSpec {
     val wf = ExampleWorkflows.parseExample("omitting/conference").get.w
 
     val x = Var("x", "A")
-    val p = Var("p", "P")
-    val r = Var("r", "R")
-
-    val inv = Forall(List(x, p, r), Implies(Fun("Conf", List(x, p)), Neg(Fun("Read", List(x, p, r)))))
-
+    val y = Var("y", "A")
+    val p = Var("p","P")
+    val r = Var("r","R")
+    val c = Fun("Conf", Some("t1"), List(x,p))
+
+//    
+    val ceq = genEq("Conf", List(x,p))
+    val oeq = genEq("O", List(x,p,r))
+    val readeq = genEq("Read", List(x,p,r)) 
+    val assigneq = genEq("Assign", List(x,p))
+    val revieweq = genEq("Review", List(x,p,r))
+//    val premise = And(Neg(c), oeq)
+//    val conclusion = And.make(ceq, readeq, assigneq, Forall(y, revieweq))
+    
+    val premise = Forall(List(p,r), And(Neg(c), oeq))
+    val conclusion = Forall(List(p,r), And.make(ceq, readeq, assigneq, revieweq))
+    
+    val inv = Forall(List(x), 
+        Implies(premise, conclusion)
+    )
     val (safe, msg) = InvariantChecker.checkStubborn(wf, inv)
-
-    safe should be(true)
+    
+    safe should be (true)
   }
+  
 
+  def genEq(name:String, params: List[Var]) = {
+    val o1 = Fun(name, Some("t1"), params)
+    val o2 = Fun(name, Some("t2"), params)
+    Eq(o1, o2)
+  }
+  
   it should "prove noninter invariants" in {
     val spec = ExampleWorkflows.parseExample("tests/simpleChoice").get