Properties.scala 3.82 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
import Properties._
Christian Müller's avatar
Christian Müller committed
10

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

Christian Müller's avatar
Christian Müller committed
22
object Causal {
Christian Müller's avatar
Christian Müller committed
23
  def apply(agent: Var, inputs: Set[Fun], outputs: Set[Fun]) = {
24
    
Christian Müller's avatar
Christian Müller committed
25 26
    val equalchoices = for (c <- inputs toList) yield {
      val newc = c.updatedParams(0, agent)
Christian Müller's avatar
Christian Müller committed
27
      Forall(c.params.drop(1), Eq(newc.in(T1), newc.in(T2)))                    
Christian Müller's avatar
Christian Müller committed
28
    }
29
    
Christian Müller's avatar
Christian Müller committed
30 31 32
    // FIXME
    // bind maximum # per type
    val types = outputs.flatMap(_.params.map(_.typ))
Christian Müller's avatar
Christian Müller committed
33 34 35 36 37 38 39 40 41 42 43
    val tobind = (for (t <- types) yield {
      val count = outputs.map(_.params.drop(1).count(_.typ == t)).max
      
      val list = for (num <- 1 to count) yield {
         Var(s"causal$agent$t$num", t) 
      }
      
      (t -> list) 
    }) toMap
    
    val vexist = tobind.flatMap(_._2) toList
44
    
Christian Müller's avatar
Christian Müller committed
45
    val violations = for (o <- outputs toList) yield {
Christian Müller's avatar
Christian Müller committed
46 47 48 49 50 51 52 53 54 55 56 57 58 59 60
      if (o.params.isEmpty || o.params.head.typ != agent.typ) {
        False
      } else {
        var counters:Map[String, Int] = Map().withDefault(_ => 0)
        
        // drop the first, since it is agent
        val agents = for (p <- o.params.drop(1); t = p.typ) yield {
          val variable = tobind(t)(counters(t))
          counters.updated(t, counters(t) + 1)
          variable
        }
        
        val newo = o.updatedParams(agent :: agents)
        Neg(Eq(newo.in(T1), newo.in(T2)))
      }
61 62
    }
    
Christian Müller's avatar
Christian Müller committed
63 64 65 66 67
    WUntil(And.make(equalchoices), Exists(vexist, Or.make(violations)))    
  }
}

object Noninterference extends LazyLogging {
Christian Müller's avatar
Christian Müller committed
68
  def apply(choices: Set[Fun], spec:Spec) = {
69
    
Christian Müller's avatar
Christian Müller committed
70
    val agent = spec.target.params(0)
Christian Müller's avatar
Christian Müller committed
71
    val samechoices = Stubborn(agent, choices)
72
    
Christian Müller's avatar
Christian Müller committed
73 74 75 76 77
    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)
Christian Müller's avatar
Christian Müller committed
78
    
Christian Müller's avatar
Christian Müller committed
79
    val difference = Neg(Eq(spec.target.in(T1), spec.target.in(T2)))
Christian Müller's avatar
Christian Müller committed
80

Christian Müller's avatar
Christian Müller committed
81
    Exists(agent, And.make(samechoices, decl, Finally(Exists(spec.target.params.drop(1), difference))))
82 83 84
  }
}

Christian Müller's avatar
Christian Müller committed
85 86
object Properties {
  
Christian Müller's avatar
Christian Müller committed
87 88 89
  val T1 = "t1"
  val T2 = "t2"
  
90
  // include optimizations for choices
Christian Müller's avatar
Christian Müller committed
91
  def noninterStubborn(spec: Spec) = {
Christian Müller's avatar
Christian Müller committed
92
    
Christian Müller's avatar
Christian Müller committed
93
    val graph = toGraph(spec.w)
94
    val cfg = sanecfg(graph)
Christian Müller's avatar
Christian Müller committed
95
    val sem = exec(spec.w.sig, graph)
96

Christian Müller's avatar
Christian Müller committed
97
    val agents = spec.target freeVars() toList
Christian Müller's avatar
Christian Müller committed
98
    
99 100
    // 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
101
    val choices = allchoices(spec.w) map (_.name)
102
    val equals = nodes ++ choices
Christian Müller's avatar
Christian Müller committed
103
    
Christian Müller's avatar
Christian Müller committed
104
    val noninter = Exists(agents, Finally(Neg(Eq(spec.target.in(T1), spec.target.in(T2)))))
Christian Müller's avatar
Christian Müller committed
105
    
106
    // maybe add exists t1, t2. phi?
Christian Müller's avatar
Christian Müller committed
107
    And.make(cfg, sem.in(T1, equals), sem.in(T2, equals), noninter)
Christian Müller's avatar
Christian Müller committed
108
  }
Christian Müller's avatar
Christian Müller committed
109
  
Christian Müller's avatar
Christian Müller committed
110
  def noninterCausal(spec:Spec) = {
Christian Müller's avatar
Christian Müller committed
111 112 113 114 115 116 117 118 119 120 121 122 123 124
    
    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)
    
Christian Müller's avatar
Christian Müller committed
125
    val noninter = Noninterference(choices, spec)
Christian Müller's avatar
Christian Müller committed
126
    
Christian Müller's avatar
Christian Müller committed
127
    val causal = And.make(for (a <- spec.causals) yield {
Christian Müller's avatar
Christian Müller committed
128
      Exists(a, Causal(a, choices, spec.w.sig.preds))
Christian Müller's avatar
Christian Müller committed
129 130 131 132 133
    })
    
    // 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
134
}