Expand heuristics, fix formatting

SemSEreport/exercises.tex

 \usepackage{epsfig}
 \usepackage{fullpage}
 \usepackage{enumerate}
+\usepackage{enumitem}
 \usepackage{xspace}
 \usepackage{todonotes}
 \usepackage{listings}
 
 \begin{itemize}
 	\item \textbf{solc}: Using \textbf{solc-select} we select the correct solc version and compile the associated *.sol file. This way we gather compiler hints and warnings.
-	\item \textbf{Mythril}: %TODO% Mythril also does something
+  \item \textbf{Mythril}: A tool used for analysis of EVM bytecode, one of the de-facto standards for such work. It is unfortunately not able to detect SWC-124, but there is an existing feature request\footnote{\url{https://github.com/Consensys/mythril/issues/861}} for support available.
 	\item \textbf{teEther}: A tool we found in the last research step of this seminar, teether is a dynamic analysis tool for smart contracts. It is unfortunately hardly documented and has been unmaintained for several years. We were unable to generate usable results with it.
 	\item \textbf{Slither}: A highly useful tool that offers a large static analysis toolkit for solidity, it not only allows the extraction of contract data like storage layouts but also automatic scanning for common weaknesses. Although it did not seem to be able to detect SWC-124, the storage layout functionality was used extensively by our team.
 \end{itemize}
 
 
-\section{Exploit Creation}
+\section{Exploit Creation}\label{sec:exploit-creation}
 
-\subsection{extra short recap of weakness definitions}
+\subsection{Short recap of weakness definitions}
 
 SWC-124 attempts to use the underlying mechanisms that govern dynamic array allocation to deterministically overwrite arbitrary data in smart contracts. An analogous weakness can be created by employing unchecked assembly instructions, although this is a less common attack vector due to its unusual structure.
 
-\subsection{exploit idea(s)}
+\subsection{Exploit heuristics}
 
-The workflow of determining the vulnerability of a given contract is straight forward and follows the general approach of automatic detection mechanisms from our last paper. Since SWC-124 requires the presence of very specific code, it is relatively easy to exclude non-vulnerable contracts. Namely any contract without dynamic arrays or raw assembly including a SSTORE instruction can immediately be considered non-vulnerable. The presence of dynamic arrays can be determined using \textbf{slither --print variable-order}. A sample output looks as follows:
+The workflow of determining the vulnerability of a given contract is straightforward and follows the general approach of automatic detection mechanisms from our last paper. Since SWC-124 requires the presence of very specific code, it is relatively easy to develop heuristics to exclude non-vulnerable contracts:
+\begin{enumerate}[label=\arabic*.]
+  \item any contract without dynamic arrays (or mappings with integer keys) or raw assembly including a SSTORE instruction can immediately be considered non-vulnerable;
+  \item if heuristic 1 does not hold and there is a dynamic array or mapping with an integer key available, we can then apply a second heuristic and namely: checking the solidity compiler version, specified at the top of the contract. Solidity version 0.8.0+ introduced integer under- and overflow protection, which are enabled per default and require extra work to be disabled. As such, we have the following "sub-heuristic":
+    \begin{enumerate}
+      \item if the version of the contract is higher than 0.8.0, we examine whether unchecked arithmetic\footnote{\url{https://docs.soliditylang.org/en/v0.8.0/control-structures.html#checked-or-unchecked-arithmetic}} has been used for modifying the arrays. If this is not the case, which it is not most of the time, we can then determine that the contract is non-vulnerable. Applying this heuristic, we found a contract that could have been vulnerable had it been compiled with a lower solidity version.
+    \end{enumerate}
+\end{enumerate}
+The presence of dynamic arrays can be determined using \textbf{slither --print variable-order}. A sample output looks as follows:
 
 \begin{verbatim}
-$slither cans.sol --print variable-order	
-	
+$slither cans.sol --print variable-order
+
 Cans:
 +----------------------------+----------------------------------------------+------+--------+
 | Name                       |                                         Type | Slot | Offset |
 | Cans.SODA_CONTRACT         |                                      address |  321 |      0 |
 | Cans.baseURI               |                                       string |  322 |      0 |
 +----------------------------+----------------------------------------------+------+--------+
-	
+
 \end{verbatim}
 
 In this example the \textbf{ERC1155.tokens} array is the only potential weakess present. We would then look for the presence of what-where writes to this array in order to confirm the potential presence of SWC-124. What-where writes are of the form
 
 \noindent and are a necessary code snippet for SWC-124. If such an instruction is present, we then attempt to reverse engineer a sequence of inputs to trigger the exploit, or formulate a reason why we believe this not to be possible.
 
+
 \section{Results}
 
-\subsection{vulnerable contracts}
+Applying the heuristics, mentioned in the previous section, we gathered the following data about the contracts.
+
+\subsection{Vulnerable contracts}
 
-None.
+Using the heuristics above, we were not able to find a contract that is vulnerable to SWC-124.
 
-\subsection{non-exploitable contracts}
+\subsection{Non-exploitable contracts}
 
 \noindent Solidity files that contained no contracts:
 
 	\item AuctionLib.sol
 	\item LibRegion.sol
 	\item LToken.sol
-	
+
 \end{itemize}
 
-\noindent Contracts that were discarded due to the non-presence of dynamic arrays or assembly using SSTORE:
+\noindent Contracts that were discarded due to the heuristics holding:
 
 \begin{itemize}
 	\item DCU.sol
 	\item GovernmentAlpha.sol
 	\item HedgeSwap.sol
 	\item HermesImplementation.sol
-	\item IMETACoin223Token\_13.sol
+	\item IMETACoin223Token\_13.sol - had this contract been compiled with solidity under 0.8.0, it could have been vulnerable.
 	\item UniswapV3PoolAdapter.sol
 	\item UserDeposit.sol
 	\item WPCMainnetBridge.sol
 \end{itemize}
 
-\subsection{undecidable contracts}
-
-\subsection{optionally fixes}
-
 \section{Discussion}
 
-\subsection{conclusions}
-
-\subsection{lessons learned: what works, what doesn't}
+\subsection{Conclusions}
 
-\subsection{open challenges}
+\subsection{Lessons learned: what works, what doesn't}
 
+\subsection{Open challenges}
 
 \bibliography{exercise.bib}