Properties.scala 5.07 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]) = {
Christian Müller's avatar
Christian Müller committed
13
    And.make(for (c <- choices.toList if c.params(0).typ == agent.typ) 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 24

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

object Noninterference extends LazyLogging {
Christian Müller's avatar
Christian Müller committed
68 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:Spec) = {
96
    
Christian Müller's avatar
Christian Müller committed
97
    val agent = spec.target.params(0)
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(Eq(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 110 111 112
object Declassification extends {
  def apply(spec: Spec) = {
    val sameoracles = for ((o,t) <- spec.declass) yield {
      // Forall fv(o). (t_T1 and t_t2) -> G (o_T1 <-> o_T2) 
Christian Müller's avatar
Christian Müller committed
113
      Globally(Forall(o.freeVars().toList, Implies(Or(t.in(T1), t.in(T2)), Eq(o.in(T1), o.in(T2)))))
114 115 116 117 118
    }
    And.make(sameoracles)
  }
}

Christian Müller's avatar
Christian Müller committed
119 120
object Properties {
  
Christian Müller's avatar
Christian Müller committed
121 122 123
  val T1 = "t1"
  val T2 = "t2"
  
124
  // include optimizations for choices
Christian Müller's avatar
Christian Müller committed
125
  def noninterStubborn(spec: Spec) = {
Christian Müller's avatar
Christian Müller committed
126
    
Christian Müller's avatar
Christian Müller committed
127
    val graph = toGraph(spec.w)
128
    val cfg = sanecfg(graph)
Christian Müller's avatar
Christian Müller committed
129
    val sem = exec(spec.w.sig, graph)
130

Christian Müller's avatar
Christian Müller committed
131
    val agents = spec.target freeVars() toList
Christian Müller's avatar
Christian Müller committed
132
    
133 134
    // 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
135
    val choices = allchoices(spec.w) map (_.name)
136
    val equals = nodes ++ choices
Christian Müller's avatar
Christian Müller committed
137
    
138 139 140
    val decl = Declassification(spec)
    
    val noninter = Exists(agents, And(decl, Finally(Neg(Eq(spec.target.in(T1), spec.target.in(T2))))))
Christian Müller's avatar
Christian Müller committed
141
    
142
    // maybe add exists t1, t2. phi?
Christian Müller's avatar
Christian Müller committed
143
    And.make(cfg, sem.in(T1, equals), sem.in(T2, equals), noninter)
Christian Müller's avatar
Christian Müller committed
144
  }
Christian Müller's avatar
Christian Müller committed
145
  
Christian Müller's avatar
Christian Müller committed
146
  def noninterCausal(spec:Spec) = {
Christian Müller's avatar
Christian Müller committed
147 148 149 150 151 152 153 154 155 156
    
    val graph = toGraph(spec.w)
    val cfg = sanecfg(graph)
    val sem = exec(spec.w.sig, graph)

    val agents = spec.target freeVars() toList
    
    val nodes = nodepredicates(graph) map (_.name)
    val choices = allchoices(spec.w)
    
Christian Müller's avatar
Christian Müller committed
157
    val noninter = Noninterference(choices, spec)
Christian Müller's avatar
Christian Müller committed
158
    
Christian Müller's avatar
Christian Müller committed
159 160 161 162 163 164 165 166 167
    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
168
    })
Christian Müller's avatar
Christian Müller committed
169
    val agentmodel = Exists(spec.causals, And.make(stubs, causals, noninter))
Christian Müller's avatar
Christian Müller committed
170 171
    
    // maybe add exists t1, t2. phi?
Christian Müller's avatar
Christian Müller committed
172
    And.make(cfg, sem.in(T1, nodes), sem.in(T2, nodes), agentmodel)
Christian Müller's avatar
Christian Müller committed
173
  }
Christian Müller's avatar
Christian Müller committed
174
}