commit e69b2ed0428abfaaf1290a7d581e15e1b51d10d3 Author: Tobias Eidelpes Date: Thu Jun 3 09:59:05 2021 +0200 Initial commit diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..92e4952 --- /dev/null +++ b/.gitignore @@ -0,0 +1,8 @@ +*.zip + +*.aux +*.fdb_latexmk +*.fls +*.log +*.out +*.synctex.gz diff --git a/Project2.fst b/Project2.fst new file mode 100644 index 0000000..f703319 --- /dev/null +++ b/Project2.fst @@ -0,0 +1,225 @@ +module Project2 + +open FStar.List.Tot + +(* opcodes of the simplified bytecode fragment *) +type opcode = + | ADD : opcode + | CALL : opcode + | AND : opcode + | LE : opcode + | PUSH : int -> opcode + | POP : opcode + | MLOAD : opcode + | MSTORE : opcode + | SLOAD : opcode + | SSTORE : opcode + | TIMESTAMP : opcode + | BALANCE : opcode + | INPUT : opcode + | ADDRESS : opcode + | GAS : opcode + | JUMP : nat -> opcode + | JUMPI : nat -> opcode + | RETURN : opcode + | STOP : opcode + | FAIL : opcode + + +(* Small step configurations. For simplicity we assume all values (in particular stack and memory values as well as memory and storage addresses) to be represented as integers *) + +type address = int +(* a contract is a tuple of a an address and its code *) +type contract = address * list opcode +(* accounts are tuples of the form (b, stor, code) where b is the account's balance, stor is the account's persistent storage, and code is it's opcode *) +type account = nat * (int -> int) * list opcode +(* the global state is a mapping from contract addresses to accounts *) +type gstate = address -> Tot account +(* execution environments are tuples of the form: (actor, input, code) where actor is the address of the active account, input is the input to the call and code is the code currently executed *) +type exenv = address * int * list opcode +(* machine states are tuples of the form: (gas, pc, m, s) where gas is the remaining gas, pc is the program counter, memory is the local memory and s is the machine stack *) +type mstate = nat * nat * (int -> int) * list int // does not carry gas +(* a regular execution state is a tuple of the form (mu, iota, sigma) where mu is the machine state, iota is the execution environment and gstate is the global state *) +type regstate = mstate * exenv * gstate +(* the transaction environment only carries the blocktimestamp represented as an integer *) +type tenv = int + +(* terminating states are either exception states or halting states of the form (sigma, d, gas) where sigma is the global state at the point of halting, d the return value of the call and gas the remaining gas at the point of halting*) +noeq type terstate = +| HaltState: gstate -> int -> nat -> terstate +| ExcState: terstate + +(* callstacks *) +type plaincallstack = list regstate +noeq type callstack = +| Ter : terstate -> plaincallstack -> callstack +| Exec : plaincallstack -> callstack + +(* Small step function *) + +(* Polymorphic update function *) +val update: (#a:eqtype) -> (f: a -> 'b) -> (p:a) -> (e: 'b) -> (x: a) -> Tot 'b +let update (#a:eqtype) (f: a -> 'b) (p: a) (e: 'b) = + fun x -> if x = p then e else f x + +(* size of callstacks *) +val size: callstack -> Tot nat +let size (cs: callstack) = + match cs with + | Exec ps -> length ps + | Ter ts ps -> 1 + length ps + +(* a function that extracts the current opcode given the code and a pc *) +val getOpcode: list opcode -> nat -> Tot opcode +let getOpcode code i = + match (nth code i) with + | None -> STOP + | Some oc -> oc + +(* a function checking whether a state is a call state. We characterize call states as state where CALL was executed and sufficiently many arguments where on the stack *) +val isCallState: regstate -> Tot bool +let isCallState rs = + match rs with + | ((gas, pc, m, to:: v:: inp:: resaddr:: stack), (actor, input, code), sigma) -> getOpcode code pc = CALL + | _ -> false + +(* Wellformedness definition: a callstack is well-formed if all of it's non top elements are call states *) +val wellformed: callstack -> Tot bool +let rec wellformed (cs: callstack) = + match cs with + | Exec [] -> false + | Ter ts ps -> for_all (fun rs -> (isCallState rs)) ps + | Exec (s::ps) -> for_all (fun rs -> (isCallState rs)) ps + +(* Type for the outcome of a single execution step: either the execution terminated (Stop) as a final state is reached or further execution steps are possible *) +noeq type step_outcome = + | Stop : (cs: callstack) -> step_outcome + | Next : (cs: callstack) -> step_outcome + +(* Auxiliary function for applying the effects of terminated states to the underneath execution states *) +val apply_returneffects: (ts: terstate) -> (rs: regstate{isCallState rs}) -> Tot regstate +let apply_returneffects ts rs = + let ((gas, pc, mem, to:: v:: imp:: resaddr:: stack), (actor, code, input), gs) = rs + in assert (pc >= 0); + match ts with + | ExcState -> ((0, pc+1, mem, 0::stack), (actor, code, input), gs) + | HaltState gs' res gas' -> ((gas', pc+1, update mem resaddr res, 1::stack), (actor, code, input), gs') + +(* 3.1: Small-step semantics *) + +(* Small step function that describes one step of execution. Replace all occurences of 'magic ()', by the definitions as specified in the paper semantics *) +val step: tenv -> cs: callstack {wellformed cs} -> Tot step_outcome +let step te cs = + match cs with + | Ter ts [] -> Stop (Ter ts []) + | Ter ts (s :: ps) -> Next (Exec ((apply_returneffects ts s)::ps)) + | Exec (s :: ps) -> + let (((gas, pc, mem, stack), (actor, input, code), gs)) = s in + if gas < 1 then Next (Ter ExcState ps) + else + match (getOpcode code pc, stack) with + | (ADD, a::b::stack') -> Next (Exec(((gas-1, pc+1, mem, (a+b):: stack'), (actor, input, code), gs) :: ps)) + | (AND, a::b::stack') -> magic () + | (LE, a::b::stack') -> magic () + | (PUSH x, stack') -> Next (Exec(((gas-1, pc+1, mem, x::stack'), (actor, input, code), gs)::ps)) + | (POP, x::stack') -> magic () + | (MSTORE, p::v::stack') -> Next (Exec(((gas-1, pc+1, update mem p v, stack'), (actor, input, code), gs)::ps)) + | (MLOAD, p::stack') -> magic () + | (SSTORE, p::v::stack') -> magic () + | (SLOAD, v::stack') -> Next (Exec(((gas-1, pc+1, mem, (let (bal, stor, code) = gs actor in stor v)::stack'), (actor, input, code), gs)::ps)) + | (BALANCE, a::stack') -> magic () + | (ADDRESS, stack') -> Next (Exec(((gas-1, pc+1, mem, actor::stack'), (actor, input, code), gs)::ps)) + | (INPUT, stack') -> magic () + | (GAS, stack') -> Next (Exec(((gas-1, pc+1, mem, gas::stack'), (actor, input, code), gs)::ps)) + | (JUMP i, stack') -> Next (Exec((((gas-1, i, mem, stack'), (actor, input, code), gs))::ps)) + | (JUMPI i, b::stack') -> magic () + | (RETURN, v::stack') -> magic () + | (STOP, stack') -> Next (Ter (HaltState gs 0 (gas-1)) ps) + | (TIMESTAMP, stack') -> magic () + | (CALL, to::v::inp::resaddr::stack') -> magic () + | _ -> Next (Ter ExcState ps) + +(* A simple wrapper for the step function that removes the execution outcome *) +val step_simp: (te: tenv) -> (cs: callstack {wellformed cs}) -> Tot (cs': callstack{wellformed cs'}) +let step_simp te cs = + match (step te cs) with + | Next cs' -> cs' + | Stop cs' -> cs' + +(* Bounded step function that executes an execution state for (at most) n execution steps *) +val nsteps: (n: nat) -> (te: tenv) -> (cs:callstack{wellformed cs}) -> Tot (cs:callstack{wellformed cs}) +let rec nsteps n te cs = + if n=0 then cs + else + nsteps (n-1) te (step_simp te cs) + +(* 3.2: Termination *) +(* We will define an interpreter function steps that executes the small step function till reaching a final state (indicated by Stop) *) +(* Our goal is to prove the termination of this function *) +(* To this end, define a function the following function on callstacks that assigns a measure (in terms of a list of naturals that gets lexicographically interpreted) to each call stack *) + +val getDecArgList: (cs: callstack {wellformed cs}) -> Tot (list nat) +let getDecArgList (cs: callstack {wellformed cs}) = + magic () + +(* A simple helper function that converts a list to a lexicgraphical ordering *) +val getLexFromList: (list nat) -> Tot (lex_t) +let rec getLexFromList ls = + match ls with + | [] -> LexTop + | (l::ls') -> LexCons #nat l (getLexFromList ls') + + +(* Interpreter function that executes the small step function till termination *) +(* Define the function getDecArg list, shuch that the given decreases clause is sufficient for proving the terminination of the function on all arguments *) +val steps: (te:tenv) -> (cs:callstack {wellformed cs}) -> Tot callstack (decreases (getLexFromList(getDecArgList cs))) +let rec steps te cs = + match (step te cs) with + | Next cs' -> steps te cs' + | Stop cs' -> cs' + + +(* 3.3: Final states *) + +(* A syntactic characterization of final call stacks (similiar to stopping criterion in step) *) +val isFinal: (cs: callstack) -> Tot bool +let isFinal cs = + match cs with + | Ter ts [] -> true + | _ -> false + +(* Prove that the syntactic characterization of final states implies a semantic characterization (namely that the execution of arbitrary steps does not affect the callstack anymore) *) +val nsteps_stop: (n: nat) -> (te:tenv) -> (cs: callstack{wellformed cs}) -> +Lemma (requires (isFinal cs)) + (ensures (nsteps n te cs == cs)) +let rec nsteps_stop n te cs = + admit () + +(* Prove that if a call stack does not change within one step then it must be final. Formulate first the Lemma and then prove it *) +(* val progress: *) + +(* 3.4: Uniqueness of callstack *) + +(* Prove that during an execution, every callstack is unique. To this end, first prove that callstacks are always decreasing within n > 0 execution steps (unless they are final) *) +(* Hint: Use the notion of 'smaller' that you used for proving the termination of steps *) +val order_decreases: (n: nat) -> (te: tenv) -> (cs: callstack{wellformed cs}) -> (cs': callstack) -> +Lemma (requires (nsteps n te cs == cs' /\ n > 0 /\ ~ (isFinal cs) )) + (ensures (getLexFromList(getDecArgList cs')<< getLexFromList(getDecArgList cs))) +let rec order_decreases n te cs cs' = + admit () + +(* Use the previous Lemma to show that the callstacks during execution are unique *) +val callstacks_unique: (n: nat) -> (te: tenv) -> (cs: callstack{wellformed cs}) -> (cs': callstack) -> +Lemma (requires (nsteps n te cs == cs' /\ n > 0 /\ ~ (isFinal cs) )) + (ensures (~ (cs == cs'))) +let rec callstacks_unique n te cs cs' = + admit () + +(* 3.5: Exception propagation *) + +(* Prove that when an exception occurs the execution will terminate within 2 * size cs steps *) +val exception_prop: (te:tenv) -> (ps:plaincallstack) -> +Lemma (requires (wellformed (Ter ExcState ps))) + (ensures (nsteps (op_Multiply 2 (length ps)) te (Ter ExcState ps) == (Ter ExcState []))) +let rec exception_prop te ps = + admit () diff --git a/Tests.fst b/Tests.fst new file mode 100644 index 0000000..d6de169 --- /dev/null +++ b/Tests.fst @@ -0,0 +1,73 @@ +module Tests + +open FStar.List.Tot +open Solution + +(* Test cases *) +let empty_gs: gstate = fun a -> (0, (fun p -> 0), []) +let code1 = [PUSH 2; PUSH 1; LE; JUMPI 5; STOP; PUSH 5; RETURN] +let ts1: tenv = 0 +let cs1 : callstack = Exec [( (20, 0, (fun p -> 0), []) , (0, 0, code1) , empty_gs)] +let cs1_res1: callstack = Exec [( (15, 6, (fun p -> 0), [5]) , (0, 0, code1) , empty_gs)] (* after 5 steps *) +let cs1_res2: callstack = Ter (HaltState empty_gs 5 14) [] + +val test1: unit -> +Lemma (ensures ((nsteps 5 ts1 cs1 == cs1_res1) /\ (nsteps 6 ts1 cs1 == cs1_res2))) +let test1 () = () + + +let code2 = [PUSH 1; PUSH 2; PUSH 0; POP; AND; PUSH 5; MSTORE; PUSH 5; MLOAD] +let ts2: tenv = 0 +let cs2 : callstack = Exec [( (20, 0, (fun p -> 0), []) , (0, 0, code2) , empty_gs)] +let cs2_res1: callstack = Exec [( (15, 5, (fun p -> 0), [1]) , (0, 0, code2) , empty_gs)] (* after 5 steps *) +let cs2_res2: callstack = Exec [( (11, 9, (update (fun p -> 0) 5 1), [1]) , (0, 0, code2) , empty_gs)] (* after 9 steps *) + + +#set-options "--max_fuel 20 --z3rlimit 10" +val test2: unit -> +Lemma (ensures (nsteps 5 ts2 cs2 == cs2_res1) /\ (nsteps 9 ts2 cs2 == cs2_res2)) +let test2 () = () +#reset-options + + +let code3 = [PUSH 7; BALANCE; TIMESTAMP; SSTORE; PUSH 5; SLOAD; SLOAD] +let gs3:gstate = update #account #address (fun _ -> (0, (fun _ -> 0), [])) 7 (42,(fun n -> n+1), []) +let ts3: tenv = 6 +let cs3 : callstack = Exec [( (20, 0, (fun p -> 0), []) , (7, 0, code3) , gs3)] +let cs3_res1: callstack = Exec [( (17, 3, (fun p -> 0), [6;42]) , (7, 0, code3) , gs3 )] (* after 3 steps *) +let cs3_res2: callstack = Exec [( (16, 4, (fun p -> 0), []) , (7, 0, code3) , update #account #address gs3 7 (42, update (fun n -> n+1) 6 42, []))] (* after 4 steps *) +let cs3_res3: callstack = Exec [( (13, 7, (fun p -> 0), [42]) , (7, 0, code3) , update #account #address gs3 7 (42, update (fun n -> n+1) 6 42, []))] (* after 7 steps *) +//let cs3_res2: callstack = Exec [( (11, 9, (update (fun p -> 0) 5 1), [1]) , (0, 0, code3) , empty_gs)] (* after 9 steps *) + +#set-options "--max_fuel 20 --z3rlimit 10" +val test3: unit -> +Lemma (ensures ((nsteps 3 ts3 cs3 == cs3_res1) /\ (nsteps 4 ts3 cs3 == cs3_res2) /\ (nsteps 7 ts3 cs3 == cs3_res3))) +let test3 () = () +#reset-options + + +let code4_1 = [PUSH 9; PUSH 7; PUSH 1; BALANCE ; PUSH 2; CALL; POP; PUSH 9; MLOAD] +let code4_2 = [INPUT; PUSH 1; ADD; RETURN] +let gs4:gstate = update #account #address (update #account #address (fun _ -> (0, (fun _ -> 0), [])) 1 (42,(fun _ -> 0), code4_1)) 2 (1337, (fun _ -> 0),code4_2) +let gs4_upd:gstate = update #account #address (update #account #address gs4 2 (1337 + 42,(fun _ -> 0), code4_2)) 1 (0, (fun _ -> 0),code4_1) +let ts4: tenv = 0 +let cs4 : callstack = Exec [( (20, 0, (fun p -> 0), []) , (1, 0, code4_1) , gs4)] +let cs4_res0: callstack = Exec [( (15, 5, (fun p -> 0), [2;42;7;9]) , (1, 0, code4_1) , gs4 )] (* after 5 steps *) +let cs4_res1: callstack = Exec [( (14, 0, (fun p -> 0), []) , (2, 7, code4_2) , gs4_upd );( (15, 5, (fun p -> 0), [2;42;7;9]) , (1, 0, code4_1) , gs4)] (* after 6 steps *) +let cs4_res2: callstack = Exec [( (11, 3, (fun p -> 0), [8]) , (2, 7, code4_2) , gs4_upd );( (15, 5, (fun p -> 0), [2;42;7;9]) , (1, 0, code4_1) , gs4)] (* after 9 steps *) +let cs4_res3: callstack = Exec [( (10, 6, update (fun p -> 0) 9 8, [1]) , (1, 0, code4_1) , gs4_upd )] (* after 11 steps *) +let cs4_res4: callstack = Exec [( (7, 9, update (fun p -> 0) 9 8, [8]) , (1, 0, code4_1) , gs4_upd )] (* after 14 steps *) + +#set-options "--max_fuel 40 --z3rlimit 60" + + +val test4: unit -> +Lemma (ensures ( + nsteps 5 ts4 cs4 == cs4_res0 /\ + nsteps 6 ts4 cs4 == cs4_res1 /\ + nsteps 9 ts4 cs4 == cs4_res2 /\ + nsteps 11 ts4 cs4 == cs4_res3 /\ + nsteps 14 ts4 cs4 == cs4_res4 + )) +let test4 () = () +#reset-options diff --git a/assignment.pdf b/assignment.pdf new file mode 100644 index 0000000..ad0447f Binary files /dev/null and b/assignment.pdf differ diff --git a/report/report.tex b/report/report.tex new file mode 100644 index 0000000..f0bfa23 --- /dev/null +++ b/report/report.tex @@ -0,0 +1,101 @@ +\documentclass[12pt,a4paper]{article} + +\usepackage[cm]{fullpage} +\usepackage{amsthm} +\usepackage{amsmath} +\usepackage{amsfonts} +\usepackage{amssymb} +\usepackage{xspace} +\usepackage[english]{babel} +\usepackage{fancyhdr} +\usepackage{titling} +\renewcommand{\thesection}{Exercise \projnumber.\arabic{section}:} + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% This part needs customization from you % +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +% 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} + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% End of customization % +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +\newcommand\fstar{F$^\star$\xspace} +\newcommand{\projnumber}{2} +\newcommand{\Title}{\fstar} +\setlength{\headheight}{15.2pt} +\setlength{\headsep}{20pt} +\setlength{\textheight}{680pt} +\pagestyle{fancy} +\fancyhf{} +\fancyhead[L]{Formal Methods for Security and Privacy \projnumber\ - ProVerif} +\fancyhead[C]{} +\fancyhead[R]{Group \groupnumber} +\renewcommand{\headrulewidth}{0.4pt} +\fancyfoot[C]{\thepage} + + +\begin{document} +\thispagestyle{empty} +\noindent\framebox[\linewidth]{% + \begin{minipage}{\linewidth}% + \hspace*{5pt} \textbf{Formal Methods for Security and Privacy (SS2018)} \hfill Prof.~Matteo Maffei \hspace*{5pt}\\ + + \begin{center} + {\bf\Large Project \projnumber~-- \Title} + \end{center} + + \vspace*{5pt}\hspace*{5pt} \hfill TU Wien \hspace*{5pt} +\end{minipage}% +} +\vspace{0.5cm} +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + + +\section*{Group \groupnumber} +Our group consists of the following members: +\begin{center} +\textbf{\name} %please fill the information above + +\matriculation %please fill the information above +\end{center} + +\section{Small-step semantics} + +\textit{Notes on semantics. Not mandatory.} + +\section{Termination} + +\paragraph{Explanation of the used measure} +%TODO + +\section{Final states} + +\paragraph{Paper proofs} +%TODO + +\paragraph{Explanation on used equalities} +%TODO + +\section{Uniqueness of call stacks} + +\paragraph{Paper proofs} +%TODO + +\paragraph{Explanation on lemma \texttt{order\_ineq}} +%TODO + +\section{Exception Propagation} + +\paragraph{Paper proof} +%TODO + +\paragraph{Explanation on alternative formulations} +%TODO + +\end{document} + diff --git a/semantics.pdf b/semantics.pdf new file mode 100644 index 0000000..0b1122d Binary files /dev/null and b/semantics.pdf differ