Commit 9ff5c284 authored by Christian Müller's avatar Christian Müller

invariants

parent f11bbc0a
......@@ -13,11 +13,14 @@ import java.io.File
import de.tum.workflows.blocks.Workflow
import de.tum.workflows.blocks.Spec
import de.tum.workflows.foltl.FormulaFunctions
import de.tum.workflows.toz3.InvariantChecker
object Main extends App with LazyLogging {
val MAXAGENTS = 8
val FOLDER = "results"
val checkinvariants = true
def clear() {
def recclear(folder:File) {
......@@ -89,12 +92,24 @@ object Main extends App with LazyLogging {
logger.info(s"Computing noninterference for target ${spec.target} using only stubborn agents")
val prop = Properties.noninterStubborn(spec)
writeExample(s"results/${name}_stubborn", spec, prop)
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", spec, cprop)
}
if (checkinvariants) {
val inv = InvariantChecker.invariantNoninterStubborn(spec)
val (t,safe) = time {
InvariantChecker.checkStubborn(spec.w, inv)
}
val string = "Workflow " + (if(safe)"proven SAFE" else "possibly UNSAFE") + s" after $t ms for invariant:\n${inv.pretty}"
write(s"$FOLDER/${name}.inv", string)
}
}
def generateExample(name: String) {
......@@ -116,6 +131,7 @@ object Main extends App with LazyLogging {
}
}
clear()
generateExample("omitting/conference")
// clear()
// generateExample("omitting/conference")
generateAllExamples()
}
\ No newline at end of file
......@@ -25,5 +25,11 @@ object Utils {
def indentLines(s: String) = {
s.lines.map(" " + _).mkString("\n")
}
def time[R](block: => R) = {
val t0 = System.nanoTime()
val result = block // call-by-name
val t1 = System.nanoTime()
((t1 - t0)/1000000, result)
}
}
\ No newline at end of file
......@@ -167,7 +167,7 @@ object FOLTL {
object Or {
def make(terms: List[Formula]) = {
BinOp.makeL(Or.apply _, terms, True)
BinOp.makeL(Or.apply _, terms, False)
}
def make(terms: Formula*) = {
BinOp.makeL(Or.apply _, terms, False)
......
......@@ -110,7 +110,7 @@ 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)
Forall(o.freeVars().toList, Implies(Or(t.in(T1), t.in(T2)), Globally(Eq(o.in(T1), o.in(T2)))))
Globally(Forall(o.freeVars().toList, Implies(Or(t.in(T1), t.in(T2)), Eq(o.in(T1), o.in(T2)))))
}
And.make(sameoracles)
}
......
......@@ -7,6 +7,8 @@ import de.tum.workflows.Implicits._
import de.tum.workflows.WorkflowParser
import de.tum.workflows.Encoding
import de.tum.workflows.Preconditions
import de.tum.workflows.foltl.Properties.T1
import de.tum.workflows.foltl.Properties.T2
import scalax.collection.edge.LDiEdge // labeled directed edge
import com.microsoft.z3.Context
......@@ -14,6 +16,7 @@ import java.util.HashMap
import org.omg.CORBA.TIMEOUT
import com.microsoft.z3.Status
import com.typesafe.scalalogging.LazyLogging
import de.tum.workflows.foltl.Properties
object InvariantChecker extends LazyLogging {
......@@ -73,8 +76,29 @@ object InvariantChecker extends LazyLogging {
val safe = list.reduceLeft(_ && _)
if (safe) {
logger.info(s"Workflow $w proven safe for invariant $inv")
logger.info(s"Workflow $w\n proven safe for invariant:\n${inv.pretty()}")
}
safe
}
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) = {
val agent = spec.target.params(0)
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, And(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(agent, Implies(premise, conclusion))
}
}
\ No newline at end of file
......@@ -220,11 +220,18 @@ object toZ3 extends LazyLogging {
val e = toZ3(ctx, f1, texpr, tvar, var_ctx)
ctx.mkNot(e)
}
case True => {
ctx.mkTrue()
}
case False => {
ctx.mkFalse()
}
}
}
def translate(f: Formula, ctx: Context) = {
logger.info(s"Using formula:\n$f")
// logger.info(s"Using formula:\n$f")
if (!f.freeVars().isEmpty) {
logger.error(s"Cannot check - formula contains free variables ${f.freeVars()}")
......@@ -232,12 +239,12 @@ object toZ3 extends LazyLogging {
fun_ctx.clear()
val expr = toZ3(ctx, f, ctx.mkInt(0), None, Map())
logger.info(s"Built Z3 expression:\n$expr")
// logger.info(s"Built Z3 expression:\n$expr")
expr
}
def translate(f: Formula, ctx: Context, varctx: VarCtx) = {
logger.info(s"Using formula:\n${f.pretty()}")
// logger.info(s"Using formula:\n${f.pretty()}")
if (!f.freeVars().isEmpty) {
logger.error(s"Cannot check - formula contains free variables ${f.freeVars()}")
......@@ -245,7 +252,7 @@ object toZ3 extends LazyLogging {
fun_ctx.clear()
val expr = toZ3(ctx, f, ctx.mkInt(0), None, varctx)
logger.info(s"Built Z3 expression:\n$expr")
// logger.info(s"Built Z3 expression:\n$expr")
expr
}
}
......@@ -49,5 +49,23 @@ class InvariantTest extends FlatSpec {
safe should be (true)
}
it should "prove noninter invariants" in {
val spec = ExampleWorkflows.parseExample("tests/simpleChoice").get
val inv = InvariantChecker.invariantNoninterStubborn(spec)
val safe = InvariantChecker.checkStubborn(spec.w, inv)
safe should be (false)
}
it should "prove the paper example as noninter invariant"in {
val spec = ExampleWorkflows.parseExample("omitting/conference").get
val inv = InvariantChecker.invariantNoninterStubborn(spec)
val safe = InvariantChecker.checkStubborn(spec.w, inv)
safe should be (true)
}
}
\ No newline at end of file
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