LTLProperties.scala 5.69 KB
Newer Older
1
package de.tum.niwo.foltl
Christian Müller's avatar
Christian Müller committed
2

3
import de.tum.niwo.Implicits._
4

5
import de.tum.niwo.foltl.LTLEncoding._
6 7 8
import de.tum.niwo.blocks._
import de.tum.niwo.foltl.FOLTL._
import de.tum.niwo.Utils._
Christian Müller's avatar
Christian Müller committed
9
import com.typesafe.scalalogging.LazyLogging
Christian Müller's avatar
Christian Müller committed
10
import Properties._
Christian Müller's avatar
Christian Müller committed
11

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

Christian Müller's avatar
Christian Müller committed
23
object Causal {
Christian Müller's avatar
Christian Müller committed
24 25

  def apply(agent: Var, others:List[Var], inputs: Set[Fun], outputs: Set[Fun]) = {
26
    
Christian Müller's avatar
Christian Müller committed
27
    val equalchoices = for (c <- inputs.toList if c.params.head.typ == agent.typ) yield {
Christian Müller's avatar
Christian Müller committed
28
      val newc = c.updatedParams(0, agent)
Christian Müller's avatar
Christian Müller committed
29
      Forall(c.params.drop(1), Equiv(newc.in(T1), newc.in(T2)))
Christian Müller's avatar
Christian Müller committed
30
    }
31
    
Christian Müller's avatar
Christian Müller committed
32
    val noutputs = outputs.filter(_.params.head.typ == agent.typ)
Christian Müller's avatar
Christian Müller committed
33 34
    
    val types = noutputs.flatMap(_.params.map(_.typ))
Christian Müller's avatar
Christian Müller committed
35
    val tobind = (for (t <- types) yield {
Christian Müller's avatar
Christian Müller committed
36
      val count = noutputs.map(_.params.drop(1).count(_.typ == t)).max
Christian Müller's avatar
Christian Müller committed
37 38 39 40 41 42 43 44 45
      
      val list = for (num <- 1 to count) yield {
         Var(s"causal$agent$t$num", t) 
      }
      
      (t -> list) 
    }) toMap
    
    val vexist = tobind.flatMap(_._2) toList
46
    
Christian Müller's avatar
Christian Müller committed
47
    val violations = for (o <- noutputs toList) yield {
Christian Müller's avatar
Christian Müller committed
48
      val counters: Map[String, Int] = Map().withDefault(_ => 0)
Christian Müller's avatar
Christian Müller committed
49 50 51 52 53 54 55 56
        
        // 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)
Christian Müller's avatar
Christian Müller committed
57
        val t = Neg(Equiv(newo.in(T1), newo.in(T2)))
Christian Müller's avatar
Christian Müller committed
58 59
        
        Noninterference.buildViolations(agents, t, others)
60 61
    }
    
Christian Müller's avatar
Christian Müller committed
62 63 64
    val viol = violations.flatten
    
    WUntil(And.make(equalchoices), Exists(vexist, Or.make(viol)))    
Christian Müller's avatar
Christian Müller committed
65 66 67 68
  }
}

object Noninterference extends LazyLogging {
Christian Müller's avatar
Christian Müller committed
69

70
  def buildViolations(vars:List[Var], t:Formula, causals:List[Var]) = {
Christian Müller's avatar
Christian Müller committed
71 72
    val univ = causals.groupBy(_.typ).withDefault(_ => List())
    
73
    def build(agents:List[Var], t:Formula):List[Formula] = {
Christian Müller's avatar
Christian Müller committed
74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94
      agents match {
        
        case x::xs => {
          
          val terms = build(xs, t)
          val replacements = for (tt <- terms; a <- univ(x.typ)) yield {
            tt.everywhere({
              case f:Fun => f.updatedParams(f.params.map(p => if (p == x) a else p))
            })
          }
          replacements ++ terms
        }
        case List() => List(t)
      }
    }
    
    // equality with causals
    val viol = build(vars, t)
    Or.make(viol)
  }
  
Christian Müller's avatar
Christian Müller committed
95
  def apply(choices: Set[Fun], spec:NISpec) = {
96
    
Christian Müller's avatar
Christian Müller committed
97
    val agent = spec.target.params.head
Christian Müller's avatar
Christian Müller committed
98
    val samechoices = Stubborn(agent, choices)
99
    
100
    val decl = Declassification(spec)
Christian Müller's avatar
Christian Müller committed
101
    
Christian Müller's avatar
Christian Müller committed
102
    val difference = Neg(Equiv(spec.target.in(T1), spec.target.in(T2)))
Christian Müller's avatar
Christian Müller committed
103 104 105
    val diff = buildViolations(spec.target.params.drop(1), difference, spec.causals)
    
    Exists(agent, And.make(samechoices, decl, Finally(Exists(spec.target.params.drop(1), diff))))
106 107 108
  }
}

109
object Declassification extends {
Christian Müller's avatar
Christian Müller committed
110
  def apply(spec: NISpec) = {
Christian Müller's avatar
Christian Müller committed
111 112
    val sameoracles = for ((o,(p,t)) <- spec.declass) yield {
      val fun = Fun(o, None, p)
113
      // Forall fv(o). (t_T1 and t_t2) -> G (o_T1 <-> o_T2) 
Christian Müller's avatar
Christian Müller committed
114
      Globally(Forall(p, Implies(Or(t.in(T1), t.in(T2)), Equiv(fun.in(T1), fun.in(T2)))))
115
    }
Christian Müller's avatar
Christian Müller committed
116
    And.make(sameoracles.toList)
117 118 119
  }
}

Christian Müller's avatar
Christian Müller committed
120 121
object Properties {
  
Christian Müller's avatar
Christian Müller committed
122 123
  val T1 = "t1"
  val T2 = "t2"
Christian Müller's avatar
Christian Müller committed
124
  val INFNAME = "informed"
125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142

  def singletrace(spec:InvariantSpec): Formula = {
    import de.tum.niwo.graphs.TSGraphEncoding._

    val graph = toGraph(spec.ts)
    val cfg = sanecfg(graph)

    // TODO: this still believes the graph is a WFGraph
    val sem = exec(spec.ts.sig, graph)

    val empties = spec.ts.sig.preds.map( pred => Forall(pred.params, Neg(pred)) )
    val emptyaxiom = And.make(empties.toList)

    val inv = Finally(Neg(spec.inv))

    And.make(cfg, sem, emptyaxiom, spec.axioms, inv)

  }
Christian Müller's avatar
Christian Müller committed
143
  
144
  // include optimizations for choices
145 146
  def noninterStubborn(spec: NISpec): Formula = {
    import de.tum.niwo.graphs.WFGraphEncoding._
Christian Müller's avatar
Christian Müller committed
147
    
Christian Müller's avatar
Christian Müller committed
148
    val graph = toGraph(spec.w)
149
    val cfg = sanecfg(graph)
Christian Müller's avatar
Christian Müller committed
150
    val sem = exec(spec.w.sig, graph)
151

Christian Müller's avatar
Christian Müller committed
152
    val agents = spec.target.freeVars.toList
Christian Müller's avatar
Christian Müller committed
153
    
154 155
    // 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
156
    val choices = allchoices(spec.w) map (_.name)
157
    val equals = nodes ++ choices
Christian Müller's avatar
Christian Müller committed
158
    
159 160
    val decl = Declassification(spec)
    
Christian Müller's avatar
Christian Müller committed
161
    val noninter = Exists(agents, And(decl, Finally(Neg(Equiv(spec.target.in(T1), spec.target.in(T2))))))
Christian Müller's avatar
Christian Müller committed
162
    
163
    // maybe add exists t1, t2. phi?
Christian Müller's avatar
Christian Müller committed
164
    And.make(cfg, sem.in(T1, equals), sem.in(T2, equals), noninter)
Christian Müller's avatar
Christian Müller committed
165
  }
Christian Müller's avatar
Christian Müller committed
166
  
167 168
  def noninterCausal(spec:NISpec): Formula = {
    import de.tum.niwo.graphs.WFGraphEncoding._
Christian Müller's avatar
Christian Müller committed
169 170 171 172 173
    
    val graph = toGraph(spec.w)
    val cfg = sanecfg(graph)
    val sem = exec(spec.w.sig, graph)

Christian Müller's avatar
Christian Müller committed
174
    val agents = spec.target.freeVars.toList
Christian Müller's avatar
Christian Müller committed
175 176 177 178
    
    val nodes = nodepredicates(graph) map (_.name)
    val choices = allchoices(spec.w)
    
Christian Müller's avatar
Christian Müller committed
179
    val noninter = Noninterference(choices, spec)
Christian Müller's avatar
Christian Müller committed
180
    
Christian Müller's avatar
Christian Müller committed
181 182 183 184 185 186 187 188 189
    val types = spec.w.sig.preds.flatMap(_.params).map(_.typ)
    
    val stubs = And.make(for (t <- types.toList) yield {
      val stuba = Var(s"typvar$t", t)
      ForallOtherThan(stuba, spec.causals, Stubborn(stuba, choices))
    })
    val causals = And.make(for (a <- spec.causals) yield {
      val others = spec.causals.filterNot(_ == a)
      Causal(a, others, choices, spec.w.sig.preds)
Christian Müller's avatar
Christian Müller committed
190
    })
Christian Müller's avatar
Christian Müller committed
191
    val agentmodel = Exists(spec.causals, And.make(stubs, causals, noninter))
Christian Müller's avatar
Christian Müller committed
192 193
    
    // maybe add exists t1, t2. phi?
Christian Müller's avatar
Christian Müller committed
194
    And.make(cfg, sem.in(T1, nodes), sem.in(T2, nodes), agentmodel)
Christian Müller's avatar
Christian Müller committed
195
  }
Christian Müller's avatar
Christian Müller committed
196
}