Seminar-Security-Blockchain/SemSEpaper/exercises.tex

\documentclass [10pt]{article}

  
\usepackage{latexsym}
\usepackage{amssymb}
\usepackage{epsfig} 
\usepackage{fullpage}
\usepackage{enumerate}
\usepackage{xspace}
\usepackage{todonotes}
\usepackage{listings}
\usepackage[ruled,linesnumbered]{algorithm2e} % Enables the writing of pseudo code.
\usepackage{float}% http://ctan.org/pkg/float

\newcommand{\true}{true}
\newcommand{\false}{false}
\pagestyle{plain}
\bibliographystyle{plain}


\title{192.127 Seminar in Software Engineering (Smart Contracts) \\
 SWC-124: Write to Arbitrary Storage Location}
\author{Exercises}

\date{WT 2023/24}

\author{\textbf{*** YOUR NAME AND STUDENT ID ***}}

\newtheorem{theorem}{Theorem}
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{corollary}[theorem]{Corollary}
\newtheorem{proposition}[theorem]{Proposition}
\newtheorem{conjecture}[theorem]{Conjecture}
\newtheorem{definition}[theorem]{Definition}
\newtheorem{example}[theorem]{Example}
\newtheorem{remark}[theorem]{Remark}
\newtheorem{exercise}[theorem]{Exercise}


\renewcommand{\labelenumi}{(\alph{enumi})}

\usepackage{xcolor}

\definecolor{codegreen}{rgb}{0,0.6,0}
\definecolor{codegray}{rgb}{0.5,0.5,0.5}
\definecolor{codepurple}{rgb}{0.58,0,0.82}
\definecolor{backcolour}{rgb}{0.95,0.95,0.92}

\lstdefinestyle{mystyle}{ 
	backgroundcolor=\color{backcolour},   
	commentstyle=\color{codegreen},
	keywordstyle=\color{magenta},
	numberstyle=\tiny\color{codegray},
	stringstyle=\color{codepurple},
	basicstyle=\ttfamily\footnotesize,
	breakatwhitespace=false,         
	breaklines=true,                 
	captionpos=b,                    
	keepspaces=true,                 
	numbers=left,                    
	numbersep=5pt,                  
	showspaces=false,                
	showstringspaces=false,
	showtabs=false,                  
	tabsize=2	
}



\begin{document}


\maketitle

\section{Weakness and consequences}

\subsection{Solidity storage layout}

Any contract's storage is a continuous 256-bit address space consisting of 32-bit values. In order to implement dynamically sized data structures like maps and arrays, Solidity distributes their entries in a pseudo-random location. Due to the vast 256-bit range of addresses collisions are statistically extremely improbable and of little practical relevance in safely implemented contracts.

\medspace

In the case of a dynamic array at variable slot $p$, data is written to continuous locations starting at $keccak(p)$. The array itself contains the length information as an $uint256$ value. Even enormous arrays are unlikely to produce collisions due to the vast address space, although an improperly managed array may store data to an unbounded user-controlled offset, thereby allowing arbitrary overwriting of data.

\medspace

For maps stored in variable slot $p$ the data for index $k$ can be found at $keccak(k . p)$ where $.$ is the concatenation operator. This is a statistically safe approach, as the chance of intentionally finding a value for $keccak(k . p)$ s.t. for a known stored variable $x$, $keccak(k . p) == storage\_address(x)$ is about one in $2^{256}$ and $keccak$ is believed to be a cryptographically secure hash function.

\subsection{The Weakness}

Any unchecked array write is potentially dangerous, as the storage-location of all variables is publicly known and an unconstrained array index can be reverse engineered to target them. This can be achieved by using the known array storage location $p$, target-variable $x$, and computing the offset-value $o$ such that $keccac(p) + o == storage\_address(x)$.

\medspace

A trivial example of such a vulnerable write operation is shown in Algorithm 1.

\lstset{style=mystyle}
\begin{algorithm}[H]
	\begin{lstlisting}[language=Octave]
	pragma solidity 0.4.25;
	
	contract MyContract {
		address private owner;
		uint[] private arr;
		
		constructor() public {
			arr = new uint[](0);
			owner = msg.sender;
		}
		
		function write(unit index, uint value) {
			arr[index] = value;
		}
	}
	\end{lstlisting}
	\caption{A completely unchecked array write}
\end{algorithm}

\medspace

In the following example (Algorithm 2) the $pop$ function incorrectly checks for an array $length >= 0$, thereby allowing the $length$ value to underflow when called with an empty array. Once this weakness is triggered, $update$ in Algorithm 2 behaves just like $write$ did in Algorithm 1. 

\medspace

\lstset{style=mystyle}
\begin{algorithm}[H]
	\begin{lstlisting}[language=Octave]
	pragma solidity 0.4.25;
	
	contract MyContract {
		address private owner;
		uint[] private arr;
		
		constructor() public {
			arr = new uint[](0);
			owner = msg.sender;
		}
		
		function push(value) {
			arr[arr.length] = value;
			arr.length++;
		}
		
		function pop() {
			require(arr.length >= 0);
			arr.length--;
		}
		
		function update(unit index, uint value) {
			require(index < arr.length);
			arr[index] = value;
		}
	}
	\end{lstlisting}
	\caption{An incorrectly managed array length}
\end{algorithm}


\section{Vulnerable contracts in literature}

collect vulnerable contracts used by different papers to motivate/illustrate the weakness

\section{Code properties and automatic detection}

Automatic detection tools can be broadly categorized into ones employing static analysis and those who use fuzzing, i.e. application of semi-random inputs. Notable static analysis tools include Securify \cite{securify} and teEther \cite{teether} which both function in a similar manner:

\medspace

Initially, the given EVM byte-code is disassembled into a control-flow-graph (CFG). In the second step, the tools identify potentially risky instructions. In the case of arbitrary writes, the instruction of note is $sstore(k,v)$ where both $k$ and $v$ are input-controlled. The tools differ in the way they identify whether or not the values are input-controlled. 

\medspace

In the case of Securify \cite{securify}, the CFG is translated into what the authors call "semantic facts" to which an elaborate set of so-called security patterns is applied. These patterns consist of building blocks in the form of predicates, which allows the tool to simply generate output based on the (transitively) matched patterns.

\medspace

teEther \cite{teether} employs a similar approach, but instead the authors opt to build a graph of dependent variables. If the graph arrives at a $sstore(k,v)$ instruction and a path can be found leading to user-controlled inputs, the tool infers a set of constraints which are then used to automatically generate an exploit.

\medspace

The fuzz-driven approach to vulnerability detection is more abstract, as general-purpose fuzzing tools generally don't have knowledge of the analysed program. For the tool SmartFuzzDriverGenerator \cite{fuzzdrivegen}, a multitude of these fuzzing libraries can be used. The problem at hand is, however, that the technique cannot interface with a smart contract out of the box. The "glue" between fuzzer and program is called a driver, hence the name of "driver-generator".

\medspace

SmartFuzzDriverGenerator aims to automatically generate such a driver by %TODO: I have no idea how it does this actually%

\medspace

The Smartian tool \cite{smartian} attempts to find a middle-ground between static and dynamic analysis by first transforming the EVM bytecode into control-flow facts. Based on this information, a set of seed-inputs is generated that are expected to have a high probability of yielding useable results. Should no exploit be found, the seed-inputs are then mutated in order to yield a higher code coverage. %TODO: This is probably extemely inprecise and should be re-written%

\section{Exploit sketch}

\cite{doughoyte}
%TODO: just explain what this guy does: https://github.com/Arachnid/uscc/tree/master/submissions-2017/doughoyte%


\bibliography{exercise.bib}

\end{document}