add causality

.gitignore

@@ -27,3 +27,4 @@ build
 # Resulting ltl formulas
 results/*.ltl
 results/*.ppltl
+results/*.foltl

cnf.dimacs

-p cnf 24 29
-6 0
--6 7 0
--6 8 0
--7 -1 -2 0
--8 9 0
--8 10 0
--9 -1 -3 0
--10 11 0
--10 12 0
--11 -1 -4 0
--12 13 0
--12 14 0
--13 -1 -5 0
--14 15 0
--14 16 0
--15 -2 -3 0
--16 17 0
--16 18 0
--17 -2 -4 0
--18 19 0
--18 20 0
--19 -2 -5 0
--20 21 0
--20 22 0
--21 -3 -4 0
--22 23 0
--22 24 0
--23 -3 -5 0
--24 -4 -5 0
+p cnf 3 2
+3 0
+-3 1 2 0

examples/easychair.spec

@@ -13,4 +13,4 @@ loop {
 
 Target
 
-(Conf(xa,p) ∧ Read(xa, xb, p, r))
+Read(xa, xb, p, r)

examples/easychair3NoOracle.spec

@@ -11,6 +11,10 @@ loop {
 	forall x,p (A(x,p) ∧ O(x,p,r)) -> Acc += (x,p)
 }
 
+Declassify
+
+¬ Conf(xa,p)
+
 Target
 
-(Conf(xa, p) ∧ Acc(xa,xb,p))
+Acc(xa,xb,p)

examples/easychairNoOracle.spec

@@ -11,6 +11,10 @@ loop {
 	forall x,p,r (A(x,p) ∧ O(x,p,r)) -> Review += (x,p,r)
 }
 
+Declassify
+
+¬ Conf(xa,p)
+
 Target
 
-(Conf(xa,p) ∧ Read(xa,xb,p,r))
\ No newline at end of file
+Read(xa,xb,p,r)
\ No newline at end of file

examples/easychair_linear.spec

@@ -9,6 +9,10 @@ forall x,p,r
 forallmay y,x,p 
 	(Ass(x,p) ∧ Ass(y,p)) -> Comm += (x,y,p)
 
+Declassify
+
+¬ Conf(x,p)
+
 Target
 
-(Conf(x,p) ∧ Comm(x, y, p))
+Comm(x, y, p)

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

@@ -133,7 +133,7 @@ object Encoding extends LazyLogging {
   }
   
   def encodeInitial(sig: Signature, g: Graph[Int, LDiEdge]) = {
-    val empties = for (f <- sig.preds) yield {
+    val empties = for (f <- sig.preds toList) yield {
       Forall(f.params, Neg(f))
     }
     And.make(empties)

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

@@ -23,6 +23,6 @@ object ExampleWorkflows extends LazyLogging {
     
     // drop file ending
     val name = f.getName.replace(ENDING, "")
-    name -> (spec.get._1, spec.get._2)
+    name -> spec.get
   }) toMap
 }

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

@@ -11,6 +11,7 @@ import de.tum.workflows.foltl.Properties
 import java.io.PrintWriter
 import java.io.File
 import de.tum.workflows.blocks.Workflow
+import de.tum.workflows.blocks.Spec
 
 object Main extends App with LazyLogging {
   
@@ -18,20 +19,22 @@ object Main extends App with LazyLogging {
   
   def generateExample(name: String) {
       logger.info(s"Generating $name")
-      val (wf, target) = ExampleWorkflows.examples(name)
-      stubbornnoninter(name, wf, target)
+      val spec = ExampleWorkflows.examples(name)
+      
+      generate(name, spec)
   }
+  
+  def write(name: String, prop:Term) {
+    val file = new File(name)
+    val writer = new PrintWriter(file)
+    writer.print(prop)
+    writer.close()
+  }
+  
+  def writeExample(name: String, prop: Term) {
 
-  def stubbornnoninter(name: String, w: Workflow, target: Term) {
-    logger.info(s"Encoding Workflow:\n$w")
-    logger.info("Using only stubborn agents")
-    val t1 = "pi1"
-    val t2 = "pi2"
-
-    logger.info(s"Computing noninterference for target $target")
-
-    val prop = Properties.noninterStubborn(w, target)
-
+    write(s"${name}.foltl", prop.pretty())
+    
     val (agents, res) = LTL.eliminateExistentials(prop)
     
     logger.info(s"Using universe $agents")
@@ -43,17 +46,24 @@ object Main extends App with LazyLogging {
     val quantfree = LTL.eliminateUniversals(res, agents)
     val ltlprop = LTL.eliminatePredicates(quantfree)
 
-    val file = new File(s"results/${name}_stubborn_${agents.size}agents.ltl")
-    val writer = new PrintWriter(file)
-    writer.print(ltlprop)
-    writer.close()
+    write(s"${name}_${agents.size}agents.ltl", ltlprop)
+    write(s"${name}_${agents.size}agents.ppltl", ltlprop.pretty())
     
-    val ppfile = new File(s"results/${name}_stubborn_${agents.size}agents.ppltl")
-    val ppwriter = new PrintWriter(ppfile)
-    ppwriter.print(ltlprop.pretty())
-    ppwriter.close()
+    logger.info(s"Written all files for $name")
+  }
 
-    logger.info(s"Saved resulting property at ${file.toPath()}")
+  def generate(name: String, spec:Spec) {
+    logger.info(s"Encoding Workflow:\n$spec.w")
+    val t1 = "pi1"
+    val t2 = "pi2"
+
+    logger.info(s"Computing noninterference for target ${spec.target} using only stubborn agents")
+    val prop = Properties.noninterStubborn(spec)
+    writeExample(s"results/${name}_stubborn", prop)
+    
+    logger.info(s"Computing noninterference for target ${spec.target} using a single causal agent")
+    val cprop = Properties.noninterCausal(spec, 1)
+    writeExample(s"results/${name}_causal", cprop)
   }
 
   for (k <- ExampleWorkflows.examples.keys) {

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

@@ -45,7 +45,7 @@ object WorkflowParser extends RegexParsers {
     
     val (oracles, rels) = filtered.partition(_.name.startsWith("O"))
     
-    Signature(oracles toList, rels toList)
+    Signature(oracles toSet, rels toSet)
   }
   
 
@@ -78,7 +78,7 @@ object WorkflowParser extends RegexParsers {
     Workflow(buildSig(choiceblocks), choiceblocks) 
   }}
   
-  def SPEC = "Workflow" ~> WORKFLOW ~ "Target" ~ TERM ^^ { case w ~ _ ~ t => (w, t) }
+  def SPEC = "Workflow" ~> WORKFLOW ~ (("Declassify" ~> TERM)?) ~ ("Target" ~> FUN) ^^ { case w ~ decl ~ tar => Spec(w, decl.getOrElse(True), tar) }
   
   def parseWorkflow(s: String) = parseAll(WORKFLOW, s)
   def parseSpec(s: String) = parseAll(SPEC, s)

src/main/scala/de/tum/workflows/blocks/Workflow.scala

@@ -2,12 +2,14 @@ package de.tum.workflows.blocks
 
 import de.tum.workflows.foltl.FOLTL._
 
-case class Signature(oracles: List[Fun], preds: List[Fun])
+case class Signature(oracles: Set[Fun], preds: Set[Fun])
 
 case class Workflow(sig: Signature, steps: List[Block]) {
   override def toString() = steps.mkString("\n")
 }
 
+case class Spec(w: Workflow, declass: Term, target: Fun)
+
 abstract sealed class Block
 
 abstract sealed class SimpleBlock extends Block {

src/main/scala/de/tum/workflows/foltl/FOLTL.scala

@@ -22,7 +22,7 @@ object FOLTL {
 
     def pretty(): String = {
       val s = this.toString
-      val broken = s replace ("∧ ", "∧ \n")
+      val broken = s replace ("∧ ", "∧\n") replace ("∨ ", "∨\n")
 
       // indent
       var opens = 0;
@@ -51,6 +51,7 @@ object FOLTL {
   }
   case class Fun(name: String, ind: Option[String], params: List[Var]) extends Term {
     override def toString() = name + Utils.mkString(ind, "(", "", ")") + params.mkString("(", ",", ")")
+    def updatedParams(index: Int, p:Var) = Fun(name, ind, params.updated(index, p)) 
   }
 
   trait Quantifier extends Term {
@@ -97,6 +98,10 @@ object FOLTL {
     val make = Until.apply _
     val opname = "U"
   }
+  
+  object WUntil {
+    def apply(t1: Term, t2: Term) = Or(Until(t1, t2), Globally(t1)) 
+  }
 
   trait UnOp extends Term {
     def make: Term => UnOp

src/main/scala/de/tum/workflows/foltl/Properties.scala

@@ -5,11 +5,12 @@ import de.tum.workflows.Encoding._
 import de.tum.workflows.blocks._
 import de.tum.workflows.foltl.FOLTL._
 import de.tum.workflows.Utils._
+import com.typesafe.scalalogging.LazyLogging
 
 object Stubborn {
   def apply(agent: Var, choices: Set[Fun], t1: String, t2: String) = {
     And.make(for (c <- choices toList) yield {
-      val f = Fun(c.name, c.params.updated(0, agent))
+      val f = c.updatedParams(0, agent)
     	Globally(
     	  Forall(c.params.drop(1), Eq(f.in(t1), f.in(t2)))    
    		)
@@ -17,45 +18,95 @@ object Stubborn {
   }
 }
 
-object Noninterference {
-  def apply(choices: Set[Fun], target: Fun, t1: String, t2:String) = {
+object Causal {
+  def apply(agent: Var, inputs: Set[Fun], outputs: Set[Fun], t1: String, t2: String) = {
     
-    val agent = target.params(0)
+    val equalchoices = for (c <- inputs toList) yield {
+      val newc = c.updatedParams(0, agent)
+      Forall(c.params.drop(1), Eq(newc.in(t1), newc.in(t2)))                    
+    }
     
-    val cechoices = for (f <- choices) yield {
-      Fun(f.name, f.params.updated(0, agent))
+    val vexist = outputs flatMap (_.params) toList
+    val violations = for (o <- outputs toList) yield {
+      val newo = o.updatedParams(0, agent)
+      Neg(Eq(newo.in(t1), newo.in(t2)))
     }
-    val samechoices = Stubborn(agent, choices, t1, t2)
     
-    val difference = Exists(target.params.drop(1), Neg(Eq(target.in(t1), target.in(t2))))
+    WUntil(And.make(equalchoices), Exists(vexist, Or.make(violations)))    
+  }
+}
+
+object Noninterference extends LazyLogging {
+  def apply(choices: Set[Fun], spec:Spec, t1: String, t2:String) = {
+        
+    if (!spec.declass.freeVars().forall(spec.target.params.contains(_))) {
+      logger.error("Not all variables of the declassification condition bound by the target")
+    }
     
-    Exists(agent, And(samechoices, Finally(difference)))
+    val agent = spec.target.params(0)
+    val samechoices = Stubborn(agent, choices, t1, t2)
     
+    // 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 difference = Neg(Eq(spec.target.in(t1), spec.target.in(t2)))
+
+    Exists(agent, And(samechoices, Finally(Exists(spec.target.params.drop(1), difference))))
   }
 }
 
 object Properties {
   
   // include optimizations for choices
-  def noninterStubborn(w: Workflow, target: Term) = {
+  def noninterStubborn(spec: Spec) = {
     
     val t1 = "t1"
     val t2 = "t2"
     
-    val graph = toGraph(w)
+    val graph = toGraph(spec.w)
     val cfg = sanecfg(graph)
-    val sem = exec(w.sig, graph)
+    val sem = exec(spec.w.sig, graph)
 
-    val agents = target freeVars() toList
+    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(w) map (_.name)
+    val choices = allchoices(spec.w) map (_.name)
     val equals = nodes ++ choices
     
-    val noninter = Exists(agents, Finally(Neg(Eq(target.in(t1), target.in(t2)))))
+    val noninter = Exists(agents, 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)
   }
+  
+  def noninterCausal(spec:Spec, causalNum: Int) = {
+    
+    val t1 = "t1"
+    val t2 = "t2"
+    
+    val causals = (0 until causalNum) map (x => Var("causal" + x)) toList
+    
+    val graph = toGraph(spec.w)
+    val cfg = sanecfg(graph)
+    val sem = exec(spec.w.sig, graph)
+
+    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)
+    
+    val noninter = Noninterference(choices, spec, t1, t2)
+    
+    val causal = And.make(for (a <- causals) yield {
+      Exists(a, Causal(a, choices, spec.w.sig.preds, t1, t2))
+    })
+    
+    // maybe add exists t1, t2. phi?
+    And.make(cfg, sem.in(t1, nodes), sem.in(t2, nodes), noninter, causal)
+  }
 }

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

@@ -14,10 +14,12 @@ import de.tum.workflows.Utils._
 import de.tum.workflows.foltl.Properties
 import de.tum.workflows.ltl.LTL
 import de.tum.workflows.ExampleWorkflows
+import de.tum.workflows.blocks._
+
 
 class EncodingTest extends FlatSpec {
 
-  val w = ExampleWorkflows.examples("simpleChoice")._1
+  val w = ExampleWorkflows.examples("simpleChoice").w
 
   // shorthands
   val n0 = Fun("n0", List())
@@ -75,11 +77,13 @@ class EncodingTest extends FlatSpec {
   }
 
   "Noninterference encoding" should "work" in {
-
+    
     val choices = Set(Fun("choice0", List("x", "y")))
     val Rab = Fun("R", List("a", "b"))
+    
+    val s = Spec(Workflow(Signature(Set(), Set()), List()), True, Rab)
 
-    val nonint = Noninterference(choices, Rab, "t1", "t2")
+    val nonint = Noninterference(choices, s, "t1", "t2")
 
     val aux0ay = Fun("choice0", List("a", "y"))
 
@@ -96,14 +100,17 @@ class EncodingTest extends FlatSpec {
 
     choices should be (Set(Fun("choice0", List("x", "s"))))
     val ce = Fun("R", List("ax", "as"))
+    
+    val s = Spec(Workflow(Signature(Set(), Set()), List()), True, ce)
 
-    val noninter = Noninterference(choices, ce, t1, t2)
+    val noninter = Noninterference(choices, s, t1, t2)
     noninter should be (
       Exists("ax", And(
         Stubborn("ax", choices, t1, t2),
         Finally(Exists("as", Neg(Eq(ce.in(t1), ce.in(t2))))))))
 
-    val prop = Properties.noninterStubborn(w, Fun("R", List("ax", "as")))
+    val s2 = Spec(w, True, Fun("R", List("ax", "as")))
+    val prop = Properties.noninterStubborn(s2)
 
     val (agents, res) = LTL.eliminateExistentials(prop)
     

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

@@ -11,6 +11,8 @@ import de.tum.workflows.foltl.FOLTL._
 import com.typesafe.scalalogging.LazyLogging
 
 class ParserTest extends FlatSpec {
+  
+  val oxrxssig = Signature(Set(Fun("O", List("x"))), Set(Fun("R", List("x", "s"))))
 
   def testResult(s: String, sig: Signature) {
     testResult(s, Workflow(sig, List()))
@@ -32,7 +34,7 @@ class ParserTest extends FlatSpec {
     }
   }
 
-  def testSpecResult(s: String, wf: Workflow, tar: Term) {
+  def testSpecResult(s: String, wf: Workflow, declass: Term, tar: Term) {
     val parsed = WorkflowParser.parseSpec(s)
 
     if (!parsed.successful) {
@@ -40,20 +42,21 @@ class ParserTest extends FlatSpec {
     }
 
     parsed.successful should be(true)
-    val pwf = parsed.get._1
+    val pwf = parsed.get.w
 
     pwf.sig should be(wf.sig)
     if (!wf.steps.isEmpty) {
       pwf.steps should be(wf.steps)
     }
 
-    parsed.get._2 should be(tar)
+    parsed.get.declass should be(declass)
+    parsed.get.target should be(tar)
   }
 
   "Workflow Parser" should "parse a single may block" in {
     val s = "forallmay x,s O(x) → R += (x,s)"
-    val sig = Signature(List(Fun("O", List("x"))), List(Fun("R", List("x", "s"))))
-    testResult(s, Workflow(sig, List(ForallMayBlock(List("x", "s"), "choice0", List(Add(Fun("O", List("x")), "R", List("x", "s")))))))
+    
+    testResult(s, Workflow(oxrxssig, List(ForallMayBlock(List("x", "s"), "choice0", List(Add(Fun("O", List("x")), "R", List("x", "s")))))))
   }
 
   it should "parse a block with 2 stmts" in {
@@ -62,7 +65,7 @@ class ParserTest extends FlatSpec {
         O(x) → R += (x,s)
         (True ∧ O(s)) → R -= (s,x)
     """
-    testResult(s, Signature(List(Fun("O", List("x"))), List(Fun("R", List("x", "s")))))
+    testResult(s, oxrxssig)
   }
 
   it should "parse a loop block with 2 stmts" in {
@@ -70,12 +73,12 @@ class ParserTest extends FlatSpec {
       loop {
         forallmay x,s 
           O(x) → R += (x,s)
-          (True ∧ O(s)) → R -= (s,x)
-        forall y
-          O(y) → R += (y,y)
+          (True ∧ O(x)) → R -= (s,x)
+        forall x
+          O(x) → R += (x,x)
       }
     """
-    testResult(s, Signature(List(Fun("O", List("s"))), List(Fun("R", List("x", "s")))))
+    testResult(s, oxrxssig)
   }
 
   it should "parse prevexample" in {
@@ -88,8 +91,8 @@ class ParserTest extends FlatSpec {
       """
     val w = Workflow(
       Signature(
-        List(Fun("O", List("s"))),
-        List(
+        Set(Fun("O", List("s"))),
+        Set(
           Fun("S", List("x", "y", "s")),
           Fun("R", List("y", "s")),
           Fun("Q", List("x", "s")))),
@@ -108,15 +111,13 @@ class ParserTest extends FlatSpec {
   it should "parse simplechoice" in {
     val s = """
       forallmay x,s
-	      O(s) -> R += (x,s)
+	      O(x) -> R += (x,s)
       """
     val w = Workflow(
-      Signature(
-        List(Fun("O", List("s"))),
-        List(Fun("R", List("x", "s")))),
+      oxrxssig,
       List(
         ForallMayBlock(List("x", "s"), "choice0",
-          Add(Fun("O", "s"), "R", List("x", "s")))))
+          Add(Fun("O", "x"), "R", List("x", "s")))))
 
     testResult(s, w)
   }
@@ -124,15 +125,13 @@ class ParserTest extends FlatSpec {
   it should "parse simpleNochoice" in {
     val s = """
       forallmay x,s
-	      O(s) -> R += (x,s)
+	      O(x) -> R += (x,s)
       """
     val w = Workflow(
-      Signature(
-        List(Fun("O", List("s"))),
-        List(Fun("R", List("x", "s")))),
+      oxrxssig,
       List(
         ForallMayBlock(List("x", "s"), "choice0",
-          Add(Fun("O", "s"), "R", List("x", "s")))))
+          Add(Fun("O", "x"), "R", List("x", "s")))))
 
     testResult(s, w)
   }
@@ -146,19 +145,45 @@ class ParserTest extends FlatSpec {
 	      
 	    Target
 	    
-	    (R(x,s) ∧ O(x))
+	    R(x,s)
       """
     val w = Workflow(
       Signature(
-        List(Fun("O", List("s"))),
-        List(Fun("R", List("x", "s")))),
+        Set(Fun("O", List("s"))),
+        Set(Fun("R", List("x", "s")))),
       List(
         ForallMayBlock(List("x", "s"), "choice0",
           Add(Fun("O", "s"), "R", List("x", "s")))))
 
-    val t = And(Fun("R", List("x", "s")), Fun("O", List("x")))
+    val t = Fun("R", List("x", "s"))
+
+    testSpecResult(s, w, True, t)
+  }
+  
+  it should "parse simpleNochoice with declassification" in {
+    val s = """
+      Workflow
+      
+      forallmay x,s
+	      O(x) -> R += (x,s)
+	      
+	    Declassify
+	    
+	    O(x)
+	      
+	    Target
+	    
+	    R(x,s)
+      """
+    val w = Workflow(
+      oxrxssig,
+      List(
+        ForallMayBlock(List("x", "s"), "choice0",
+          Add(Fun("O", "x"), "R", List("x", "s")))))
+
+    val t = Fun("R", List("x", "s"))
 
-    testSpecResult(s, w, t)
+    testSpecResult(s, w, Fun("O", List("x")), t)
   }
 
 }
\ No newline at end of file