\documentclass [10pt]{article}


\usepackage{latexsym}
\usepackage{amssymb}
\usepackage{epsfig}
\usepackage{fullpage}
\usepackage{enumerate}
\usepackage{xspace}
\usepackage{todonotes}
\usepackage{listings}
\usepackage{url}
\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{Ivanov, Ivaylo (11777707) \& Millauer, Peter (01350868)}}

\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~\ref{alg:vuln-write}.

\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}
  \label{alg:vuln-write}
\end{algorithm}

\medspace

In the following example (Algorithm~\ref{alg:pop-incorrect}) 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~\ref{alg:pop-incorrect} behaves just like $write$ did in Algorithm~\ref{alg:pop-incorrect}.

\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}
  \label{alg:pop-incorrect}
\end{algorithm}

Another weakness that allows arbitrary storage access is unchecked assembly code. Assembly is a powerful tool that allows the developers to get as close to the EVM as they can,
but it may also be very dangerous when not tested correctly. As per the documentation\footnote{\url{https://docs.soliditylang.org/en/latest/assembly.html}}: \textit{"this [inline assembly]
bypasses important safety features and checks of Solidity. You should only use it for tasks that need it, and only if you are confident with using it."}
When given access to such lowlevel structures, a programmer can built-in not only weaknesses similar to the ones described previously, but also others, such as overwriting map locations,
contract variables etc.

An example for such a weakness is given in Algorithm~\ref{alg:unchecked-assembly}.

\medspace

\lstset{style=mystyle}
\begin{algorithm}[H]
	\begin{lstlisting}[language=Octave]
	pragma solidity 0.4.25;

	contract MyContract {
		address private owner;
    mapping(address => bool) public managers;

		constructor() public {
			owner = msg.sender;
      setNextUserRole(msg.sender);
		}

    function setNextManager(address next) internal {
      uint256 slot;
      assembly {
        slot := managers.slot
        sstore(slot, next)
      }

      bytes32 location = keccak256(abi.encode(160, uint256(slot)));
      assembly {
        sstore(location, true)
      }
		}

    function registerUser(address user) {
      require(msg.sender == owner);
      setNextManager(user);
    }

    function cashout() {
      require(managers[msg.sender]);
      address payable manager = msg.sender;
      manager.transfer(address(this).balance);
    }
	}
	\end{lstlisting}
	\caption{An unchecked assembly write to mapping}
  \label{alg:unchecked-assembly}
\end{algorithm}

The contract has a manager mapping, which should be used as a stack.
The developer has added the \texttt{setNextManager} function, which should set the top of the stack to the latest user as a manager.
The issue is that the function is implemented in such a way, that the stack would not grow, but the first element would always be overwritten - this arises from the fact that the memory slot
of the managers mapping does not point to the memory address on the top of the stack, but instead to the base of it.
The function is then using this slot address directly, without calculating any offset, overwriting the base of the stack.


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