zenon/formal-methods-minniethor
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

Final

Browse Source
This commit is contained in:
Tobias Eidelpes 2021-07-09 16:01:21 +02:00
parent 57bff6d2e9
commit 4d027b6ecb
19 changed files with 1106 additions and 16 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

277
abstract-semantics.txt Normal file
View File

@ -0,0 +1,277 @@
/* ============ Selector Functions ============ */
/* === General Infrastructure === */
sel pcs: unit -> [int]; // gives all pcs of the contract
sel pcsForOpcode: int -> [int]; // gives all pcs for a certain opcode
sel argumentForPc: int -> [int]; // gives the argument for the opcode at pc (can only be invoked pcs containing a PUSH, JUMP or JUMPI)
/* ============ Opcodes ============= */
const ADD := 0;
const AND := 1;
const LE := 2;
const PUSH := 3;
const POP := 4;
const MLOAD := 5;
const MSTORE := 6;
const SLOAD := 7;
const SSTORE := 8;
const TIMESTAMP := 9;
const BALANCE := 10;
const INPUT := 11;
const ADDRESS := 12;
const GAS := 13;
const JUMP := 14;
const JUMPI := 15;
const RETURN := 16;
const STOP := 17;
const FAIL := 18;
const CALL := 19;
/* ============ Abstract Domain and abstract operations ============ */
eqtype AbsDom := @T | @V<int>; /* Abstract Domain: @T represents the top element, V(v) concrete elements of value v */
// operation that checks whether a value is concrete (not top)
op isConcrete(a:AbsDom): bool := match a with | @T => false | _ => true;
//operation that extracts the concrete value from an abstract value (in case of @T it defaults to 0)
op extractConcrete(a:AbsDom): int := match a with | @V(x) => x | _ => 0;
op isAbstract(a:AbsDom): bool := ~ isConcrete(a);
op absAdd(a:AbsDom, b:AbsDom): AbsDom :=
match (a, b) with
| (@V(n), @V(m)) => @V(n+m)
| _ => @T;
op absAnd(a:AbsDom, b:AbsDom): AbsDom :=
match (a, b) with
| (@V(n), @V(m)) => (n > 0 && m > 0) ? (@V(1)) : (@V(0))
| _ => @T;
op absLe(a:AbsDom, b:AbsDom): AbsDom :=
match (a, b) with
| (@V(n), @V(m)) => (n <= m) ? (@V(1)) : (@V(0))
| _ => @T;
/* ============ Predicates ============ */
pred ExState{int}: int * array<AbsDom> * array<AbsDom> * AbsDom * array<AbsDom> * bool; // Execution State: <pc>, size, stack, memory, input, storage, cl (call level)
pred Exc{}: bool; // Exceptional Halting: cl, predicate signalizing exceptional halting
pred Halt{}: array<AbsDom> * AbsDom * bool; // Successful Halting: storage, return value, cl
/* ============ Abstract Rules ============ */
rule exception :=
for (!pc: int) in pcs()
clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool]
ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl)
=> Exc(?cl);
rule add :=
for (!pc: int) in pcsForOpcode(ADD)
clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool, ?x: AbsDom, ?y: AbsDom]
ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl),
?size > 1,
?x = select ?sa (?size - 1),
?y = select ?sa (?size - 2)
=> ExState{!pc+1}(?size - 1, store ?sa (?size - 2) (absAdd(?x, ?y)), ?mem, ?in, ?stor, ?cl);
rule and :=
for (!pc: int) in pcsForOpcode(AND)
clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool, ?x: AbsDom, ?y: AbsDom]
ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl),
?size > 1,
?x = select ?sa (?size - 1),
?y = select ?sa (?size - 2)
=> ExState{!pc+1}(?size - 1, store ?sa (?size - 2) (absAnd(?x, ?y)), ?mem, ?in, ?stor, ?cl);
rule le :=
for (!pc: int) in pcsForOpcode(LE)
clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool, ?x: AbsDom, ?y: AbsDom]
ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl),
?size > 1,
?x = select ?sa (?size - 1),
?y = select ?sa (?size - 2)
=> ExState{!pc+1}(?size - 1, store ?sa (?size - 2) (absLe(?x, ?y)), ?mem, ?in, ?stor, ?cl);
rule push :=
for (!pc: int) in pcsForOpcode(PUSH), (!v: int) in argumentForPc(!pc)
clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool]
ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl)
=> ExState{!pc+1}(?size + 1, store ?sa ?size @V(!v), ?mem, ?in, ?stor, ?cl);
rule pop :=
for (!pc: int) in pcsForOpcode(POP)
clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool]
ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl),
?size >= 1
=> ExState{!pc+1}(?size - 1, ?sa, ?mem, ?in, ?stor, ?cl);
rule mstore :=
for (!pc: int) in pcsForOpcode(MSTORE)
clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool, ?p: AbsDom, ?v: AbsDom]
ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl),
?size >= 2,
?p = select ?sa (?size - 1),
isConcrete(?p),
?v = select ?sa (?size - 2)
=> ExState{!pc+1}(?size - 2, ?sa, store ?mem extractConcrete(?p) ?v, ?in, ?stor, ?cl),
clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool, ?p: AbsDom, ?v: AbsDom]
ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl),
?size >= 2,
?p = select ?sa (?size - 1),
isAbstract(?p)
=> ExState{!pc+1}(?size - 2, ?sa, [@T], ?in, ?stor, ?cl);
rule mload :=
for (!pc: int) in pcsForOpcode(MLOAD)
clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool, ?p: AbsDom, ?v: AbsDom]
ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl),
?size >= 1,
?p = select ?sa (?size -1),
isConcrete(?p),
?v = select ?mem (extractConcrete(?p))
=> ExState{!pc+1}(?size, store ?sa (?size - 1) ?v, ?mem, ?in, ?stor, ?cl),
clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool, ?p: AbsDom, ?v: AbsDom]
ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl),
?size >= 1,
?p = select ?sa (?size -1),
isAbstract(?p)
=> ExState{!pc+1}(?size, store ?sa (?size - 1) @T, ?mem, ?in, ?stor, ?cl);
rule sload :=
for (!pc: int) in pcsForOpcode(SLOAD)
clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool, ?v: AbsDom, ?p: AbsDom]
ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl),
?size >= 1,
?p = select ?sa (?size -1),
isConcrete(?p),
?v = select ?stor extractConcrete(?p)
=> ExState{!pc+1}(?size, store ?sa (?size - 1) ?v, ?mem, ?in, ?stor, ?cl),
clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool, ?p: AbsDom]
ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl),
?size >= 1,
?p = select ?sa (?size -1),
isAbstract(?p)
=> ExState{!pc+1}(?size, store ?sa (?size - 1) @T, ?mem, ?in, ?stor, ?cl);
rule sstore :=
for (!pc: int) in pcsForOpcode(SSTORE)
clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool, ?p: AbsDom, ?v: AbsDom]
ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl),
?size >= 2,
?p = select ?sa (?size -1),
isConcrete(?p),
?v = select ?sa (?size -2)
=> ExState{!pc+1}(?size - 2, ?sa, ?mem, ?in, store ?stor extractConcrete(?p) ?v, ?cl),
clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool, ?p: AbsDom]
ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl),
?size >= 2,
?p = select ?sa (?size -1),
isAbstract(?p)
=> ExState{!pc+1}(?size - 2, ?sa, ?mem, ?in, [@T], ?cl);
rule timestamp :=
for (!pc: int) in pcsForOpcode(TIMESTAMP)
clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool]
ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl)
=> ExState{!pc+1}(?size + 1, store ?sa ?size @T, ?mem, ?in, ?stor, ?cl);
rule balance :=
for (!pc: int) in pcsForOpcode(BALANCE)
clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool]
ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl),
?size >= 1
=> ExState{!pc+1}(?size, store ?sa (?size - 1) @T, ?mem, ?in, ?stor, ?cl);
rule input :=
for (!pc: int) in pcsForOpcode(INPUT)
clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool]
ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl)
=> ExState{!pc+1}(?size + 1, store ?sa ?size ?in, ?mem, ?in, ?stor, ?cl);
rule address :=
for (!pc: int) in pcsForOpcode(ADDRESS)
clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool]
ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl)
=> ExState{!pc+1}(?size + 1, store ?sa ?size @T, ?mem, ?in, ?stor, ?cl);
rule gas :=
for (!pc: int) in pcsForOpcode(GAS)
clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool]
ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl)
=> ExState{!pc+1}(?size + 1, store ?sa ?size @T, ?mem, ?in, ?stor, ?cl);
rule jump :=
for (!pc: int) in pcsForOpcode(JUMP), (!j: int) in argumentForPc(!pc)
clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool]
ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl)
=> ExState{!j}(?size, ?sa, ?mem, ?in, ?stor, ?cl);
rule jumpi :=
for (!pc: int) in pcsForOpcode(JUMPI), (!j: int) in argumentForPc(!pc)
clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool, ?p: AbsDom]
ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl),
?size >= 1,
?p = select ?sa (?size - 1),
(isAbstract(?p) || extractConcrete(?p) != 0)
=> ExState{!j}(?size-1, ?sa, ?mem, ?in, ?stor, ?cl),
clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool, ?p: AbsDom]
ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl),
?size >= 1,
?p = select ?sa (?size - 1),
(isAbstract(?p) || extractConcrete(?p) = 0)
=> ExState{!pc+1}(?size-1, ?sa, ?mem, ?in, ?stor, ?cl);
rule return :=
for (!pc: int) in pcsForOpcode(RETURN)
clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool, ?p: AbsDom]
ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl),
?size >= 1,
?p = select ?sa (?size -1)
=> Halt{}(?stor, ?p, ?cl);
rule stop :=
for (!pc: int) in pcsForOpcode(STOP)
clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool]
ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl)
=> Halt{}(?stor, @V(0), ?cl);
rule fail :=
for (!pc: int) in pcsForOpcode(FAIL)
clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool]
ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl)
=> Exc(?cl);
rule call1 :=
for (!pc: int) in pcsForOpcode(CALL)
clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool]
ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl),
?size > 3
=> ExState{0}(0, [@V(0)], [@V(0)], @T, ?stor, true);
rule call2 :=
for (!pc: int) in pcsForOpcode(CALL)
clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool, ?storInv:array<AbsDom>, ?r: AbsDom]
ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl),
?size > 3,
Halt{}(?storInv, ?r, true)
=> ExState{0}(0, [@V(0)], [@V(0)], @T, ?storInv, true);
rule call3 :=
for (!pc: int) in pcsForOpcode(CALL)
clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool]
ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl),
?size > 3
=> ExState{!pc+1}(?size-3, store ?sa (?size - 4) @T, [@T], ?in, [@T], ?cl);
/* ============ Initialization ============ */
rule initOp :=
clause
true
=> ExState{0}(0, [@V(0)], [@V(0)], @T, [@T], false); // execution starts at pc 0 in empty execution state

14
alice.txt Normal file
View File

@ -0,0 +1,14 @@
PUSH 4294967295;
SLOAD;
PUSH 1;
LE;
PUSH 64;
JUMPI 13;
PUSH 0;
PUSH 2;
INPUT;
CALL;
PUSH 1;
PUSH 4294967295;
SSTORE;
STOP;

14
bob.txt Normal file
View File

@ -0,0 +1,14 @@
PUSH 4294967295;
SLOAD;
PUSH 1;
LE;
JUMPI 13;
PUSH 64;
PUSH 0;
PUSH 2;
INPUT;
CALL;
PUSH 1;
PUSH 4294967295;
SSTORE;
STOP;

15
call-contract.txt Normal file
View File

@ -0,0 +1,15 @@
// writes 10 to 3 in storage
/* 0 */ PUSH 10;
/* 1 */ PUSH 3;
/* 2 */ SSTORE;
// calls another contract
/* 3 */ PUSH 0; // oa
/* 4 */ PUSH 2; // id
/* 5 */ PUSH 3; // va
/* 6 */ PUSH 42; // to
/* 7 */ CALL;
// writes 20 to 3 in storage
/* 8 */ PUSH 20;
/* 9 */ PUSH 3;
/* 10 */ SSTORE;
/* 11 */ STOP;

120
call-tests.txt Normal file
View File

@ -0,0 +1,120 @@
/* Special tests for the Call rules. To be run with call-contract.txt */
// Check that the storage can have the right values before calling (at this point there is only one possible value at call level 0)
test storageSoundnesBeforeTest expect SAT
[?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>,?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool]
ExState{7}(4, ?sa, ?mem, ?in, ?stor, false),
stackMoreAbstractThanForall{4}(?sa, store (store (store (store [@V(0)] 0 @V(0)) 1 @V(2)) 2 @V(3)) 3 @V(42)),
arrayMoreAbstractThan{1}(?mem, store [UPDATEDUMMY] 0 @UP(0, @V(0))),
arrayMoreAbstractThan{1}(?stor, store [UPDATEDUMMY] 0 @UP(3, @V(10)));
test storagePrecisePossibleBeforeTest expect SAT
[?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>,?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool]
ExState{7}(4, ?sa, ?mem, ?in, ?stor, false),
stackEqualForall{4}(?sa, store (store (store (store [@V(0)] 0 @V(0)) 1 @V(2)) 2 @V(3)) 3 @V(42)),
?mem = [@V(0)],
(select ?stor 3) = @V(10);
test storagePreciseUniqueBeforeTest expect UNSAT
[?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>,?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool]
ExState{7}(?size, ?sa, ?mem, ?in, ?stor, false),
(?size != 4 || ?mem != [@V(0)]
|| stackInequalExists{4}(?sa, store (store (store (store [@V(0)] 0 @V(0)) 1 @V(2)) 2 @V(3)) 3 @V(42))
|| (select ?stor 3) != @V(10));
//Check for the right storage when reentering (can be 10 or 20, but nothing else)
test storageSoundnessReenteringTest1 expect SAT
[?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>,?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool]
ExState{0}(0, ?sa, ?mem, ?in, ?stor, true),
valueMoreAbstractThan(?in, @T),
arrayMoreAbstractThan{1}(?mem, store [UPDATEDUMMY] 0 @UP(0, @V(0))),
arrayMoreAbstractThan{1}(?stor, store [UPDATEDUMMY] 0 @UP(3, @V(10)));
test storageSoundnessReenteringTest2 expect SAT
[?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>,?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool]
ExState{0}(0, ?sa, ?mem, ?in, ?stor, true),
valueMoreAbstractThan(?in, @T),
arrayMoreAbstractThan{1}(?mem, store [UPDATEDUMMY] 0 @UP(0, @V(0))),
arrayMoreAbstractThan{1}(?stor, store [UPDATEDUMMY] 0 @UP(3, @V(20)));
test storagePrecisePossibleReenteringTest1 expect SAT
[?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>,?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool]
ExState{0}(0, ?sa, ?mem, ?in, ?stor, true),
?mem = [@V(0)],
?in = @T,
(select ?stor 3) = @V(10);
test storagePrecisePossibleReenteringTest2 expect SAT
[?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>,?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool]
ExState{0}(0, ?sa, ?mem, ?in, ?stor, true),
?mem = [@V(0)],
?in = @T,
(select ?stor 3) = @V(20);
test storagePreciseUniqueReenteringTest expect UNSAT
[?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>,?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool]
ExState{0}(?size, ?sa, ?mem, ?in, ?stor, true),
(?mem != [@V(0)] || ?in != @T || ?size != 0 ||
(select ?stor 3) != @V(10) && (select ?stor 3) != @V(20));
// Check that the storage is sound after reentering (on both levels)
test storageSoundnessResumeTest1 expect SAT
[?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>,?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool]
ExState{8}(1, ?sa, ?mem, ?in, ?stor, false),
stackMoreAbstractThanForall{1}(?sa, store [@V(0)] 0 @T),
arrayMoreAbstractThan{1}(?mem, store [UPDATEDUMMY] 0 @UP(0, @T)),
arrayMoreAbstractThan{1}(?stor, store [UPDATEDUMMY] 0 @UP(3, @V(10)));
test storageSoundnessResumeTest2 expect SAT
[?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>,?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool]
ExState{8}(1, ?sa, ?mem, ?in, ?stor, false),
stackMoreAbstractThanForall{1}(?sa, store [@V(0)] 0 @T),
arrayMoreAbstractThan{1}(?mem, store [UPDATEDUMMY] 0 @UP(0, @T)),
arrayMoreAbstractThan{1}(?stor, store [UPDATEDUMMY] 0 @UP(3, @V(20)));
test storageSoundnessResumeTest3 expect SAT
[?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>,?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool]
ExState{8}(1, ?sa, ?mem, ?in, ?stor, true),
stackMoreAbstractThanForall{1}(?sa, store [@V(0)] 0 @T),
arrayMoreAbstractThan{1}(?mem, store [UPDATEDUMMY] 0 @UP(0, @T)),
arrayMoreAbstractThan{1}(?stor, store [UPDATEDUMMY] 0 @UP(3, @V(10)));
test storageSoundnessResumeTest4 expect SAT
[?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>,?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool]
ExState{8}(1, ?sa, ?mem, ?in, ?stor, true),
stackMoreAbstractThanForall{1}(?sa, store [@V(0)] 0 @T),
arrayMoreAbstractThan{1}(?mem, store [UPDATEDUMMY] 0 @UP(0, @T)),
arrayMoreAbstractThan{1}(?stor, store [UPDATEDUMMY] 0 @UP(3, @V(20)));
// Check that the storage is right when halting
test storageSoundnessHaltTest1 expect SAT
[?res: AbsDom, ?stor: array<AbsDom>]
Halt(?stor, ?res, false),
valueMoreAbstractThan(?res, @V(0)),
arrayMoreAbstractThan{1}(?stor, store [UPDATEDUMMY] 0 @UP(3, @V(20)));
test storageSoundnessHaltTest2 expect SAT
[?res: AbsDom, ?stor: array<AbsDom>]
Halt(?stor, ?res, true),
valueMoreAbstractThan(?res, @V(0)),
arrayMoreAbstractThan{1}(?stor, store [UPDATEDUMMY] 0 @UP(3, @V(20)));
test storagePrecisePossibleHaltTest1 expect SAT
[?res: AbsDom, ?stor: array<AbsDom>]
Halt(?stor, ?res, false),
?res = @V(0),
(select ?stor 3) = @V(20);
test storagePrecisePossibleHaltTest2 expect SAT
[?res: AbsDom, ?stor: array<AbsDom>]
Halt(?stor, ?res, true),
?res = @V(0),
(select ?stor 3) = @V(20);
test storagePreciseUniqueHaltTest expect UNSAT
[?res: AbsDom, ?stor: array<AbsDom>, ?cl: bool]
Halt(?stor, ?res, ?cl),
(select ?stor 3) != @V(20) || (?res != @V(0)) ;

33
call1.txt Normal file
View File

@ -0,0 +1,33 @@
rule rule1 :=
for (!pc: int) in pcsForOpcode(CALL)
clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool]
ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl),
?size > 3
=> ExState{0}(0, [@V(0)], [@V(0)], @T, ?stor, true);
rule rule2 :=
for (!pc: int) in pcsForOpcode(CALL)
clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool, ?storInv: array<AbsDom>, ?r: AbsDom]
ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl),
?size > 3,
Halt{}(?storInv,?r,true)
=> ExState{0}(0, [@V(0)], [@V(0)], @T, ?storInv, true);
rule rule3 :=
for (!pc: int) in pcsForOpcode(CALL)
clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool]
ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl),
?size > 3,
isAbstract(select ?sa (?size - 4))
=> ExState{!pc+1}(?size-3, store ?sa (?size - 4) @T, [@T], ?in, [@T], ?cl);
rule rule4 :=
for (!pc: int) in pcsForOpcode(CALL)
clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool, ?p: AbsDom, ?storInv: array<AbsDom>, ?r: AbsDom]
ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl),
?size > 3,
?p = select ?sa (?size - 4),
isConcrete(?p),
extractConcrete(?p) >= 0,
Halt(?storInv, ?r, true)
=> ExState{!pc+1}(?size-3, store ?sa (?size - 4) @T, store ?mem (extractConcrete (?p)) ?r, ?in, [@T], ?cl);

29
call2.txt Normal file
View File

@ -0,0 +1,29 @@
rule rule1 :=
for (!pc: int) in pcsForOpcode(CALL)
clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool]
ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl),
?size > 3
=> ExState{0}(0, [@V(0)], [@V(0)], @T, ?stor, true);
rule rule2 :=
for (!pc: int) in pcsForOpcode(CALL)
clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool, ?storInv: array<AbsDom>, ?r: AbsDom]
ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl),
?size > 3,
Halt{}(?storInv, ?r, true)
=> ExState{0}(0, [@V(0)], [@V(0)], @T, ?storInv, true);
rule rule3 :=
for (!pc: int) in pcsForOpcode(CALL)
clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool]
ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl),
?size > 3
=> ExState{!pc+1}(?size-3, store ?sa (?size - 4) @T, [@T], ?in, ?stor, ?cl);
rule rule4 :=
for (!pc: int) in pcsForOpcode(CALL)
clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool, ?storInv: array<AbsDom>, ?r: AbsDom]
ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl),
?size > 3,
Halt(?storInv, ?r, true)
=> ExState{!pc+1}(?size-3, store ?sa (?size - 4) @T, [@T], ?in, ?storInv, ?cl);

13
call3.txt Normal file
View File

@ -0,0 +1,13 @@
rule rule1 :=
for (!pc: int) in pcsForOpcode(CALL)
clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool]
ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl),
?size > 3
=> ExState{0}(0, [@V(0)], [@V(0)], @T, ?stor, true);
rule rule2 :=
for (!pc: int) in pcsForOpcode(CALL)
clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool]
ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl),
?size > 3
=> ExState{!pc+1}(?size-3, store ?sa (?size - 4) @T, [@T], ?in, [@T], ?cl);

22
call4.txt Normal file
View File

@ -0,0 +1,22 @@
rule rule1 :=
for (!pc: int) in pcsForOpcode(CALL)
clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool, ?v: AbsDom]
ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl),
?size > 3,
?v = select ?sa (?size -3)
=> ExState{0}(0, [@V(0)], [@V(0)], ?v, ?stor, true);
rule rule2 :=
for (!pc: int) in pcsForOpcode(CALL)
clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool, ?storInv: array<AbsDom>, ?r: AbsDom]
ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl),
?size > 3,
Halt{}(?storInv, ?r, true)
=> ExState{0}(0, [@V(0)], [@V(0)], @T, ?storInv, true);
rule rule3 :=
for (!pc: int) in pcsForOpcode(CALL)
clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool]
ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl),
?size > 3
=> ExState{!pc+1}(?size-3, store ?sa (?size - 4) @T, [@T], ?in, [@T], ?cl);

28
call5.txt Normal file
View File

@ -0,0 +1,28 @@
rule rule1 :=
for (!pc: int) in pcsForOpcode(CALL)
clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool]
ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl),
?size > 3
=> ExState{0}(0, [@V(0)], [@V(0)], @T, ?stor, true);
rule rule2 :=
for (!pc: int) in pcsForOpcode(CALL)
clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool, ?storInv: array<AbsDom>, ?r: AbsDom]
ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl),
?size > 3,
Halt{}(?storInv, ?r, true)
=> ExState{0}(0, [@V(0)], [@V(0)], @T, ?storInv, true);
rule rule3 :=
for (!pc: int) in pcsForOpcode(CALL)
clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool]
ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl),
?size > 3
=> ExState{!pc+1}(?size-3, store ?sa (?size - 4) @V(1), [@T], ?in, [@T], ?cl);
rule rule4 :=
for (!pc: int) in pcsForOpcode(CALL)
clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool]
ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl),
?size > 3
=> ExState{!pc+1}(?size-3, store ?sa (?size - 4) @V(0), ?mem, ?in, [@T], ?cl);

23
counter-example1.txt Normal file
View File

@ -0,0 +1,23 @@
PUSH 123; // address of sent
SLOAD; // get value of sent
PUSH 1;
LE; // check 1 <= sent (= !(sent < 1))
JUMPI 22;
PUSH 1;
PUSH 123;
SSTORE; // sent = 1
PUSH ~1337; // - oa
PUSH 0; // - id
PUSH 2; // - va
INPUT; // - to
CALL; // call 1
PUSH ~1337;
MLOAD;
PUSH 123;
SSTORE; // sent = memory[oa]
PUSH ~1337;
PUSH 0; // - id
PUSH 2; // - va
INPUT; // - to
CALL; // call 2
STOP;

20
counter-example3.txt Normal file
View File

@ -0,0 +1,20 @@
INPUT;
JUMPI 16;
PUSH 2;
SLOAD;
PUSH 1;
LE; // 1 <= sent ( == !(sent < 1))
JUMPI 19;
PUSH 1;
PUSH 2;
SSTORE; // sent := 1
PUSH 1;
PUSH 2;
PUSH 2;
PUSH 4;
CALL;
STOP;
PUSH 0;
PUSH 2;
SSTORE; // sent := 0
STOP;

11
counter-example4.txt Normal file
View File

@ -0,0 +1,11 @@
PUSH 0;
INPUT;
LE; // x <= 0
JUMPI 10;
PUSH 123; // - oa
PUSH 0; // - id, important
PUSH 2; // - va
PUSH 1337; // - to, attacker
CALL;
STOP;
FAIL;

54
local-contract.txt Normal file
View File

@ -0,0 +1,54 @@
/* 0 */ PUSH 1; // [1]
/* 1 */ PUSH ~2; // [~2, 1]
/* 2 */ ADD; // [~1]
/* 3 */ PUSH 1; // [1, ~1]
/* 4 */ AND; // [0]
/* 5 */ PUSH 2; // [2, 0]
/* 6 */ LE; // [0]
/* 7 */ PUSH ~1; // [~1, 0]
/* 8 */ LE; // [1]
/* 9 */ PUSH 336633572; // [336633572, 1]
/* 10 */ AND; // [1]
/* 11 */ POP; // []
/* 12 */ PUSH 246435; // [246435]
/* 13 */ MLOAD; // [0]
/* 14 */ PUSH 2; // [2, 0]
/* 15 */ ADD; // [2]
/* 16 */ PUSH 1; // [1, 2]
/* 17 */ MSTORE; // [] [[1 -> 2]]
/* 18 */ PUSH 1; // [1]
/* 19 */ MLOAD; // [2]
/* 20 */ TIMESTAMP; // [T, 2]
/* 21 */ MLOAD; // [T, 2]
/* 22 */ MSTORE; // [] [[_ -> T]]
/* 23 */ PUSH ~42; // [~42]
/* 24 */ SLOAD; // [T]
/* 25 */ SLOAD; // [T]
/* 26 */ POP; // []
/* 27 */ PUSH ~1337; // [~1337]
/* 28 */ PUSH ~67; // [~67, ~1337]
/* 29 */ SSTORE; // [] ((~67 -> ~1337))
/* 30 */ PUSH ~67; // [~67]
/* 31 */ SLOAD; // [~1337]
/* 32 */ BALANCE; // [T]
/* 33 */ SLOAD; // [T]
/* 34 */ INPUT; // [T, T]
/* 35 */ SSTORE; // [] ((_ -> T))
/* 36 */ ADDRESS; // [T]
/* 37 */ GAS; // [T, T]
/* 38 */ JUMP 40; // [T, T]
/* 39 */ RETURN; // UNREACHABLE (over-jumped)
/* 40 */ JUMPI 43; // [T]
/* 41 */ BALANCE; // [T]
/* 42 */ RETURN; // [T]
/* 43 */ JUMPI 45; // []
/* 44 */ STOP; // []
/* 45 */ GAS; // [T]
/* 46 */ JUMPI 48; // []
/* 47 */ FAIL; //
/* 48 */ PUSH 1; // [1]
/* 49 */ JUMPI 51; // []
/* 50 */ FAIL; // UNREACHABLE (over-jumped)
/* 51 */ STOP; // []
// CALL tests are missing

289
local-tests.txt Normal file
View File

@ -0,0 +1,289 @@
/* Tests for the local instructions of tinyEVM. To be run on local-contract.txt */
op pcToConfig(pc: int): Config :=
match pc with
| 0 => @C( 0,
[@V(0)],
UPDATELISTDUMMY,
UPDATELISTDUMMY)
| 1 => @C( 1,
store [@V(0)] 0 @V(1),
UPDATELISTDUMMY,
UPDATELISTDUMMY)
| 2 => @C( 2,
store (store [@V(0)] 0 @V(1)) 1 @V(~2),
UPDATELISTDUMMY,
UPDATELISTDUMMY)
| 3 => @C( 1,
store [@V(0)] 0 @V(~1),
UPDATELISTDUMMY,
UPDATELISTDUMMY)
| 4 => @C( 2,
store (store [@V(0)] 0 @V(~1)) 1 @V(1),
UPDATELISTDUMMY,
UPDATELISTDUMMY)
| 5 => @C( 1,
store [@V(0)] 0 @V(0),
UPDATELISTDUMMY,
UPDATELISTDUMMY)
| 6 => @C( 2,
store (store [@V(0)] 0 @V(0)) 1 @V(2),
UPDATELISTDUMMY,
UPDATELISTDUMMY)
| 7 => @C( 1,
store [@V(0)] 0 @V(0),
UPDATELISTDUMMY,
UPDATELISTDUMMY)
| 8 => @C( 2,
store (store [@V(0)] 0 @V(0)) 1 @V(~1),
UPDATELISTDUMMY,
UPDATELISTDUMMY)
| 9 => @C( 1,
store [@V(0)] 0 @V(1),
UPDATELISTDUMMY,
UPDATELISTDUMMY)
| 10 => @C( 2,
store (store [@V(0)] 0 @V(1)) 1 @V(336633572),
UPDATELISTDUMMY,
UPDATELISTDUMMY)
| 11 => @C( 1,
store [@V(0)] 0 @V(1),
UPDATELISTDUMMY,
UPDATELISTDUMMY)
| 12 => @C( 0,
[@V(0)],
UPDATELISTDUMMY,
UPDATELISTDUMMY)
| 13 => @C( 1,
store [@V(0)] 0 @V(246435),
UPDATELISTDUMMY,
UPDATELISTDUMMY)
| 14 => @C( 1,
[@V(0)],
UPDATELISTDUMMY,
UPDATELISTDUMMY)
| 15 => @C( 2,
store [@V(0)] 1 @V(2),
UPDATELISTDUMMY,
UPDATELISTDUMMY)
| 16 => @C( 1,
store [@V(0)] 0 @V(2),
UPDATELISTDUMMY,
UPDATELISTDUMMY)
| 17 => @C( 2,
store (store [@V(0)] 0 @V(2)) 1 @V(1),
UPDATELISTDUMMY,
UPDATELISTDUMMY)
| 18 => @C( 0,
[@V(0)],
addUpdate(UPDATELISTDUMMY, @UP(1, @V(2))),
UPDATELISTDUMMY)
| 19 => @C( 1,
store [@V(0)] 0 @V(1),
addUpdate(UPDATELISTDUMMY, @UP(1, @V(2))),
UPDATELISTDUMMY)
| 20 => @C( 1,
store [@V(0)] 0 @V(2),
addUpdate(UPDATELISTDUMMY, @UP(1, @V(2))),
UPDATELISTDUMMY)
| 21 => @C( 2,
store (store [@V(0)] 0 @V(2)) 1 @T,
addUpdate(UPDATELISTDUMMY, @UP(1, @V(2))),
UPDATELISTDUMMY)
| 22 => @C( 2,
store (store [@V(0)] 0 @V(2)) 1 @T,
addUpdate(UPDATELISTDUMMY, @UP(1, @V(2))),
UPDATELISTDUMMY)
| 23 => @C( 0,
[@V(0)],
addUpdate(UPDATELISTDUMMY, @UP(1, @T)),
UPDATELISTDUMMY)
| 24 => @C( 1,
store [@V(0)] 0 @V(~42),
addUpdate(UPDATELISTDUMMY, @UP(1, @T)),
UPDATELISTDUMMY)
| 25 => @C( 1,
store [@V(0)] 0 @T,
addUpdate(UPDATELISTDUMMY, @UP(1, @T)),
UPDATELISTDUMMY)
| 26 => @C( 1,
store [@V(0)] 0 @T,
addUpdate(UPDATELISTDUMMY, @UP(1, @T)),
UPDATELISTDUMMY)
| 27 => @C( 0,
[@V(0)],
addUpdate(UPDATELISTDUMMY, @UP(1, @T)),
UPDATELISTDUMMY)
| 28 => @C( 1,
store [@V(0)] 0 @V(~1337),
addUpdate(UPDATELISTDUMMY, @UP(1, @T)),
UPDATELISTDUMMY)
| 29 => @C( 2,
store (store [@V(0)] 0 @V(~1337)) 1 @V(~67),
addUpdate(UPDATELISTDUMMY, @UP(1, @T)),
UPDATELISTDUMMY)
| 30 => @C( 0,
[@V(0)],
addUpdate(UPDATELISTDUMMY, @UP(1, @T)),
addUpdate(UPDATELISTDUMMY, @UP(~67, @V(~1337))))
| 31 => @C( 1,
store [@V(0)] 0 @V(~67),
addUpdate(UPDATELISTDUMMY, @UP(1, @T)),
addUpdate(UPDATELISTDUMMY, @UP(~67, @V(~1337))))
| 32 => @C( 1,
store [@V(0)] 0 @V(~1337),
addUpdate(UPDATELISTDUMMY, @UP(1, @T)),
addUpdate(UPDATELISTDUMMY, @UP(~67, @V(~1337))))
| 33 => @C( 1,
store [@V(0)] 0 @T,
addUpdate(UPDATELISTDUMMY, @UP(1, @T)),
addUpdate(UPDATELISTDUMMY, @UP(~67, @V(~1337))))
| 34 => @C( 1,
store [@V(0)] 0 @T,
addUpdate(UPDATELISTDUMMY, @UP(1, @T)),
addUpdate(UPDATELISTDUMMY, @UP(~67, @V(~1337))))
| 35 => @C( 2,
store (store [@V(0)] 0 @T) 1 @T,
addUpdate(UPDATELISTDUMMY, @UP(1, @T)),
addUpdate(UPDATELISTDUMMY, @UP(~67, @V(~1337))))
| 36 => @C( 0,
[@V(0)],
addUpdate(UPDATELISTDUMMY, @UP(1, @T)),
addUpdate(UPDATELISTDUMMY, @UP(~67, @T)))
| 37 => @C( 1,
store [@V(0)] 0 @T,
addUpdate(UPDATELISTDUMMY, @UP(1, @T)),
addUpdate(UPDATELISTDUMMY, @UP(~67, @T)))
| 38 => @C( 2,
store (store [@V(0)] 0 @T) 1 @T,
addUpdate(UPDATELISTDUMMY, @UP(1, @T)),
addUpdate(UPDATELISTDUMMY, @UP(~67, @T)))
| 40 => @C( 2,
store (store [@V(0)] 0 @T) 1 @T,
addUpdate(UPDATELISTDUMMY, @UP(1, @T)),
addUpdate(UPDATELISTDUMMY, @UP(~67, @T)))
| 41 => @C( 1,
store [@V(0)] 0 @T,
addUpdate(UPDATELISTDUMMY, @UP(1, @T)),
addUpdate(UPDATELISTDUMMY, @UP(~67, @T)))
| 42 => @C( 1,
store [@V(0)] 0 @T,
addUpdate(UPDATELISTDUMMY, @UP(1, @T)),
addUpdate(UPDATELISTDUMMY, @UP(~67, @T)))
| 43 => @C( 1,
store [@V(0)] 0 @T,
addUpdate(UPDATELISTDUMMY, @UP(1, @T)),
addUpdate(UPDATELISTDUMMY, @UP(~67, @T)))
| 44 => @C( 0,
[@V(0)],
addUpdate(UPDATELISTDUMMY, @UP(1, @T)),
addUpdate(UPDATELISTDUMMY, @UP(~67, @T)))
| 45 => @C( 0,
[@V(0)],
addUpdate(UPDATELISTDUMMY, @UP(1, @T)),
addUpdate(UPDATELISTDUMMY, @UP(~67, @T)))
| 46 => @C( 1,
store [@V(0)] 0 @T,
addUpdate(UPDATELISTDUMMY, @UP(1, @T)),
addUpdate(UPDATELISTDUMMY, @UP(~67, @T)))
| 47 => @C( 0,
[@V(0)],
addUpdate(UPDATELISTDUMMY, @UP(1, @T)),
addUpdate(UPDATELISTDUMMY, @UP(~67, @T)))
| 48 => @C( 0,
[@V(0)],
addUpdate(UPDATELISTDUMMY, @UP(1, @T)),
addUpdate(UPDATELISTDUMMY, @UP(~67, @T)))
| 49 => @C( 1,
store [@V(0)] 0 @V(1),
addUpdate(UPDATELISTDUMMY, @UP(1, @T)),
addUpdate(UPDATELISTDUMMY, @UP(~67, @T)))
| 51 => @C( 0,
[@V(0)],
addUpdate(UPDATELISTDUMMY, @UP(1, @T)),
addUpdate(UPDATELISTDUMMY, @UP(~67, @T)))
| _ => @C( 0,
[@V(0)],
UPDATELISTDUMMY,
UPDATELISTDUMMY);
const INTERVALS := 3;
test pcToStackTest expect SAT [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>,?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool]
ExState{1}(?size, ?sa, ?mem, ?in, ?stor, ?cl),
(@V(1)) = (select (getStackArray(pcToConfig(1))) 0);
test soundnessTest expect SAT
for (!i: int) in interval(0, INTERVALS), (!pc: int) in interval((!i = 0)? (0): ((!i = 1)?(40):(51)), (!i = 0)? (39): ((!i = 1)?(50):(52))) // ugly way to only invoke the rule on certain intervals
[?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>,?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool]
ExState{!pc}(getStackSize(pcToConfig(!pc)), ?sa, ?mem, @T, ?stor, false),
stackMoreAbstractThanForall{getStackSize(pcToConfig(!pc))}(?sa, getStackArray(pcToConfig(!pc))),
arrayMoreAbstractThan{getUpdateSize(getMemUpdateList(pcToConfig(!pc)))}(?mem, getUpdates(getMemUpdateList(pcToConfig(!pc)))),
arrayMoreAbstractThan{getUpdateSize(getStorUpdateList(pcToConfig(!pc)))}(?stor, getUpdates(getStorUpdateList(pcToConfig(!pc))))
;
test precisionPossibleTest expect SAT
for (!i: int) in interval(0, INTERVALS), (!pc: int) in interval((!i = 0)? (0): ((!i = 1)?(40):(51)), (!i = 0)? (39): ((!i = 1)?(50):(52)))
[?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>,?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool]
ExState{!pc}(getStackSize(pcToConfig(!pc)), ?sa, ?mem, @T, ?stor, false),
stackEqualForall{getStackSize(pcToConfig(!pc))}(?sa, getStackArray(pcToConfig(!pc))),
arrayEqual{getUpdateSize(getMemUpdateList(pcToConfig(!pc)))}(?mem, getUpdates(getMemUpdateList(pcToConfig(!pc)))),
arrayEqual{getUpdateSize(getStorUpdateList(pcToConfig(!pc)))}(?stor, getUpdates(getStorUpdateList(pcToConfig(!pc))))
;
test precisionUniqueTest expect UNSAT
for (!i: int) in interval(0, INTERVALS), (!pc: int) in interval((!i = 0)? (0): ((!i = 1)?(40):(51)), (!i = 0)? (39): ((!i = 1)?(50):(52)))
[?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>,?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool]
ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, false),
(?size != getStackSize(pcToConfig(!pc)))
|| (stackInequalExists{getStackSize(pcToConfig(!pc))}(?sa, getStackArray(pcToConfig(!pc))))
|| (arrayInequalExists{getUpdateSize(getMemUpdateList(pcToConfig(!pc)))}(?mem, getUpdates(getMemUpdateList(pcToConfig(!pc)))))
|| (?in != @T)
|| (arrayInequalExists{getUpdateSize(getStorUpdateList(pcToConfig(!pc)))}(?stor, getUpdates(getStorUpdateList(pcToConfig(!pc)))))
;
/* Additional Tests concerning reachability, halting, etc. */
// pcs 39 and 50 should be unreachable because they are over-jumped
test unreachable39Test expect UNSAT
[?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>,?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool]
ExState{39}(?size, ?sa, ?mem, ?in, ?stor, ?cl);
test unreachable50Test expect UNSAT
[?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>,?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool]
ExState{50}(?size, ?sa, ?mem, ?in, ?stor, ?cl);
// Tests for correct halting
test haltSoundnessTest expect SAT
[?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>,?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool, ?res: AbsDom]
Halt(?stor, ?res, false),
valueMoreAbstractThan(?res, @V(0));
test haltPrecisePossibleTest expect SAT
[?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>,?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool, ?res: AbsDom]
Halt(?stor, @V(0), false);
// the only possible return results are 0 and T (due to stop and RETURN)
test haltPreciionUniquenessTest expect UNSAT
[?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>,?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool, ?res: AbsDom]
Halt(?stor, ?res, false),
(?res != @V(0) && ?res != @T);
// Reaching an exceptional state should be possible
test exceptionPossibleTest expect SAT
Exc(false);
test noCallTest2 expect UNSAT
Exc(true);
/*
query testQuery [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>,?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool, ?res: AbsDom, ?p: AbsDom]
ExState{13}(?size, ?sa, ?mem, ?in, ?stor, ?cl), ?size > 0,
?p = select ?sa (?size -1),
?res = (isConcrete(?p))? (select ?mem (extractConcrete(?p))):(@T),
?res = @V(0); */

7
queries.txt Normal file
View File

@ -0,0 +1,7 @@
/* ============ Reentrancy query ============ */
query reentrancyCall for (!pc:int) in pcsForOpcode(CALL)
[?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?size:int]
ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, true);

BIN
report/report.pdf Normal file
View File

Binary file not shown.

51
report/report.tex
View File

@ -17,9 +17,9 @@
% please enter your group number your names and matriculation numbers here
%TODO
\newcommand{\groupnumber}{Our group number}
\newcommand{\name}{Our names}
\newcommand{\matriculation}{Our matriculations, same order as the names}
\newcommand{\groupnumber}{5}
\newcommand{\name}{Tobias Eidelpes}
\newcommand{\matriculation}{01527193}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% End of customization %
@ -43,7 +43,7 @@
\thispagestyle{empty}
\noindent\framebox[\linewidth]{%
\begin{minipage}{\linewidth}%
\hspace*{5pt} \textbf{Formal Methods for Security and Privacy (SS2020)} \hfill Prof.~Matteo Maffei \hspace*{5pt}\\
\hspace*{5pt} \textbf{Formal Methods for Security and Privacy (SS2021)} \hfill Prof.~Matteo Maffei \hspace*{5pt}\\
\begin{center}
{\bf\Large Project \projnumber~-- \Title}
@ -65,21 +65,52 @@ Our group consists of the following members:
\end{center}
\section{Abstract Semantics}
\emph{Nothing to fill in here, unless you feel that there is something about the implementation that we should consider when grading.}
\emph{Nothing to fill in here, unless you feel that there is something about the
implementation that we should consider when grading.}
\section{Fixing reentrancy}
\paragraph{Justification for the soundness of \texttt{alice.txt}:}
\subsubsection*{Justification for the soundness of \texttt{alice.txt}:}
%TODO
By switching the order of line 5 and line 6 in \texttt{alice.txt}, the contract
\texttt{bob.txt} has been fixed. This works because \texttt{sent} is set to 1
\emph{before} the call instruction is executed and therefore reentering the
function is possible but will not execute another call instruction because
\texttt{sent} has already been set to 1. The contract now follows the
\emph{Check-Effects-Interactions Pattern}, which requires that checks and state
changes have to occur before calls to other contracts.
\section{Soundness of the \texttt{CALL} rules}
\paragraph{Soundness classification of \texttt{CALL} rule sets:}
\subsubsection*{Soundness classification of \texttt{CALL} rule sets:}
\paragraph{Intuition for the sound rule sets:}
\textbf{Call 1}: Unsound \\
\textbf{Call 2}: Sound \\
\textbf{Call 3}: Unsound \\
\textbf{Call 4}: Unsound \\
\textbf{Call 5}: Sound
\paragraph{Attack descriptions for the counter examples to the unsound rule sets:}
\subsubsection*{Intuition for the sound rule sets:}
\paragraph{Call 2:}
The first two rules are the same rules as presented in the lecture. The third rule
models the case where the contract resumes execution after a call with the same
storage as before the call. This rule applies when the contract was not called
and produced a successful halting state before the contract resumes the
execution after the call.
The fourth rule, however, models the case where the contract resumes execution
after it was left by another call from a contract that resulted in a halting
state.
\paragraph{Call 5:}
As for Call 2, the first two rules are the same as presented in the lecture. The
third rule is correct because in case of $sa[size - 4] = 1$, the local memory
and the persistent storage are correctly over-approximated. The other case is
where $sa[size - 4] = 0$. In this case the caller's memory may not be
manipulated, as formalized by the small-step semantics.
\end{document}

90
test-infrastructure.txt Normal file
View File

@ -0,0 +1,90 @@
/* Testing infrastructure */
sel interval: int * int -> [int]; // interval function: interval (m, n) provides the numbers m, ..., n-1
op valueMoreAbstractThan (a: AbsDom, b:AbsDom): bool :=
match (a, b) with
| (@T, _) => true
| (@V(x), @V(y)) => x = y
| _ => false;
// Checks whether there exists a position where the two stacks disagree
op stackInequalExists{!size: int}(sa: array<AbsDom>, sb: array<AbsDom>): bool :=
for (!i: int) in interval(0,!size): || ((select sa !i) != (select sb !i));
// Checks whether the stacks agree at all positions
op stackEqualForall{!size: int}(sa: array<AbsDom>, sb: array<AbsDom>): bool :=
for (!i: int) in interval(0,!size): && ((select sa !i) = (select sb !i));
// Checks that the first stack is more abstract than the second one at all positions
op stackMoreAbstractThanForall{!size: int}(sa: array<AbsDom>, sb: array<AbsDom>): bool :=
for (!i: int) in interval(0,!size): && (valueMoreAbstractThan(select sa !i, select sb !i));
// Update representation for AbsDom arrays. Used for easily checking against a sequence of probing points in memory or storage
datatype Update := @UP<int*AbsDom>;
datatype UpdateList := @UPLIST<int*array<Update>>;
const UPDATEDUMMY := @UP(0, @T);
const UPDATELISTDUMMY := @UPLIST(0, [UPDATEDUMMY]);
op addUpdate(updates: UpdateList, up: Update): UpdateList :=
match updates with
| @UPLIST(size, ups) => @UPLIST(size + 1, store ups size up)
| _ => UPDATELISTDUMMY;
// Checks whether the array sa agrees with all updates of the Update array sb
op arrayEqual{!size:int} (sa: array<AbsDom>, sb: array<Update>): bool :=
for (!i:int) in interval(0, !size): &&
(match (select sb !i) with
| @UP(p, v) => (select sa p) = v
| _ => false)
;
// Checks whether the array sa is at all update points more concrete than the updates in sb
op arrayMoreAbstractThan{!size:int} (sa: array<AbsDom>, sb: array<Update>): bool :=
for (!i:int) in interval(0, !size): &&
(match (select sb !i) with
| @UP(p, v) => valueMoreAbstractThan(select sa p, v)
| _ => false)
;
// Checks whether array sa disagrees on one of the update points with the updates in sb
op arrayInequalExists{!size:int} (sa: array<AbsDom>, sb: array<Update>): bool :=
for (!i:int) in interval(0, !size): ||
(match (select sb !i) with
| @UP(p, v) => (select sa p) != v
| _ => false)
;
// Configurations that we use for testing. Consist of the stack size, the stack array, and update lists for memory and storage (to probe at the specified points)
datatype Config := @C<int*array<AbsDom>*UpdateList*UpdateList>;
op getStackSize(conf: Config): int :=
match conf with
| @C(size, sa, mem, stor) => size
| _ => 0;
op getStackArray(conf: Config): array<AbsDom> :=
match conf with
| @C(size, sa, mem, stor) => sa
| _ => [@T];
op getMemUpdateList(conf: Config): UpdateList :=
match conf with
| @C(size, sa, mem, stor) => mem
| _ => UPDATELISTDUMMY;
op getStorUpdateList(conf: Config): UpdateList :=
match conf with
| @C(size, sa, mem, stor) => stor
| _ => UPDATELISTDUMMY;
op getUpdateSize(ul: UpdateList): int :=
match ul with
| @UPLIST(s, ua) => s
| _ => 0;
op getUpdates(ul: UpdateList): array<Update> :=
match ul with
| @UPLIST(s, ua) => ua
| _ => [UPDATEDUMMY];