Properties.scala 5.11 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 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94
  
    
  def buildViolations(vars:List[Var], t:Term, causals:List[Var]) = {
    val univ = causals.groupBy(_.typ).withDefault(_ => List())
    
    def build(agents:List[Var], t:Term):List[Term] = {
      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
      Forall(o.freeVars().toList, Implies(Or(t.in(T1), t.in(T2)), Globally(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 157 158 159
    
    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
    
    val nodes = nodepredicates(graph) map (_.name)
    val choices = allchoices(spec.w)
    
Christian Müller's avatar
Christian Müller committed
160
    val noninter = Noninterference(choices, spec)
Christian Müller's avatar
Christian Müller committed
161
    
Christian Müller's avatar
Christian Müller committed
162 163 164 165 166 167 168 169 170
    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
171
    })
Christian Müller's avatar
Christian Müller committed
172
    val agentmodel = Exists(spec.causals, And.make(stubs, causals, noninter))
Christian Müller's avatar
Christian Müller committed
173 174
    
    // maybe add exists t1, t2. phi?
Christian Müller's avatar
Christian Müller committed
175
    And.make(cfg, sem.in(t1, nodes), sem.in(t2, nodes), agentmodel)
Christian Müller's avatar
Christian Müller committed
176
  }
Christian Müller's avatar
Christian Müller committed
177
}