Initial commit

.gitignore

@@ -0,0 +1,8 @@
+*.zip
+
+*.aux
+*.fdb_latexmk
+*.fls
+*.log
+*.out
+*.synctex.gz

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 () 

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 

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}
+