Properties.scala 3.5 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
    
29
    val max = outputs.map(_.params.length).max
Christian Müller's avatar
Christian Müller committed
30 31
    
    // TODO: Add correct types
32 33 34
    val vexist = (for (num <- 1 until max) yield { Var(s"causalce$num") }) toList
    val agents = agent :: vexist
    
Christian Müller's avatar
Christian Müller committed
35
    val violations = for (o <- outputs toList) yield {
36
      val newo = o.updatedParams(agents.take(o.params.length))
Christian Müller's avatar
Christian Müller committed
37
      Neg(Eq(newo.in(t1), newo.in(t2)))
38 39
    }
    
Christian Müller's avatar
Christian Müller committed
40 41 42 43 44 45 46 47 48 49
    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")
    }
50
    
Christian Müller's avatar
Christian Müller committed
51 52
    val agent = spec.target.params(0)
    val samechoices = Stubborn(agent, choices, t1, t2)
53
    
Christian Müller's avatar
Christian Müller committed
54 55 56 57 58 59 60 61 62
    // 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))))
63 64 65
  }
}

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

Christian Müller's avatar
Christian Müller committed
78
    val agents = spec.target freeVars() toList
Christian Müller's avatar
Christian Müller committed
79
    
80 81
    // 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
82
    val choices = allchoices(spec.w) map (_.name)
83
    val equals = nodes ++ choices
Christian Müller's avatar
Christian Müller committed
84
    
Christian Müller's avatar
Christian Müller committed
85
    val noninter = Exists(agents, Finally(Neg(Eq(spec.target.in(t1), spec.target.in(t2)))))
Christian Müller's avatar
Christian Müller committed
86
    
87
    // maybe add exists t1, t2. phi?
88
    And.make(cfg, sem.in(t1, equals), sem.in(t2, equals), noninter)
Christian Müller's avatar
Christian Müller committed
89
  }
Christian Müller's avatar
Christian Müller committed
90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116
  
  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
117
}