Skip to content
GitLab
Commit 301bbee4 authored by Christian Müller's avatar Christian Müller
Browse files

add declass stuff

parent ebac74bf
Hide whitespace changes
Inline Side-by-side
src/main/scala/de/tum/workflows/Encoding.scala
View file @ 301bbee4
......@@ -194,6 +194,8 @@ object Encoding extends LazyLogging {
//
// And.make(List(cfg, sanity, sem, init))
// }
val MAXINVLENGTH = 1200
def toDot(g: WorkflowGraph)(labels:Map[WorkflowGraph#NodeT, String], edges:Set[g.EdgeT]) = {
val root = DotRootGraph(
......@@ -223,7 +225,7 @@ object Encoding extends LazyLogging {
}
def nodeTransformer(innerNode: WorkflowGraph#NodeT): Option[(DotGraph, DotNodeStmt)] = {
val str = labels(innerNode)
val label = if (str.length() > 1000) str.substring(0, 600) + "..." else str
val label = if (str.length() > MAXINVLENGTH) str.substring(0, MAXINVLENGTH) + "..." + s"(${str.length()} characters)" else str
Some((root, DotNodeStmt(innerNode.toString, List(DotAttr("label", "Node " + innerNode + ":\n" + label)))))
}
......
src/main/scala/de/tum/workflows/Preconditions.scala
View file @ 301bbee4
......@@ -8,16 +8,11 @@ import de.tum.workflows.foltl.FOLTL._
import de.tum.workflows.foltl.FormulaFunctions._
import de.tum.workflows.foltl.FormulaFunctions
import de.tum.workflows.ltl.FOTransformers
import de.tum.workflows.foltl.Properties._
object Preconditions extends LazyLogging {
val INFNAME = "informed"
val T1 = "t1"
val T2 = "t2"
def elaborateSteps(b:SimpleBlock, s:Spec) = {
val newsteps = (for (stmt <- b.steps) yield {
val first = stmt.tuple.head
if (first.typ == s.target.params.head.typ) {
......@@ -31,6 +26,30 @@ object Preconditions extends LazyLogging {
newsteps.flatten
}
def elaborateOraclyBlock(b:SimpleBlock, s:Spec) = {
if (b.isoracly) {
val stmt = b.steps.head // can only be one
def fixguard(f:Formula) = {
f.everywhere {
case f:Fun if f.isOracle() => True
}
}
def findOracle(f:Formula) = {
f.collect {
case f:Fun if (f.isOracle()) => List(f.name)
}
}
val name = findOracle(stmt.guard).head
val newstmt = stmt match {
case Add(guard, fun, tuple) => Add(fixguard(guard).simplify(), fun, tuple)
case Remove(guard, fun, tuple) => Remove(fixguard(guard).simplify(), fun, tuple)
}
ForallMayBlock(b.agents, name, List(newstmt))
} else b
}
def subst(f:Formula, updates: List[(String, (List[FOLTL.Var], FOLTL.Formula))], b:SimpleBlock) = {
updates.foldRight(f)((update, f) => {
......@@ -50,8 +69,9 @@ object Preconditions extends LazyLogging {
})
}
def weakestPrecondition(f: Formula, b: SimpleBlock, spec:Spec, stubborn:Boolean) = {
def weakestPrecondition(f: Formula, outerb: SimpleBlock, spec:Spec, stubborn:Boolean) = {
val b = elaborateOraclyBlock(outerb, spec)
// elaborate only if non-stubborn
val steps = if (stubborn) elaborateSteps(b, spec) else b.steps
......@@ -67,7 +87,12 @@ object Preconditions extends LazyLogging {
// Trace related substitution for informedness
// TODO: make switch on/off etc
val con = if (choice.isDefined) {
val con = if (outerb.isoracly) {
val decl = spec.declass.getOrElse(b.pred.get, (List(), False))._2
// FIXME: substitutions?
// FIXME: decl in T2?
Or(And(decl.in(T1), choice.get.in(T1)), And(Neg(decl.in(T1)), choice.get))
} else if (choice.isDefined) {
val inner = if (first.typ == spec.target.params.head.typ) {
val inf = Fun(INFNAME, List(s.tuple.head))
if (stubborn) {
......
src/main/scala/de/tum/workflows/WorkflowParser.scala
View file @ 301bbee4
......@@ -179,9 +179,15 @@ object WorkflowParser extends RegexParsers with LazyLogging {
(("Declassify" ~> DECLASS)?) ~
("Target" ~> FUN) ~
(("Causality" ~> repsep(TYPEDVAR, ","))?) ^^ {
case _ ~ w ~ decl ~ tar ~ causals => Spec(w, decl.toList, tar, causals.getOrElse(List()))
case _ ~ w ~ decl ~ tar ~ causals => Spec(w, toMap(decl.toList), tar, causals.getOrElse(List()))
}
def toMap(list:List[(Fun, Formula)]):Map[String, (List[Var], Formula)] = {
list.map { l =>
l._1.name -> (l._1.params, l._2)
} toMap
}
def parseWorkflow(s: String) = parseAll(WORKFLOW, s)
def parseSpec(s: String) = parseAll(SPEC, s)
def parseTerm(s:String) = parseAll(TERM, s)
......
src/main/scala/de/tum/workflows/blocks/Workflow.scala
View file @ 301bbee4
......@@ -19,7 +19,7 @@ object Workflow {
val EMPTY = Workflow(Signature.EMPTY, List())
}
case class Spec(w: Workflow, declass: List[(Fun, Formula)], target: Fun, causals:List[Var]) extends LazyLogging {
case class Spec(w: Workflow, declass: Map[String, (List[Var], Formula)], target: Fun, causals:List[Var]) extends LazyLogging {
override def toString = {
s"Spec\nWorkflow:\n$w\nDeclass:$declass\nTarget:$target"
}
......@@ -33,11 +33,23 @@ case class Spec(w: Workflow, declass: List[(Fun, Formula)], target: Fun, causals
val ta = target.params(0)
// check declass bindings
for ((o, t) <- declass if !t.freeVars().forall(v => (o.freeVars().contains(v) || (v == ta)))) {
for ((o, (f, t)) <- declass if !t.freeVars().forall(v => (f.contains(v) || (v == ta)))) {
logger.error(s"Not all variables of the declassification condition for $o bound by the oracle")
sane = false
}
def saneoraclestmt(stmt:Statement, frees:List[Var]) = {
// Oracle only positive
val f = stmt.guard.toNegNf()
val noneg = !(f hasSubFormula {
case Neg(f:Fun) if f.isOracle() => true
})
val allvars = f hasSubFormula {
case f:Fun if f.isOracle && f.params == frees => true
}
noneg && allvars
}
// check same relation only updated once per block
def isSane(steps:List[Block]):Boolean = {
val sanes = steps map {s =>
......@@ -48,7 +60,10 @@ case class Spec(w: Workflow, declass: List[(Fun, Formula)], target: Fun, causals
pred.map(p =>
logger.error(s"Predicate $p updated more than once in $b")
)
pred.isEmpty
// if using oracle, only single stmt
val saneoracly = if (b.isoracly) { b.pred.isEmpty && b.steps.size == 1 && saneoraclestmt(b.steps.head, b.agents) } else true
if (!saneoracly) { logger.error(s"Oracles used wrongly in $b") }
pred.isEmpty // && saneoracly TODO: enable this later?
}
case Loop(steps) => isSane(steps)
case NondetChoice(left, right) => isSane(left) && isSane(right)
......@@ -57,12 +72,11 @@ case class Spec(w: Workflow, declass: List[(Fun, Formula)], target: Fun, causals
sanes reduce (_ && _)
}
sane &&= isSane(w.steps)
sane
}
}
object Spec {
val EMPTY = Spec(Workflow.EMPTY, List(), Fun("NOTHING", List()), List())
val EMPTY = Spec(Workflow.EMPTY, Map(), Fun("NOTHING", List()), List())
}
abstract sealed class Block {
......@@ -79,6 +93,12 @@ abstract sealed class SimpleBlock extends Block {
// a simple block is omitting, if there exists a statement where not all agents appear in the tuple
steps.exists(s => agents.exists(a => !s.tuple.contains(a)))
}
def isoracly = {
steps.exists(s => s.guard.hasSubFormula {
case f:Fun => f.isOracle()
})
}
}
abstract class Statement {
......
src/main/scala/de/tum/workflows/foltl/FOLTL.scala
View file @ 301bbee4
......@@ -36,6 +36,7 @@ object FOLTL {
def ∧ (f2:Formula) = And(this, f2)
def ∨ (f2:Formula) = Or(this, f2)
// TODO: better line breaking
def pretty(): String = {
val remeq = this.everywhere {
case Eq(t1, t2) if FormulaFunctions.annotateOverwrite(t1, Properties.T1, Properties.T2) == t2 =>
......@@ -88,6 +89,9 @@ object FOLTL {
override def toString() = name + Utils.mkString(ind, "(", "", ")") + params.map(_.name).mkString("(", ",", ")")
def updatedParams(index: Int, p:Var) = Fun(name, ind, params.updated(index, p))
def updatedParams(list: List[Var]) = Fun(name, ind, list)
def isOracle() = name.startsWith("O")
def encodeToVar() = {
val pi = if (ind.isDefined) "#" + ind.get else ""
Var(name + pi + Utils.mkString(params, "_", "_", ""))
......
src/main/scala/de/tum/workflows/foltl/FormulaFunctions.scala
View file @ 301bbee4
......@@ -27,6 +27,7 @@ object FormulaFunctions extends LazyLogging {
free(t, Set())
}
@tailrec
def simplify(t: Formula): Formula = {
val simp: PartialFunction[Formula, Formula] = {
// Push negation inward
......@@ -101,8 +102,8 @@ object FormulaFunctions extends LazyLogging {
// make(qmake(xs, t1), t2)
}
val t1 = everywhere(simp, t)
if (t == t1) t1 else simplify(t1)
val (changed, t1) = everywhereFP(simp, t)
if (!changed) t1 else simplify(t1)
}
def eliminateImplication(f: Formula): Formula = {
......@@ -120,6 +121,29 @@ object FormulaFunctions extends LazyLogging {
}
}
}
def everywhereFP(trans: PartialFunction[Formula, Formula], t: Formula): (Boolean, Formula) = {
if (trans.isDefinedAt(t))
(true, trans(t))
else
t match {
// Extractors
case Quantifier(make, ps, t1) => {
val sub = everywhereFP(trans, t1)
(sub._1, make(ps, sub._2))
}
case UnOp(make, t1) => {
val sub = everywhereFP(trans, t1)
(sub._1, make(sub._2))
}
case BinOp(make, t1, t2) => {
val (c1, sub1) = everywhereFP(trans, t1)
val (c2, sub2) = everywhereFP(trans, t2)
(c1 || c2, make(sub1, sub2))
}
case x => (false, x)
}
}
def everywhere(trans: PartialFunction[Formula, Formula], t: Formula): Formula = {
if (trans.isDefinedAt(t))
......@@ -406,7 +430,8 @@ object FormulaFunctions extends LazyLogging {
val normalized = f.toNegNf().toPrenex().simplify()
// normalized is now Quantifiers, then only And/Or with Negation inside
toCNFSub(normalized).simplify()
// no simplification here
toCNFSub(normalized)
}
/**
......
src/main/scala/de/tum/workflows/foltl/Properties.scala
View file @ 301bbee4
......@@ -108,11 +108,12 @@ object Noninterference extends LazyLogging {
object Declassification extends {
def apply(spec: Spec) = {
val sameoracles = for ((o,t) <- spec.declass) yield {
val sameoracles = for ((o,(p,t)) <- spec.declass) yield {
val fun = Fun(o, None, p)
// Forall fv(o). (t_T1 and t_t2) -> G (o_T1 <-> o_T2)
Globally(Forall(o.freeVars().toList, Implies(Or(t.in(T1), t.in(T2)), Eq(o.in(T1), o.in(T2)))))
Globally(Forall(p.toList, Implies(Or(t.in(T1), t.in(T2)), Eq(fun.in(T1), fun.in(T2)))))
}
And.make(sameoracles)
And.make(sameoracles.toList)
}
}
......@@ -120,6 +121,7 @@ object Properties {
val T1 = "t1"
val T2 = "t2"
val INFNAME = "informed"
// include optimizations for choices
def noninterStubborn(spec: Spec) = {
......
src/main/scala/de/tum/workflows/ltl/FOTransformers.scala
View file @ 301bbee4
......@@ -53,7 +53,7 @@ object FOTransformers extends LazyLogging {
}
def eliminateAuxiliaryPredicate(f:Formula, AUX:String) = {
val cnf = f.toCNF().simplify()
val cnf = f.toCNF()
val quantifiers = FormulaFunctions.collectQuantifiers(cnf)
......
src/main/scala/de/tum/workflows/toz3/InvariantChecker.scala
View file @ 301bbee4
......@@ -16,46 +16,52 @@ import de.tum.workflows.blocks._
import de.tum.workflows.foltl.FOLTL._
import de.tum.workflows.foltl.FormulaFunctions
import de.tum.workflows.ltl.FOTransformers
import de.tum.workflows.Utils
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 qe = ctx.mkTactic("qe")
// val default = ctx.mkTactic("smt")
// val t = ctx.andThen(qe, default)
// val s = ctx.mkSolver(t)
val s = ctx.mkSolver()
// Can only check universal things
val neg = Neg(f).simplify()
// univfree is now in E*, so can be solved as SAT Problem
val stripped = FormulaFunctions.stripQuantifiers(neg)
// val prefix = FormulaFunctions.collectQuantifiersSub(univfree)
val satform = FOTransformers.eliminatePredicates(stripped)
// Checking QFree
s.add(Z3QFree.translate(satform, 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 status satisfiable")
// logger.info(s"${s.getModel()}")
val (time, res) = Utils.time {
// Set up Z3
val cfg = new HashMap[String, String]()
cfg.put("timeout", TIMEOUT.toString())
val ctx = new Context(cfg)
// val qe = ctx.mkTactic("qe")
// val default = ctx.mkTactic("smt")
// val t = ctx.andThen(qe, default)
// val s = ctx.mkSolver(t)
val s = ctx.mkSolver()
// Can only check universal things
val neg = Neg(f).simplify()
// univfree is now in E*, so can be solved as SAT Problem
val stripped = FormulaFunctions.stripQuantifiers(neg)
// val prefix = FormulaFunctions.collectQuantifiersSub(univfree)
val satform = FOTransformers.eliminatePredicates(stripped)
// Checking QFree
s.add(Z3QFree.translate(satform, 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 status satisfiable")
// logger.info(s"${s.getModel()}")
}
(c, s)
}
(c, s)
logger.info(s"Z3 call took $time ms")
res
}
def checkBlockInvariant(spec:Spec, b: SimpleBlock, pre: Formula, post: Formula, stubborn: Boolean, isfirst: Boolean) = {
......@@ -116,8 +122,16 @@ object InvariantChecker extends LazyLogging {
// --> unsafe, relabel incoming node, invalidate all proven guarantees for that node
// check if relabelled invariant still satisfiable
// never relabel initial node
logger.info(s"Invariant not inductive, strengthening")
if (!isfirst) {
val newinv = And(labels(next._1), Preconditions.abstractPrecondition(post, next, stubborn, spec)).simplify()
// check if strengthened -> old_inv else use conjunction
val strengthened = Preconditions.abstractPrecondition(post, next, stubborn, spec)
// val newinv = if (checkOnZ3(Implies(labels(next._1), strengthened))._1 == Status.SATISFIABLE) {
// And(labels(next._1), strengthened).simplify()
// } else {
// strengthened.simplify()
// }
val newinv = And(labels(next._1), strengthened).simplify()
val (status2, solver2) = checkOnZ3(Implies(newinv, False))
......
src/main/scala/de/tum/workflows/toz3/InvariantGenerator.scala
View file @ 301bbee4
......@@ -15,53 +15,51 @@ object InvariantGenerator {
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, 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(agent, premise → conclusion).simplify()
}
// 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, 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(agent, premise → conclusion).simplify()
// }
def invariantNoninterStubbornSingleBS(spec: Spec) = {
val agent = spec.target.params(0)
val premise = for ((o, t) <- spec.declass) yield {
// Forall fv(o). (t_T1 or t_t2) -> G (o_T1 <-> o_T2)
(o.freeVars().toList, Implies(Or(t.in(T1), t.in(T2)), Eq(o.in(T1), o.in(T2))))
}
val quants = premise.flatMap(_._1).toSet.toList // eliminate doubles
// val premise = for ((o, t) <- spec.declass) yield {
// // Forall fv(o). (t_T1 or t_t2) -> G (o_T1 <-> o_T2)
// (o.freeVars().toList, Implies(Or(t.in(T1), t.in(T2)), Eq(o.in(T1), o.in(T2))))
// }
// val quants = premise.flatMap(_._1).toSet.toList // eliminate doubles
val quant = spec.target.params.drop(1)
val conclusion = Forall(quant, genEq(spec.target, agent :: quant))
Forall(agent, Forall(quants, Implies(And.make(premise.map(_._2)), conclusion))).simplify()
val conclusion = genEq(spec.target, spec.target.params)
Forall(spec.target.params, conclusion).simplify()
}
def invariantNoninterStubbornBS(spec: Spec) = {
val agent = spec.target.params(0)
val premise = for ((o, t) <- spec.declass) yield {
// Forall fv(o). (t_T1 or t_t2) -> G (o_T1 <-> o_T2)
(o.freeVars().toList, Implies(Or(t.in(T1), t.in(T2)), Eq(o.in(T1), o.in(T2))))
}
val quants = premise.flatMap(_._1).toSet.toList // eliminate doubles
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, Forall(quants, Implies(And.make(premise.map(_._2)), conclusion))).simplify()
}
// def invariantNoninterStubbornBS(spec: Spec) = {
// val agent = spec.target.params(0)
//
// val premise = for ((o, t) <- spec.declass) yield {
// // Forall fv(o). (t_T1 or t_t2) -> G (o_T1 <-> o_T2)
// (o.freeVars().toList, Implies(Or(t.in(T1), t.in(T2)), Eq(o.in(T1), o.in(T2))))
// }
// val quants = premise.flatMap(_._1).toSet.toList // eliminate doubles
//
// 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, Forall(quants, Implies(And.make(premise.map(_._2)), conclusion))).simplify()
// }
def invariantAllEqual(spec: Spec) = {
And.make(for (r <- spec.w.sig.preds.toList) yield {
......
src/test/scala/de/tum/workflows/ltl/tests/EncodingTest.scala
View file @ 301bbee4
......@@ -17,7 +17,6 @@ import de.tum.workflows.ltl.FOTransformers
import de.tum.workflows.ExampleWorkflows
import de.tum.workflows.blocks._
class EncodingTest extends FlatSpec {
val w = ExampleWorkflows.parseExample("tests/simpleChoice").get.w
......@@ -82,7 +81,7 @@ class EncodingTest extends FlatSpec {
val choices = Set(Fun("choice0", List("x", "y")))
val Rab = Fun("R", List("a", "b"))
val s = Spec(Workflow.EMPTY, List(), Rab, List())
val s = Spec(Workflow.EMPTY, Map(), Rab, List())
val nonint = Noninterference(choices, s)
......@@ -100,7 +99,7 @@ class EncodingTest extends FlatSpec {
choices should be (Set(Fun("choice0", List("x", "s"))))
val ce = Fun("R", List("ax", "as"))
val s = Spec(Workflow.EMPTY, List(), ce, List())
val s = Spec(Workflow.EMPTY, Map(), ce, List())
val noninter = Noninterference(choices, s)
noninter should be (
......@@ -108,7 +107,7 @@ class EncodingTest extends FlatSpec {
Stubborn("ax", choices),
Finally(Exists("as", Neg(Eq(ce.in(T1), ce.in(T2))))))))
val s2 = Spec(w, List(), Fun("R", List("ax", "as")), List())
val s2 = Spec(w, Map(), Fun("R", List("ax", "as")), List())
val prop = Properties.noninterStubborn(s2)
val (agents, res) = FOTransformers.eliminateExistentials(prop)
......
src/test/scala/de/tum/workflows/ltl/tests/FOLTLTest.scala
View file @ 301bbee4
......@@ -84,7 +84,7 @@ class FOLTLTest extends FlatSpec {
it should "compute CNF" in {
val f = Or(And("a", "b"), And("c","d"))
f.toCNF() should be (
f.toCNF().simplify() should be (
And.make(
Or("a", "c"), Or("a","d"),
Or("b","c"), Or("b","d")
......@@ -94,7 +94,7 @@ class FOLTLTest extends FlatSpec {
it should "compute CNF for formulas with quantifiers" in {
val f = Or(And(Exists("c", "c"), "b"), And(Exists("c", "c"),"d"))
f.toCNF() should be (
f.toCNF().simplify() should be (
Exists(List("c"), And.make(
"c",
Or("c","d"),
......
src/test/scala/de/tum/workflows/ltl/tests/InvariantEasychairTest.scala
View file @ 301bbee4
......@@ -24,49 +24,56 @@ class InvariantEasychairTest extends FlatSpec {
"InvariantChecker" should "prove nonomitting/conference safe" in {
val name = "nonomitting/conference"
val x = Var("x", "A")
val p = Var("p","P")
val x = Var("xt", "A")
val p = Var("pt","P")
val inv = Forall(List(x, p), genEq("Conf", List(x, p)))
assert(checkSafe(name, inv))
}
it should "prove nonomitting/conference_linear with declass safe" in {
val name = "nonomitting/conference_linear"
val x = Var("xt", "X")
val y = Var("yt","X")
val p = Var("pt","P")
val inv = Forall(List(x, p), genEq("Comm", List(x, y, p)))
assert(checkSafe(name, inv))
}
it should "prove tests/conferenceNoOracle safe" in {
val name = "tests/conferenceNoOracle"
val xa = Var("xa","A")
val xb = Var("xb","A")
val p = Var("p","P")
val xa = Var("xat","A")
val xb = Var("xbt","A")
val p = Var("pt","P")
val inv = Forall(List(xa, xb, p), genEq("Read", List(xa, xb, p)))