Properties.scala 3.59 KB
Newer Older
Christian Müller's avatar
Christian Müller committed
1 2 3 4
package de.tum.workflows.foltl

import de.tum.workflows.Implicits._
import de.tum.workflows.Encoding._
5
import de.tum.workflows.blocks._
Christian Müller's avatar
Christian Müller committed
6 7
import de.tum.workflows.foltl.FOLTL._
import de.tum.workflows.Utils._
Christian Müller's avatar
Christian Müller committed
8
import com.typesafe.scalalogging.LazyLogging
Christian Müller's avatar
Christian Müller committed
9

10 11 12
object Stubborn {
  def apply(agent: Var, choices: Set[Fun], t1: String, t2: String) = {
    And.make(for (c <- choices toList) yield {
Christian Müller's avatar
Christian Müller committed
13
      val f = c.updatedParams(0, agent)
14 15 16 17 18 19 20
    	Globally(
    	  Forall(c.params.drop(1), Eq(f.in(t1), f.in(t2)))    
   		)
    })
  }
}

Christian Müller's avatar
Christian Müller committed
21 22
object Causal {
  def apply(agent: Var, inputs: Set[Fun], outputs: Set[Fun], t1: String, t2: String) = {
23
    
Christian Müller's avatar
Christian Müller committed
24 25 26 27
    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)))                    
    }
28
    
Christian Müller's avatar
Christian Müller committed
29 30 31 32 33 34 35
    // FIXME
    // bind maximum # per type
    val types = outputs.flatMap(_.params.map(_.typ))
    val tobind = for (t <- types) yield {
      val count = outputs.map(_.params.count(_.typ == t)).max
      (t -> count) 
    }
Christian Müller's avatar
Christian Müller committed
36
    
Christian Müller's avatar
Christian Müller committed
37
    val vexist = (for ((t,count) <- tobind; num <- 1 until count) yield { Var(s"causal$agent$t$num", t) }) toList
38 39
    val agents = agent :: vexist
    
Christian Müller's avatar
Christian Müller committed
40
    val violations = for (o <- outputs toList) yield {
41
      val newo = o.updatedParams(agents.take(o.params.length))
Christian Müller's avatar
Christian Müller committed
42
      Neg(Eq(newo.in(t1), newo.in(t2)))
43 44
    }
    
Christian Müller's avatar
Christian Müller committed
45 46 47 48 49 50 51 52 53 54
    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")
    }
55
    
Christian Müller's avatar
Christian Müller committed
56 57
    val agent = spec.target.params(0)
    val samechoices = Stubborn(agent, choices, t1, t2)
58
    
Christian Müller's avatar
Christian Müller committed
59 60 61 62 63 64 65 66 67
    // 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))))
68 69 70
  }
}

Christian Müller's avatar
Christian Müller committed
71 72
object Properties {
  
73
  // include optimizations for choices
Christian Müller's avatar
Christian Müller committed
74
  def noninterStubborn(spec: Spec) = {
Christian Müller's avatar
Christian Müller committed
75 76 77 78
    
    val t1 = "t1"
    val t2 = "t2"
    
Christian Müller's avatar
Christian Müller committed
79
    val graph = toGraph(spec.w)
80
    val cfg = sanecfg(graph)
Christian Müller's avatar
Christian Müller committed
81
    val sem = exec(spec.w.sig, graph)
82

Christian Müller's avatar
Christian Müller committed
83
    val agents = spec.target freeVars() toList
Christian Müller's avatar
Christian Müller committed
84
    
85 86
    // choice and node predicates are equal in both runs (stubborn)
    val nodes = nodepredicates(graph) map (_.name)
Christian Müller's avatar
Christian Müller committed
87
    val choices = allchoices(spec.w) map (_.name)
88
    val equals = nodes ++ choices
Christian Müller's avatar
Christian Müller committed
89
    
Christian Müller's avatar
Christian Müller committed
90
    val noninter = Exists(agents, Finally(Neg(Eq(spec.target.in(t1), spec.target.in(t2)))))
Christian Müller's avatar
Christian Müller committed
91
    
92
    // maybe add exists t1, t2. phi?
93
    And.make(cfg, sem.in(t1, equals), sem.in(t2, equals), noninter)
Christian Müller's avatar
Christian Müller committed
94
  }
Christian Müller's avatar
Christian Müller committed
95
  
Christian Müller's avatar
Christian Müller committed
96
  def noninterCausal(spec:Spec) = {
Christian Müller's avatar
Christian Müller committed
97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112
    
    val t1 = "t1"
    val t2 = "t2"
    
    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)
    
Christian Müller's avatar
Christian Müller committed
113
    val causal = And.make(for (a <- spec.causals) yield {
Christian Müller's avatar
Christian Müller committed
114 115 116 117 118 119
      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)
  }
Christian Müller's avatar
Christian Müller committed
120
}