Properties.scala 3.33 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
    val vexist = outputs flatMap (_.params) toList
    val violations = for (o <- outputs toList) yield {
      val newo = o.updatedParams(0, agent)
      Neg(Eq(newo.in(t1), newo.in(t2)))
33 34
    }
    
Christian Müller's avatar
Christian Müller committed
35 36 37 38 39 40 41 42 43 44
    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")
    }
45
    
Christian Müller's avatar
Christian Müller committed
46 47
    val agent = spec.target.params(0)
    val samechoices = Stubborn(agent, choices, t1, t2)
48
    
Christian Müller's avatar
Christian Müller committed
49 50 51 52 53 54 55 56 57
    // 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))))
58 59 60
  }
}

Christian Müller's avatar
Christian Müller committed
61 62
object Properties {
  
63
  // include optimizations for choices
Christian Müller's avatar
Christian Müller committed
64
  def noninterStubborn(spec: Spec) = {
Christian Müller's avatar
Christian Müller committed
65 66 67 68
    
    val t1 = "t1"
    val t2 = "t2"
    
Christian Müller's avatar
Christian Müller committed
69
    val graph = toGraph(spec.w)
70
    val cfg = sanecfg(graph)
Christian Müller's avatar
Christian Müller committed
71
    val sem = exec(spec.w.sig, graph)
72

Christian Müller's avatar
Christian Müller committed
73
    val agents = spec.target freeVars() toList
Christian Müller's avatar
Christian Müller committed
74
    
75 76
    // 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
77
    val choices = allchoices(spec.w) map (_.name)
78
    val equals = nodes ++ choices
Christian Müller's avatar
Christian Müller committed
79
    
Christian Müller's avatar
Christian Müller committed
80
    val noninter = Exists(agents, Finally(Neg(Eq(spec.target.in(t1), spec.target.in(t2)))))
Christian Müller's avatar
Christian Müller committed
81
    
82
    // maybe add exists t1, t2. phi?
83
    And.make(cfg, sem.in(t1, equals), sem.in(t2, equals), noninter)
Christian Müller's avatar
Christian Müller committed
84
  }
Christian Müller's avatar
Christian Müller committed
85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111
  
  def noninterCausal(spec:Spec, causalNum: Int) = {
    
    val t1 = "t1"
    val t2 = "t2"
    
    val causals = (0 until causalNum) map (x => Var("causal" + x)) toList
    
    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)
    
    val causal = And.make(for (a <- causals) yield {
      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
112
}