Commit f5463307 authored by Christian Müller's avatar Christian Müller

improve types

parent 9840f81e
......@@ -14,3 +14,7 @@ loop {
Target
Read(xa:A, xb:A, p:P, r:R)
Causality
a:A
Workflow
forallmay x,p
forallmay x:A,p:P
True -> Conf += (x,p)
forallmay x,p
}
forallmay x:A,p:P
!Conf(x,p) -> Ass += (x,p)
forallmay x,p
forallmay x:A,p:P
(Ass(x,p) ∧ O(x,p)) -> Acc += (x,p)
loop {
forall xa,xb,p (A(xa,p) ∧ Acc(xb,p)) -> Read += (xa,xb,p)
forallmay x,p (A(x,p) ∧ O(x,p)) -> Acc += (x,p)
forall xa:X,xb:X,p:P (A(xa,p) ∧ Acc(xb,p)) -> Read += (xa,xb,p)
forallmay x:X,p:P (A(x,p) ∧ O(x,p)) -> Acc += (x,p)
}
Declassify
......@@ -17,4 +18,4 @@ Declassify
Target
Read(xa,xb,p)
Read(xa:X,xb:X,p:P)
Workflow
forallmay x,p
forallmay x:X,p:P
True -> Conf += (x,p)
forallmay x,p
forallmay x:X,p:P
!Conf(x,p) -> Ass += (x,p)
forall x,p,r
}
forall x:X,p:P,r:R
(Ass(x,p) ∧ O(p,r)) -> Read += (x,p,r)
forallmay y,x,p
forallmay y:Y,x:X,p:P
(Ass(x,p) ∧ Ass(y,p)) -> Comm += (x,y,p)
Declassify
¬ Conf(x,p)
¬ Conf(x:X,p:P)
Target
Comm(x, y, p)
Comm(x:X, y:X, p:P)
Workflow
forall x:X,s:S
O(s) -> R += (x,s)
Target
R(x:X,s:S)
Workflow
forall x:A,s:S
forall x,s
O(s) -> R += (x,s)
Target
R(x:A,s:S)
R(x,s)
......@@ -16,6 +16,7 @@ import de.tum.workflows.blocks.Spec
object Main extends App with LazyLogging {
val MAXAGENTS = 5
val FOLDER = "results"
def generateExample(name: String) {
logger.info(s"Generating $name")
......@@ -47,8 +48,8 @@ object Main extends App with LazyLogging {
val quantfree = LTL.eliminateUniversals(res, agents)
val ltlprop = LTL.eliminatePredicates(quantfree)
write(s"${name}_${agents.size}agents.ltl", ltlprop.toString())
write(s"${name}_${agents.size}agents.ppltl", ltlprop.pretty())
write(s"${name}_size${agents.size}.ltl", ltlprop.toString())
write(s"${name}_size${agents.size}.ppltl", ltlprop.pretty())
logger.info(s"Written all files for $name")
}
......@@ -62,11 +63,19 @@ object Main extends App with LazyLogging {
val prop = Properties.noninterStubborn(spec)
writeExample(s"results/${name}_stubborn", prop)
logger.info(s"Computing noninterference for target ${spec.target} using a single causal agent")
val cprop = Properties.noninterCausal(spec, 1)
writeExample(s"results/${name}_causal", cprop)
if (!spec.causals.isEmpty) {
logger.info(s"Computing noninterference for target ${spec.target} using causal agents ${spec.causals}")
val cprop = Properties.noninterCausal(spec)
writeExample(s"$FOLDER/${name}_causal", cprop)
}
}
// Clear results folder
val folder = new File(FOLDER)
folder.mkdirs()
folder.listFiles().foreach(_.delete())
// Fill results
for ((k, value) <- ExampleWorkflows.examples) {
generateExample(k)
}
......
......@@ -153,7 +153,13 @@ object WorkflowParser extends RegexParsers with LazyLogging {
}
}
def SPEC = "Workflow" ~! WORKFLOW ~ (("Declassify" ~> TERM)?) ~ ("Target" ~> FUN) ^^ { case _ ~ w ~ decl ~ tar => Spec(w, decl.getOrElse(True), tar) }
def SPEC =
"Workflow" ~! WORKFLOW ~
(("Declassify" ~> TERM)?) ~
("Target" ~> FUN) ~
(("Causality" ~> repsep(TYPEDVAR, ","))?) ^^ {
case _ ~ w ~ decl ~ tar ~ causals => Spec(w, decl.getOrElse(True), tar, causals.getOrElse(List()))
}
def parseWorkflow(s: String) = parseAll(WORKFLOW, s)
def parseSpec(s: String) = parseAll(SPEC, s)
......
......@@ -14,13 +14,13 @@ object Workflow {
val EMPTY = Workflow(Signature.EMPTY, List())
}
case class Spec(w: Workflow, declass: Term, target: Fun) {
case class Spec(w: Workflow, declass: Term, target: Fun, causals:List[Var]) {
override def toString = {
s"Spec\nWorkflow:\n$w\nDeclass:$declass\nTarget:$target"
}
}
object Spec {
val EMPTY = Spec(Workflow.EMPTY, True, Fun("NOTHING", List()))
val EMPTY = Spec(Workflow.EMPTY, True, Fun("NOTHING", List()), List())
}
abstract sealed class Block
......
......@@ -26,10 +26,15 @@ object Causal {
Forall(c.params.drop(1), Eq(newc.in(t1), newc.in(t2)))
}
val max = outputs.map(_.params.length).max
// FIXME
// bind maximum # per type
val types = outputs.flatMap(_.params.map(_.typ))
val tobind = for (t <- types) yield {
val count = outputs.map(_.params.count(_.typ == t)).max
(t -> count)
}
// TODO: Add correct types
val vexist = (for (num <- 1 until max) yield { Var(s"causalce$num") }) toList
val vexist = (for ((t,count) <- tobind; num <- 1 until count) yield { Var(s"causal$agent$t$num", t) }) toList
val agents = agent :: vexist
val violations = for (o <- outputs toList) yield {
......@@ -88,13 +93,11 @@ object Properties {
And.make(cfg, sem.in(t1, equals), sem.in(t2, equals), noninter)
}
def noninterCausal(spec:Spec, causalNum: Int) = {
def noninterCausal(spec:Spec) = {
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)
......@@ -107,7 +110,7 @@ object Properties {
val noninter = Noninterference(choices, spec, t1, t2)
val causal = And.make(for (a <- causals) yield {
val causal = And.make(for (a <- spec.causals) yield {
Exists(a, Causal(a, choices, spec.w.sig.preds, t1, t2))
})
......
......@@ -27,7 +27,7 @@ object LTL extends LazyLogging {
def eliminateExistentials(t:Term) = {
def coll:PartialFunction[Term, List[Var]] = {
case Exists(a, term) => List.concat(a, term.collect(coll))
case Exists(a, term) => a ++ term.collect(coll)
// don't go over Foralls
case Forall(_, _) => List.empty
// don't go over Globally
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment