Commit 4351dd62 authored by Christian Müller's avatar Christian Müller

checker

parent e9d94f43
......@@ -102,7 +102,7 @@ object Main extends App with LazyLogging {
val inv = InvariantChecker.invariantNoninterStubborn(spec)
val (t,(safe, msg)) = time {
InvariantChecker.checkStubborn(spec.w, inv)
InvariantChecker.checkInvariant(spec.w, inv, true)
}
val noninter = s"Noninterference Invariant (took $t ms):\n$msg"
......@@ -131,5 +131,6 @@ object Main extends App with LazyLogging {
// clear()
// generateExample("omitting/conference")
generateAllExamples()
generateExample("tests/declasstest")
// generateAllExamples()
}
\ No newline at end of file
......@@ -19,55 +19,57 @@ import com.typesafe.scalalogging.LazyLogging
import de.tum.workflows.foltl.Properties
object InvariantChecker extends LazyLogging {
val TIMEOUT = 60000 // in milliseconds
def checkOnZ3(f:Formula) = {
// Set up Z3
val cfg = new HashMap[String, String]()
cfg.put("timeout", TIMEOUT.toString())
val ctx = new Context(cfg)
// val t = ctx.andThen(ctx.mkTactic("qe"), ctx.mkTactic("smt"))
val s = ctx.mkSolver()
s.add(toZ3.translate(f, ctx))
// Send to z3
val c = s.check()
if (c == Status.UNKNOWN) {
logger.info(s"Z3 status unknown: ${s.getReasonUnknown()}")
}
if (c == Status.SATISFIABLE) {
logger.info(s"Z3 model:\n${s.getModel()}")
}
(c, s)
def checkOnZ3(f: Formula) = {
// Set up Z3
val cfg = new HashMap[String, String]()
cfg.put("timeout", TIMEOUT.toString())
val ctx = new Context(cfg)
// val t = ctx.andThen(ctx.mkTactic("qe"), ctx.mkTactic("smt"))
val s = ctx.mkSolver()
s.add(toZ3.translate(f, ctx))
// Send to z3
val c = s.check()
if (c == Status.UNKNOWN) {
logger.info(s"Z3 status unknown: ${s.getReasonUnknown()}")
}
if (c == Status.SATISFIABLE) {
logger.info(s"Z3 model:\n${s.getModel()}")
}
(c, s)
}
def checkStubborn(w:Workflow, inv:Formula) = {
def checkInvariant(w: Workflow, inv: Formula, stubborn: Boolean) = {
// Build graph
val graph = Encoding.toGraph(w)
val msg = new StringBuilder()
msg ++= s"Trying to prove safe with invariant:\n\n${inv.pretty()}\n\n"
// Check all edges
val list = for (e <- graph.edges) yield {
// Check I -> WP[w](inv)
val b:SimpleBlock = e
val b: SimpleBlock = e
val precond = Preconditions.weakestPrecondition(inv, b)
// Stubborn agents -> remove trace variable from choice predicate
val stubprecond = precond.everywhere {
case Fun(f, i, p) if b.may && f == b.pred.get => Fun(f, p)
}
val stubprecond = if (stubborn) {
precond.everywhere {
case Fun(f, i, p) if b.may && f == b.pred.get => Fun(f, p)
}
} else precond
val f = Implies(inv, stubprecond)
logger.info(s"Checking invariant implication for ${e.label}")
val tocheck = Neg(f).simplify()
val (res, solver) = checkOnZ3(tocheck)
if (res != Status.UNSATISFIABLE) {
msg ++= s"Possibly unsafe: Block may not uphold invariant:\n\n${e.label}\n\n"
......@@ -84,7 +86,7 @@ object InvariantChecker extends LazyLogging {
}
res == Status.UNSATISFIABLE
}
val safe = list.reduceLeft(_ && _)
if (safe) {
msg ++= s"Proven safe.\n"
......@@ -92,25 +94,26 @@ object InvariantChecker extends LazyLogging {
}
(safe, msg)
}
def genEq(f:Fun, p:List[Var]) = {
def genEq(f: Fun, p: List[Var]) = {
val newf = f.parallelRename(f.params, p)
Eq(newf.in(T1), newf.in(T2))
}
def invariantNoninterStubborn(spec:Spec) = {
def invariantNoninterStubborn(spec: Spec) = {
val agent = spec.target.params(0)
val premise = And.make(for ((o,t) <- spec.declass) yield {
val premise = And.make(for ((o, t) <- spec.declass) yield {
// Forall fv(o). (t_T1 or t_t2) -> G (o_T1 <-> o_T2)
Forall(o.freeVars().toList, Implies(Or(t.in(T1), t.in(T2)), Eq(o.in(T1), o.in(T2))))
})
val conclusion = And.make(for (r <- spec.w.sig.preds.toList if r.params.head.typ == agent.typ) yield {
val quant = r.params.drop(1)
Forall(quant, genEq(r, agent::quant))
Forall(quant, genEq(r, agent :: quant))
})
Forall(agent, Implies(premise, conclusion)).simplify()
}
}
\ No newline at end of file
......@@ -20,7 +20,7 @@ class InvariantTest extends FlatSpec {
val inv = Forall(List("a", "b"), Eq(Fun("R", Some("t1"), List("a", "b")), Fun("R", Some("t2"), List("a", "b"))))
val (safe, msg) = InvariantChecker.checkStubborn(wf, inv)
val (safe, msg) = InvariantChecker.checkInvariant(wf, inv, true)
safe should be(true)
}
......@@ -31,7 +31,7 @@ class InvariantTest extends FlatSpec {
val inv = Forall(List("a", "b"), Eq(Fun("R", Some("t1"), List("a", "b")), Fun("R", Some("t2"), List("a", "b"))))
val (safe, msg) = InvariantChecker.checkStubborn(wf, inv)
val (safe, msg) = InvariantChecker.checkInvariant(wf, inv, true)
safe should be(false)
}
......@@ -60,7 +60,7 @@ class InvariantTest extends FlatSpec {
val inv = Forall(List(x),
Implies(premise, conclusion)
)
val (safe, msg) = InvariantChecker.checkStubborn(wf, inv)
val (safe, msg) = InvariantChecker.checkInvariant(wf, inv, true)
safe should be (true)
}
......@@ -76,7 +76,7 @@ class InvariantTest extends FlatSpec {
val spec = ExampleWorkflows.parseExample("tests/simpleChoice").get
val inv = InvariantChecker.invariantNoninterStubborn(spec)
val (safe, msg) = InvariantChecker.checkStubborn(spec.w, inv)
val (safe, msg) = InvariantChecker.checkInvariant(spec.w, inv, true)
safe should be(false)
}
......@@ -85,7 +85,7 @@ class InvariantTest extends FlatSpec {
val spec = ExampleWorkflows.parseExample("omitting/conference").get
val inv = InvariantChecker.invariantNoninterStubborn(spec)
val (safe, msg) = InvariantChecker.checkStubborn(spec.w, inv)
val (safe, msg) = InvariantChecker.checkInvariant(spec.w, inv,true)
safe should be(true)
}
......
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