Commit a45f9930 authored by Eugen Zalinescu's avatar Eugen Zalinescu

after merge and conflict resolving

parents 655c4be6 9ff5c284
......@@ -16,7 +16,7 @@ forallmay a,b
Declassify
O(x): F (T1(x))
O(x): T1(x)
Target
......
......@@ -18,7 +18,7 @@ forallmay a,b
Declassify
O(x): F (T1(x) ∨ T2(x))
O(x): (T1(x) ∨ T2(x))
Target
......
......@@ -13,7 +13,7 @@ loop {
Declassify
O(x:A,p:P): G ¬ Conf(at:A,p:P)
O(x:A,p:P): ¬ Conf(at:A,p:P)
Target
......
......@@ -13,7 +13,7 @@ loop {
Declassify
O(x:A,p:P,r:R): G ¬ Conf(at:A,p:P)
O(x:A,p:P,r:R): ¬ Conf(at:A,p:P)
Target
......
......@@ -11,7 +11,7 @@ forallmay y:X,x:X,p:P
Declassify
O(x:X,p:P,r:R): G ¬ Conf(xt:X,p:P)
O(x:X,p:P,r:R): ¬ Conf(xt:X,p:P)
Target
......
......@@ -12,7 +12,7 @@ loop {
Declassify
Oracle(i:Info,x:User): F (Written(i:Info, u:User))
Oracle(i:Info,x:User): Written(i:Info, u:User)
Target
......
......@@ -9,7 +9,7 @@ forallmay t:TA,s:Student
Declassify
O(p:Prof,s:Student,g:Grade): F Grading(p:Prof,as:Student,g:Grade)
O(p:Prof,s:Student,g:Grade): Grading(p:Prof,as:Student,g:Grade)
Target
......
......@@ -13,7 +13,7 @@ loop {
Declassify
O(x:A,p:P,r:R): G ¬ Conf(at:A,p:P)
O(x:A,p:P,r:R): ¬ Conf(at:A,p:P)
Target
......
......@@ -9,7 +9,7 @@ loop {
Declassify
O(x:A,p:P): G ¬ Conf(at:A,p:P)
O(x:A,p:P): ¬ Conf(at:A,p:P)
Target
......
......@@ -7,7 +7,7 @@ forall x:X,s:S
Declassify
O(x:X,s:S): G ¬ C(xt:X,s:S)
O(x:X,s:S): ¬ C(xt:X,s:S)
Target
......
......@@ -16,7 +16,7 @@ forallmay a,b
Declassify
O(x): F (T1(x) ∨ T2(x))
O(x): (T1(x) ∨ T2(x))
Target
......
......@@ -16,7 +16,7 @@ forallmay a,b
Declassify
O(x): F (T1(x) ∨ T2(x))
O(x): (T1(x) ∨ T2(x))
Target
......
......@@ -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,7 +239,7 @@ 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
}
......
......@@ -65,10 +65,29 @@ class InvariantTest extends FlatSpec {
safe should be (true)
}
def genEq(name:String, params: List[Var]) = {
val o1 = Fun(name, Some("t1"), params)
val o2 = Fun(name, Some("t2"), params)
Eq(o1, o2)
}
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