From ce5134360537254c54fb11b4f5b9ea180d746972 Mon Sep 17 00:00:00 2001 From: akashlal Date: Sun, 5 Apr 2015 19:52:59 +0530 Subject: Some test cases for SecureVCGen (disabled for lit currently) --- Test/secure/MultiParty.bpl | 187 ++++++++++++++++++++++++++++++++++++++ Test/secure/ObliviousTransfer.bpl | 87 ++++++++++++++++++ Test/secure/simple.bpl | 57 ++++++++++++ 3 files changed, 331 insertions(+) create mode 100644 Test/secure/MultiParty.bpl create mode 100644 Test/secure/ObliviousTransfer.bpl create mode 100644 Test/secure/simple.bpl (limited to 'Test') diff --git a/Test/secure/MultiParty.bpl b/Test/secure/MultiParty.bpl new file mode 100644 index 00000000..eb110a01 --- /dev/null +++ b/Test/secure/MultiParty.bpl @@ -0,0 +1,187 @@ +// Type for data +type T = bv4; +const N: int; axiom N == 4; +const one: T; axiom one == 1bv4; + +// helper operations +function {:inline} xor(a: bool, b: bool) returns (bool) { (!a && b) || (a && !b) } +function {:bvbuiltin "bvxor"} xorT(p1: T, p2: T) : T; +function {:bvbuiltin "bvult"} bv2lt(p1: bv2, p2: bv2) : bool; +function {:bvbuiltin "bvult"} bvlt(p1: T, p2: T) : bool; // unsigned less than +function {:bvbuiltin "bvlshr"} shiftrightAny(p1: T, n: T) : T; // shift right +function {:inline} shiftright(p1: T) : T { shiftrightAny(p1, one) } +function bv2bool(x: bv1) : bool { if (x == 0bv1) then false else true } + +// Oblivious Transfer +procedure ObliviousTransfer( + {:visible "A"} m0: T, {:visible "A"} m1: T, + {:visible "B"} c: bool) +returns ({:visible "B"} m: T) +// spec +ensures (m == if c then m1 else m0); +// Implementation +{ + var {:visible "A"} m0p, m1p: T; + var {:visible "B"} mp: T; + var {:visible "B"} cp: bool; + + var x: bool; + var y, z: T; + + havoc cp; + havoc m0p, m1p; + mp := if cp then m0p else m1p; + + x := xor(c, cp); + y := xorT(m0, if x then m0p else m1p); + z := xorT(m1, if x then m1p else m0p); + + m := xorT(if c then z else y, mp); +} + +// Oblivious Transfer for Bools +procedure ObliviousTransferBool( + {:visible "A"} m0: bool, {:visible "A"} m1: bool, + {:visible "B"} c: bool) +returns ({:visible "B"} m: bool); +// spec +free ensures (m == if c then m1 else m0); + + +// Lover's Protocol 1 +procedure LoversProtocol1( + {:visible "A"} a: bool, {:visible "B"} b: bool) +returns ({:visible "A"} ap: bool, {:visible "B"} bp: bool) +// spec +ensures xor(ap, bp) == (a && b); +{ + havoc ap; + call bp := ObliviousTransferBool(ap, xor(a, ap), b); +} + +// Lover's Protocol 1 Modified +procedure LoversProtocol1Modified( + {:visible "A"} a: bool, {:visible "B"} b: bool) +returns ({:visible "A"} ap: bool, {:visible "B"} bp: bool) +// spec +ensures xor(ap, bp) == xor(a, b); +{ + var {:visible "B"} bpp: bool; + + havoc ap; + bpp := xor(ap, a); + bp := xor(bpp, b); +} + +// Lover's Protocol 2 +procedure LoversProtocol2( + {:visible "A"} aA: bool, {:visible "A"} bA: bool, + {:visible "B"} aB: bool, {:visible "B"} bB: bool) +returns ({:visible "A"} ap: bool, {:visible "B"} bp: bool) +// spec +ensures xor(ap, bp) == (xor(aA, aB) && xor(bA, bB)); +{ + var {:visible "A"} rA, wA: bool; + var {:visible "B"} rB, wB: bool; + + call rA, wA := LoversProtocol1(aA, bB); + call rB, wB := LoversProtocol1(aB, bA); + + ap := xor(xor(aA && bA, rA), wA); + bp := xor(xor(wB, rB), aB && bB); +} + +// While functionally correct, this isn't secure +procedure Incorrect( + {:visible "A"} a: bool, {:visible "B"} b: bool) +returns ({:visible "A"} ap: bool, {:visible "B"} bp: bool) +// spec +ensures xor(ap, bp) == xor(a, b); +{ + ap := a; + bp := b; +} + +procedure TwoBitMillionaires( + {:visible "A"} a: bv2, {:visible "B"} b: bv2) +returns ({:visible "A"} ap: bool, {:visible "B"} bp: bool) +ensures xor(ap, bp) == bv2lt(a, b); +{ + var {:visible "A"} a0, a1: bool; + var {:visible "B"} b0, b1: bool; + + // Extract bits + a0 := bv2bool(a[1:0]); + a1 := bv2bool(a[2:1]); + b0 := bv2bool(b[1:0]); + b1 := bv2bool(b[2:1]); + + call ap, bp := TwoBitMillionairesExplicit(a0, a1, b0, b1); +} + +procedure TwoBitMillionairesExplicit( + {:visible "A"} a0: bool, {:visible "A"} a1: bool, + {:visible "B"} b0: bool, {:visible "B"} b1: bool) +returns ({:visible "A"} ap: bool, {:visible "B"} bp: bool) +ensures xor(ap, bp) == xor(!a1 && b1, (a1 == b1) && (!a0 && b0)); +{ + var {:visible "A"} aA, bA, wA: bool; + var {:visible "B"} aB, bB, wB: bool; + + + call aA, aB := LoversProtocol1(!a1, b1); + call wA, wB := LoversProtocol1(!a0, b0); + call bA, bB := LoversProtocol2(!a1, wA, b1, wB); + + ap := xor(aA, bA); + bp := xor(aB, bB); +} + +procedure TwoBitMillionairesExplicitModified( + {:visible "A"} a0: bool, {:visible "A"} a1: bool, + {:visible "B"} b0: bool, {:visible "B"} b1: bool) +returns ({:visible "A"} ap: bool, {:visible "B"} bp: bool) +ensures xor(ap, bp) == xor(!a1 && b1, (a1 == b1) && xor(a0, b0)); +{ + var {:visible "A"} aA, bA, wA: bool; + var {:visible "B"} aB, bB, wB: bool; + + + call aA, aB := LoversProtocol1(!a1, b1); + call wA, wB := LoversProtocol1Modified(a0, b0); + call bA, bB := LoversProtocol2(!a1, wA, b1, wB); + + ap := xor(aA, bA); + bp := xor(aB, bB); +} + +procedure NBitMillionaires( + {:visible "A"} a: T, {:visible "B"} b: T) +returns ({:visible "A"} la: bool, {:visible "B"} lb: bool) +ensures xor(la, lb) == bvlt(a, b); +{ + var n: int; + + var {:visible "A"} aleft: T; + var {:visible "B"} bleft: T; + var {:visible "A"} an: bool; + var {:visible "B"} bn: bool; + + n := 0; + aleft := a; + bleft := b; + + havoc la, lb; assume xor(la, lb) == false; + while (n < N) + invariant true; + { + an := bv2bool(aleft[1:0]); + bn := bv2bool(bleft[1:0]); + aleft := shiftright(aleft); + bleft := shiftright(bleft); + + call la, lb := TwoBitMillionairesExplicitModified(la, an, lb, bn); + n := n + 1; + } +} + diff --git a/Test/secure/ObliviousTransfer.bpl b/Test/secure/ObliviousTransfer.bpl new file mode 100644 index 00000000..0f26062f --- /dev/null +++ b/Test/secure/ObliviousTransfer.bpl @@ -0,0 +1,87 @@ +type T = bv2; +function {:inline} xor(a: bool, b: bool) returns (bool) { (!a && b) || (a && !b) } +function {:bvbuiltin "bvxor"} xorT(p1: T, p2: T) : T; + +// Oblivious Transfer +procedure ObliviousTransfer_A( + {:visible} m0: T, {:visible} m1: T, + {:hidden} c: bool) +returns ({:hidden} m: T, + {:visible} m0p: T, {:visible} m1p: T, + {:visible} x: bool, + {:visible} y: T, {:visible} z: T + ) +// spec +ensures (m == if c then m1 else m0); +// Implementation +{ + var {:hidden} mp: T; + var {:hidden} cp: bool; + + havoc cp; + havoc m0p, m1p; + mp := if cp then m0p else m1p; + + x := xor(c, cp); + y := xorT(m0, if x then m0p else m1p); + z := xorT(m1, if x then m1p else m0p); + + m := xorT(if c then z else y, mp); +} + + +// Oblivious Transfer +procedure ObliviousTransfer_B( + {:hidden} m0: T, {:hidden} m1: T, + {:visible} c: bool) +returns ({:visible} m: T, + {:visible} mp: T, {:visible} cp: bool, + {:visible} x: bool, + {:visible} y: T, {:visible} z: T + ) +// spec +ensures (m == if c then m1 else m0); +// Implementation +{ + var {:hidden} m0p, m1p: T; + + havoc cp; + havoc m0p, m1p; + mp := if cp then m0p else m1p; + + x := xor(c, cp); + y := xorT(m0, if x then m0p else m1p); + z := xorT(m1, if x then m1p else m0p); + + m := xorT(if c then z else y, mp); + //y := m0; +} + +// Oblivious Transfer +procedure ObliviousTransfer_X( + {:hidden} m0: T, {:hidden} m1: T, + {:hidden} c: bool) +returns ({:hidden "B"} m: T) +// spec +ensures (m == if c then m1 else m0); +// Implementation +{ + var {:hidden} m0p, m1p: T; + var {:hidden} mp: T; + var {:hidden} cp: bool; + + var {:hidden} x: bool; + var {:hidden} y, z: T; + + havoc cp; + havoc m0p, m1p; + mp := if cp then m0p else m1p; + + x := xor(c, cp); + y := xorT(m0, if x then m0p else m1p); + z := xorT(m1, if x then m1p else m0p); + + m := xorT(if c then z else y, mp); +} + + diff --git a/Test/secure/simple.bpl b/Test/secure/simple.bpl new file mode 100644 index 00000000..1d726014 --- /dev/null +++ b/Test/secure/simple.bpl @@ -0,0 +1,57 @@ +// Z3 4.1: /trace /z3opt:MBQI=true /proverOpt:OPTIMIZE_FOR_BV=true /z3opt:RELEVANCY=0 +function {:inline} xor(a: bool, b: bool) returns (bool) { (!a && b) || (a && !b) } + +procedure Incorrect_A( + {:visible} a: bool, {:hidden} b: bool) +returns ({:visible} ap: bool, {:hidden} bp: bool) + ensures xor(ap, bp) == xor(a, b); +{ + ap := a; + bp := b; +} + +procedure Incorrect_B( + {:hidden} a: bool, {:visible} b: bool) +returns ({:hidden} ap: bool, {:visible} bp: bool) + ensures xor(ap, bp) == xor(a, b); +{ + ap := a; + bp := b; +} + +procedure Incorrect_X( + {:hidden} a: bool, {:hidden} b: bool) +returns ({:hidden} ap: bool, {:hidden} bp: bool) + ensures xor(ap, bp) == xor(a, b); +{ + ap := a; + bp := b; +} + +procedure Correct_A( + {:visible} a: bool, {:hidden} b: bool) +returns ({:visible} ap: bool, {:hidden} bp: bool) + ensures xor(ap, bp) == xor(a, b); +{ + havoc ap; + bp := xor(xor(ap, a), b); +} + +procedure Correct_B( + {:hidden} a: bool, {:visible} b: bool) +returns ({:hidden} ap: bool, {:visible} bp: bool) + ensures xor(ap, bp) == xor(a, b); +{ + havoc ap; + bp := xor(xor(ap, a), b); +} + +procedure Correct_X( + {:hidden} a: bool, {:hidden} b: bool) +returns ({:hidden} ap: bool, {:hidden} bp: bool) + ensures xor(ap, bp) == xor(a, b); +{ + havoc ap; + bp := xor(xor(ap, a), b); +} + -- cgit v1.2.3