text:
%% bare_conf.tex
%% V1.4b
%% 2015/08/26
%% by Michael Shell
%% See:
%% http://www.michaelshell.org/
%% for current contact information.
%%
%% This is a skeleton file demonstrating the use of IEEEtran.cls
%% (requires IEEEtran.cls version 1.8b or later) with an IEEE
%% conference paper.
%%
%% Support sites:
%% http://www.michaelshell.org/tex/ieeetran/
%% http://www.ctan.org/pkg/ieeetran
%% and
%% http://www.ieee.org/

%%*************************************************************************
%% Legal Notice:
%% This code is offered as-is without any warranty either expressed or
%% implied; without even the implied warranty of MERCHANTABILITY or
%% FITNESS FOR A PARTICULAR PURPOSE!
%% User assumes all risk.
%% In no event shall the IEEE or any contributor to this code be liable for
%% any damages or losses, including, but not limited to, incidental,
%% consequential, or any other damages, resulting from the use or misuse
%% of any information contained here.
%%
%% All comments are the opinions of their respective authors and are not
%% necessarily endorsed by the IEEE.
%%
%% This work is distributed under the LaTeX Project Public License (LPPL)
%% ( http://www.latex-project.org/ ) version 1.3, and may be freely used,
%% distributed and modified. A copy of the LPPL, version 1.3, is included
%% in the base LaTeX documentation of all distributions of LaTeX released
%% 2003/12/01 or later.
%% Retain all contribution notices and credits.
%% ** Modified files should be clearly indicated as such, including  **
%% ** renaming them and changing author support contact information. **
%%*************************************************************************

% *** Authors should verify (and, if needed, correct) their LaTeX system  ***
% *** with the testflow diagnostic prior to trusting their LaTeX platform ***
% *** with production work. The IEEE's font choices and paper sizes can   ***
% *** trigger bugs that do not appear when using other class files.       ***                          ***
% The testflow support page is at:
% http://www.michaelshell.org/tex/testflow/

\documentclass[conference]{IEEEtran}
% Some Computer Society conferences also require the compsoc mode option,
% but others use the standard conference format.
%
% If IEEEtran.cls has not been installed into the LaTeX system files,
% manually specify the path to it like:
% \documentclass[conference]{../sty/IEEEtran}

% Some very useful LaTeX packages include:
% (uncomment the ones you want to load)

% *** MISC UTILITY PACKAGES ***
%
%\usepackage{ifpdf}
% Heiko Oberdiek's ifpdf.sty is very useful if you need conditional
% compilation based on whether the output is pdf or dvi.
% usage:
% \ifpdf
%   % pdf code
% \else
%   % dvi code
% \fi
% The latest version of ifpdf.sty can be obtained from:
% http://www.ctan.org/pkg/ifpdf
% Also, note that IEEEtran.cls V1.7 and later provides a builtin
% \ifCLASSINFOpdf conditional that works the same way.
% When switching from latex to pdflatex and vice-versa, the compiler may
% have to be run twice to clear warning/error messages.

% *** CITATION PACKAGES ***
%
%\usepackage{cite}
% cite.sty was written by Donald Arseneau
% V1.6 and later of IEEEtran pre-defines the format of the cite.sty package
% \cite{} output to follow that of the IEEE. Loading the cite package will
% result in citation numbers being automatically sorted and properly
% "compressed/ranged". e.g., [1], [9], [2], [7], [5], [6] without using
% cite.sty will become [1], [2], [5]--[7], [9] using cite.sty. cite.sty's
% \cite will automatically add leading space, if needed. Use cite.sty's
% noadjust option (cite.sty V3.8 and later) if you want to turn this off
% such as if a citation ever needs to be enclosed in parenthesis.
% cite.sty is already installed on most LaTeX systems. Be sure and use
% version 5.0 (2009-03-20) and later if using hyperref.sty.
% The latest version can be obtained at:
% http://www.ctan.org/pkg/cite
% The documentation is contained in the cite.sty file itself.

% *** GRAPHICS RELATED PACKAGES ***
%
\ifCLASSINFOpdf
  \usepackage[pdftex]{graphicx}
  % declare the path(s) where your graphic files are
  \graphicspath{{C:/Users/Gautam/Pictures}}
  % and their extensions so you won't have to specify these with
  % every instance of \includegraphics
  \DeclareGraphicsExtensions{.pdf,.jpeg,.png,.jpg}
\else
  % or other class option (dvipsone, dvipdf, if not using dvips). graphicx
  % will default to the driver specified in the system graphics.cfg if no
  % driver is specified.
   \usepackage[dvips]{graphicx}
  % declare the path(s) where your graphic files are
   \graphicspath{{C:/Users/Gautam/Pictures}}
  % and their extensions so you won't have to specify these with
  % every instance of \includegraphics
   \DeclareGraphicsExtensions{.eps}
\fi
% graphicx was written by David Carlisle and Sebastian Rahtz. It is
% required if you want graphics, photos, etc. graphicx.sty is already
% installed on most LaTeX systems. The latest version and documentation
% can be obtained at:
% http://www.ctan.org/pkg/graphicx
% Another good source of documentation is "Using Imported Graphics in
% LaTeX2e" by Keith Reckdahl which can be found at:
% http://www.ctan.org/pkg/epslatex
%
% latex, and pdflatex in dvi mode, support graphics in encapsulated
% postscript (.eps) format. pdflatex in pdf mode supports graphics
% in .pdf, .jpeg, .png and .mps (metapost) formats. Users should ensure
% that all non-photo figures use a vector format (.eps, .pdf, .mps) and
% not a bitmapped formats (.jpeg, .png). The IEEE frowns on bitmapped formats
% which can result in "jaggedy"/blurry rendering of lines and letters as
% well as large increases in file sizes.
%
% You can find documentation about the pdfTeX application at:
% http://www.tug.org/applications/pdftex

% *** MATH PACKAGES ***
%
%\usepackage{amsmath}
% A popular package from the American Mathematical Society that provides
% many useful and powerful commands for dealing with mathematics.
%
% Note that the amsmath package sets \interdisplaylinepenalty to 10000
% thus preventing page breaks from occurring within multiline equations. Use:
%\interdisplaylinepenalty=2500
% after loading amsmath to restore such page breaks as IEEEtran.cls normally
% does. amsmath.sty is already installed on most LaTeX systems. The latest
% version and documentation can be obtained at:
% http://www.ctan.org/pkg/amsmath

% *** SPECIALIZED LIST PACKAGES ***
%
%\usepackage{algorithmic}
% algorithmic.sty was written by Peter Williams and Rogerio Brito.
% This package provides an algorithmic environment fo describing algorithms.
% You can use the algorithmic environment in-text or within a figure
% environment to provide for a floating algorithm. Do NOT use the algorithm
% floating environment provided by algorithm.sty (by the same authors) or
% algorithm2e.sty (by Christophe Fiorio) as the IEEE does not use dedicated
% algorithm float types and packages that provide these will not provide
% correct IEEE style captions. The latest version and documentation of
% algorithmic.sty can be obtained at:
% http://www.ctan.org/pkg/algorithms
% Also of interest may be the (relatively newer and more customizable)
% algorithmicx.sty package by Szasz Janos:
% http://www.ctan.org/pkg/algorithmicx

\usepackage{booktabs}

% *** ALIGNMENT PACKAGES ***
%
\usepackage{array}
% Frank Mittelbach's and David Carlisle's array.sty patches and improves
% the standard LaTeX2e array and tabular environments to provide better
% appearance and additional user controls. As the default LaTeX2e table
% generation code is lacking to the point of almost being broken with
% respect to the quality of the end results, all users are strongly
% advised to use an enhanced (at the very least that provided by array.sty)
% set of table tools. array.sty is already installed on most systems. The
% latest version and documentation can be obtained at:
% http://www.ctan.org/pkg/array

% IEEEtran contains the IEEEeqnarray family of commands that can be used to
% generate multiline equations as well as matrices, tables, etc., of high
% quality.

% *** SUBFIGURE PACKAGES ***
\ifCLASSOPTIONcompsoc
  \usepackage[caption=false,font=normalsize,labelfont=sf,textfont=sf]{subfig}
\else
  \usepackage[caption=false,font=footnotesize]{subfig}
\fi
% subfig.sty, written by Steven Douglas Cochran, is the modern replacement
% for subfigure.sty, the latter of which is no longer maintained and is
% incompatible with some LaTeX packages including fixltx2e. However,
% subfig.sty requires and automatically loads Axel Sommerfeldt's caption.sty
% which will override IEEEtran.cls' handling of captions and this will result
% in non-IEEE style figure/table captions. To prevent this problem, be sure
% and invoke subfig.sty's "caption=false" package option (available since
% subfig.sty version 1.3, 2005/06/28) as this is will preserve IEEEtran.cls
% handling of captions.
% Note that the Computer Society format requires a larger sans serif font
% than the serif footnote size font used in traditional IEEE formatting
% and thus the need to invoke different subfig.sty package options depending
% on whether compsoc mode has been enabled.
%
% The latest version and documentation of subfig.sty can be obtained at:
% http://www.ctan.org/pkg/subfig

% *** FLOAT PACKAGES ***
%
%\usepackage{fixltx2e}
% fixltx2e, the successor to the earlier fix2col.sty, was written by
% Frank Mittelbach and David Carlisle. This package corrects a few problems
% in the LaTeX2e kernel, the most notable of which is that in current
% LaTeX2e releases, the ordering of single and double column floats is not
% guaranteed to be preserved. Thus, an unpatched LaTeX2e can allow a
% single column figure to be placed prior to an earlier double column
% figure.
% Be aware that LaTeX2e kernels dated 2015 and later have fixltx2e.sty's
% corrections already built into the system in which case a warning will
% be issued if an attempt is made to load fixltx2e.sty as it is no longer
% needed.
% The latest version and documentation can be found at:
% http://www.ctan.org/pkg/fixltx2e

%\usepackage{stfloats}
% stfloats.sty was written by Sigitas Tolusis. This package gives LaTeX2e
% the ability to do double column floats at the bottom of the page as well
% as the top. (e.g., "\begin{figure*}[!b]" is not normally possible in
% LaTeX2e). It also provides a command:
%\fnbelowfloat
% to enable the placement of footnotes below bottom floats (the standard
% LaTeX2e kernel puts them above bottom floats). This is an invasive package
% which rewrites many portions of the LaTeX2e float routines. It may not work
% with other packages that modify the LaTeX2e float routines. The latest
% version and documentation can be obtained at:
% http://www.ctan.org/pkg/stfloats
% Do not use the stfloats baselinefloat ability as the IEEE does not allow
% \baselineskip to stretch. Authors submitting work to the IEEE should note
% that the IEEE rarely uses double column equations and that authors should try
% to avoid such use. Do not be tempted to use the cuted.sty or midfloat.sty
% packages (also by Sigitas Tolusis) as the IEEE does not format its papers in
% such ways.
% Do not attempt to use stfloats with fixltx2e as they are incompatible.
% Instead, use Morten Hogholm'a dblfloatfix which combines the features
% of both fixltx2e and stfloats:
%
% \usepackage{dblfloatfix}
% The latest version can be found at:
% http://www.ctan.org/pkg/dblfloatfix

% *** PDF, URL AND HYPERLINK PACKAGES ***
%
%\usepackage{url}
% url.sty was written by Donald Arseneau. It provides better support for
% handling and breaking URLs. url.sty is already installed on most LaTeX
% systems. The latest version and documentation can be obtained at:
% http://www.ctan.org/pkg/url
% Basically, \url{my_url_here}.

% *** Do not adjust lengths that control margins, column widths, etc. ***
% *** Do not use packages that alter fonts (such as pslatex).         ***
% There should be no need to do such things with IEEEtran.cls V1.6 and later.
% (Unless specifically asked to do so by the journal or conference you plan
% to submit to, of course. )

% correct bad hyphenation here

\begin{document}
%
% paper title
% Titles are generally capitalized except for words such as a, an, and, as,
% at, but, by, for, in, nor, of, on, or, the, to and up, which are usually
% not capitalized unless they are the first or last word of the title.
% Linebreaks \\ can be used within to get better formatting as desired.
% Do not put math or special symbols in the title.
\title{Importance of Cooperative gameplay in Multiplayer online battle arena (MOBA) games}

% author names and affiliations
% use a multiple column layout for up to three different
% affiliations
\author{\IEEEauthorblockN{Gautam Baghel, Magy Seif El-Nasr}
\IEEEauthorblockA{College of Computer and Information Science\\
Northeastern University\\
Boston, Massachusetts 02115\\}

}

% conference papers do not typically use \thanks and this command
% is locked out in conference mode. If really needed, such as for
% the acknowledgment of grants, issue a \IEEEoverridecommandlockouts
% after \documentclass

% for over three affiliations, or if they all won't fit within the width
% of the page, use this alternative format:
%
%\author{\IEEEauthorblockN{Michael Shell\IEEEauthorrefmark{1},
%Homer Simpson\IEEEauthorrefmark{2},
%James Kirk\IEEEauthorrefmark{3},
%Montgomery Scott\IEEEauthorrefmark{3} and
%Eldon Tyrell\IEEEauthorrefmark{4}}
%\IEEEauthorblockA{\IEEEauthorrefmark{1}School of Electrical and Computer Engineering\\
%Georgia Institute of Technology,
%Atlanta, Georgia 30332--0250\\ Email: see http://www.michaelshell.org/contact.html}
%\IEEEauthorblockA{\IEEEauthorrefmark{2}Twentieth Century Fox, Springfield, USA\\
%Email: homer@thesimpsons.com}
%\IEEEauthorblockA{\IEEEauthorrefmark{3}Starfleet Academy, San Francisco, California 96678-2391\\
%Telephone: (800) 555--1212, Fax: (888) 555--1212}
%\IEEEauthorblockA{\IEEEauthorrefmark{4}Tyrell Inc., 123 Replicant Street, Los Angeles, California 90210--4321}}

% use for special paper notices
%\IEEEspecialpapernotice{(Invited Paper)}

% make the title area
\maketitle

% As a general rule, do not put math, special symbols or citations
% in the abstract
\begin{abstract}
Computer game contributes a huge part to modern culture. Among different types of computer games, the multi-player online battle arena games generated an electronic sports community and attracted plentiful audiences. LOL (League of Legends), as one of the leading multi-player online battle arena games, Riot has a big responsibility on analyzing game data and improving game experiences to players. This paper applies classification methods to identify the contribution of teamwork performance and star player performance to winning. Through various methods verification, the results show using teamwork behavior has higher prediction accuracy than using one-star player performance data in a match. In sum, the results with a data set of 534398 team data in 2015 recommend better teamwork contributes more to winning than single star player performance.
\end{abstract}

% no keywords

% For peer review papers, you can put extra information on the cover
% page as needed:
% \ifCLASSOPTIONpeerreview
% \begin{center} \bfseries EDICS Category: 3-BBND \end{center}
% \fi
%
% For peerreview papers, this IEEEtran command inserts a page break and
% creates the second title. It will be ignored for other modes.
\IEEEpeerreviewmaketitle

\section{Introduction}
% no \IEEEPARstart

In recent years, there is a rise in popularity of MOBA (Multi-Player Online Battle Arena) games. These games are usually composed of several players forming teams and competing against each other in matches. Each match can range from few minutes of play to hours of play. League of Legends alone reportedly has over 100 million monthly active users \cite{Loterina}. Professional players have made careers out of playing professional MOBA games with earnings in the range of two million dollars annually \cite{esports}. Electronic sports (eSports) are becoming an important part of our culture. In this paper, we are interested in (a) understanding how teamwork is established within a team and how that may impact win/loss. Understanding if the team is important rather than just one player which means more engagement to all the team rather than them relying upon one has design and user experience implication, but also perhaps a learning implication. For game designers, it may be environmental elements of the game which contribute to synergy in a game. For producers, it may be involvement of more players and getting them hooked on the game. For players, it gives them an opportunity to refine their skills where it proved to be inadequate.

To achieve this goal, the paper uses a game analytics approach where data from a MOBA game is analyzed through machine learning algorithms. There has been similar work in this area. Looking at several aspects of team composition from player personalities to champion types in the game. Player personalities may vary in different players altogether and the findings are preliminary. Champion type analysis only looks at the composition based on champion specific skills, player effectiveness in using the champion is not evident. Team versus star player analysis gives a better picture of cooperation versus competition in the game.

In order to tackle this problem, we analyzed 534,398 data of team statistics from MOBA game. We used analyzed the team vs. star player on the team in terms of their contribution to winning/losing. To answer that we turned this into a classification question where we predict win/loss based on team features vs. star-player features. This kind of analysis is the first of its kind to understand the contribution of team members and features influencing win/loss from different team members. The contribution is in the results that we found and it adds to previous work on team level analysis in MOBA game from a different perspective.

This paper is divided into the following section. First, we discuss previous work in more detail outlining the open problems given the work done in MOBA games. Second, we discuss the game we used and the dataset. Third, we discuss the algorithms used and results obtained. We then discuss the results in more detail. We conclude by outlining the contribution and applications of the results.

% You must have at least 2 lines in the paragraph with the drop letter
% (should never be an issue)
%I wish you the best of success.

%\hfill mds

%\hfill August 26, 2015

%\subsection{Subsection Heading Here}
%Subsection text here.

%\subsubsection{Subsubsection Heading Here}
%Subsubsection text here.

\section{Previous Work}
A study by Christoph Eggert and team \cite{Eggert2015} which classified players into sets of classes and segments of games with respect to their roles, effectiveness in time (early/late) and support items/ damage types. Using Logistic Regression, Random Forest and Bayesian Networks to reduce the set of player classes for better accuracy in predicting the winner. A team-based approach to MOBA is similar but on aspects divided on roles. Limitations may include predetermining roles in the game which may lead to some early misdirection in team formation.

 Personality aspects have also been taken into consideration while forming a team where the study investigated how personality trait and expertise affect virtual team interactions \cite{Balthazard2004}. Using correlation analysis, regression analysis, and a series of post hoc t-tests they were able to hypothesize the mechanisms through which personal characteristics of individuals are aggregated via group-level dynamics to produce group-level outcomes and approached the  team v/s individual performance based on personality traits. They concluded that the results were preliminary and since they were formed into interdependent teams for only the relatively brief duration of their task it cannot be used universally.

Another team analysis 'Learning Dota 2 Team Compositions' \cite{Agarwala2014}, studied teams using PCA and second order PCA with Logistic regression was done for a different MOBA game Dota 2, using hero composition. They concluded that cleaner data or better models are needed. Factors responsible may have been player skills which were not taken into consideration.

The clustering algorithm used in the paper Player Behavior and Optimal Team Composition based on champion types is done in Online Multiplayer Game study based on champion types by Hao Yi Ong and team \cite{Bainbridge2009} was effective in forming teams based on champion types. The focus in this paper is on player types like ambush-er, magic, physical, support etc. and team composition from that, whether a specific class of champions has any effect on winning. It uses clustering of players based on their behaviors, visualizing the data using PCA and predicting the winner using classification. Factors not taken into consideration was team play behaviors like assists and player skill-based classification.

Research done in similar area  Player Skill Decomposition in Multiplayer Online Battle Arenas \cite{Chen2016} looked at 14 cooperative games to find out game-play design aspects which determine the interaction between player. Their research showed that helping occurred when the game was difficult for players which may be a factor in teams which win in the league of legends. Results may be time dependent and as the game changes rapidly over the years, player strategies may have evolved differently from MOBA games.

Making use of game log data, 'On Successful Team Formation' \cite{Pobiedina2013b} chose a statistical approach to identify factors that increase the chance of a team to win. Their hypothesis being better role distribution in a team increases the chance to win a game,     teams with more experienced players have a higher chance to win, playing with friends increases the chance to win and
the selection of a proper leader as well as a good matching of heroes inside a team positively influence the success. Using ANOVA test and Mann-Whitney-Wilcoxon-tests they were able to identify better Individual Hero Selection vs Team Hero Selection with log-linear analysis. In this approach, specific Gameplay elements not considered the part of analysis since MOBAs tend to be different from other online multiplayer games where gameplay aspects like inhibitors, dragons are quintessential to form strategies it falls short.

Effectiveness of Machine Learning algorithms in predicting game outcome by systematic review and compare performance of most frequently used machine learning algorithms for prediction of the match winner from the teams' drafts in DotA 2 computer game \cite{Semenov} deals with algorithms such as Naive Bayes classifier, Logistic Regression and Decision trees to validate consistency in data mining. Using the algorithms this paper comes up with standard performance metrics for players. This paper deals with different algorithms than the ones previously presented.

\section{Game and Data}
The data set consists of about two million League of Legends (LOL) matches that happened in 2015 summer retrieved using riots API system. The game mode is called 5-vs-5 ranked matches of a solo queue which is extensively played MOBA mode. A typical such match involves ten players who form two teams of five. Each match consists of ten rows with statistics of each player as shown in Fig 1. Star player and team data set are segregated which will consist of two rows per match. In the Star player data set, a player who falls under the category of the star player will be placed on each team and in the team data set aggregate of all the player from each team will make two rows per match.

\begin{figure}[!t]
%\centering
\includegraphics[width=\linewidth]{tab4}
% where an .eps filename suffix will be assumed under latex,
% and a .pdf suffix will be assumed for pdflatex; or what has been declared
% via \DeclareGraphicsExtensions.
\caption{Dataset with retrieved from riot's API}
\label{fig_sim}
\end{figure}

\section{Feature Extraction}
We derived several features from the given data above:
\begin{itemize}
  \item \textbf{Star Player}  Using backward feature selection which includes all the predictors and recursively removes the predictors which are less influential, goldEarned was the most important predictor with Akaike information criterion that overrules other predictors. The findings here were corroborated in the heat map of the predictors show that gold earned supersedes every other predictor by huge margins \cite{Patterson}.
  \item \textbf{Team features}  A similar approach is made as with the star player analysis. Using backward feature selection on assist components of the game which reduces to totalDamageDealt, firstTowerAssist, firstBloodAssist, assists, and firstInhibitorAssist.
\end{itemize}

\section{Team Features vs. Star Player affecting Win/Loss in Moba Game}

We considered and compared several methods to predict the effect of team vs. star player as features for predicting win/loss.
After the separation of data set into two distinctive halves, we tried to form a learning model based on the features. The datasets comprised of categorical and quantitative data so every algorithm used had its pros and cons. When choosing reasonable methods, some dimensions are considered. For example, the number of training examples, the feature space dimensionality, the relationship between features, the linearly dependent expiations between features and target variable (winner), the problem of overfitting and the computer system’s capacity on running data analysis. Based on the dimensions we considered, these five models were chosen.

\begin{itemize}
  \item \textbf{Logistic Regression}
We chose this method due to we expect the LOL data features are roughly linear and the hypothesis problem to be linearly separable. This method is also efficient. Also, since LR output can be interpreted as a probability, it is good for predicting winning or losing.

  \item \textbf{Linear Discriminant Analysis }
Also known as Fisher Linear Discriminant (FLD), is a classical algorithm for pattern recognition. It is an effective feature extraction method. Using this method, the inter-class scatter matrix of the post-projection pattern samples can be maximized, and the intra-class scatter matrix is minimized. In other words, it can guarantee the smallest-in-class distance and the largest inter-class distance in the new space, that is, the pattern can be best separated in that space. However, LDA is not effective when sample information is dependent on variance rather than mean.

  \item \textbf{Quadratic Discriminant Analysis }
LDA requires an assumption of equal variance-covariance matrices between the input variables of the classes. QDA is a modification of LDA which allows for the above heterogeneity of classes' covariance matrices. Since in our team dataset we can't be sure whether the covariance of each of the classes is identical or not it is a good idea to use QDA as well. And it can be used to build the model for more problems. The difference is, when the covariance matrices of different categorical samples are the same, LDA should be chosen. Otherwise, QDA should be used. The reason we use both LDA and QDA is to test which method works better on our problem.

  \item \textbf{Regression Tree}
A Decision Tree (DT) is a graph that uses a branching method to illustrate every possible outcome of a decision. Generally, DT is easier to understand and be explained to most people. Since DT is nonparametric, no worry is needed about whether the data and the outliers are linearly separable. DT’s main drawback is that it is easy to over-fit, which makes the random forest (Random Forest, RF) (or Boosted tree) and other integrated learning algorithm arise. The R package we use is rpart. It solves the over-fitting problem through prune method. It firstly builds a complicated tree model and then estimates the error of each model under different” pruning” conditions according to the Cross-Validation method. This model may prove better as our dataset may contain lots of outliers especially when we analyze the star player. Also, it is useful for our data to be explained in a straightforward way.

  \item \textbf{Clustering}
Another approach is based on unsupervised learning which is different from all the models used above.In clustering we do not train the data set to predict winning, we simply form groups of players with similar characteristics in terms of being a star player or team player. We’ll use our initial training set without segregating it into teams and star players. K-means is a clustering algorithm which tries to form initial cluster centroids and proceeds by repeating cluster assignments and updating centroids. These steps are performed until the algorithm converges. Using the k-means clustering method we’ll append each player a cluster number to which they belong.
So the dataset currently looks like in Fig. 3.

%----\begin{figure}[!t]
%\centering
%----\includegraphics[width=\linewidth]{tab3}
% where an .eps filename suffix will be assumed under latex,
% and a .pdf suffix will be assumed for pdflatex; or what has been declared
% via \DeclareGraphicsExtensions.
%----\caption{Dataset with a column named cluster included for every player}
%----\label{fig_sim}
%-----\end{figure}

 K-means starts with a random choice of cluster centers and needs the number of clusters to be specified we have to plot and see the number of clusters appropriate for the analysis.

\begin{figure}[!t]
%\centering
\includegraphics[width=\linewidth]{tab4}
% where an .eps filename suffix will be assumed under latex,
% and a .pdf suffix will be assumed for pdflatex; or what has been declared
% via \DeclareGraphicsExtensions.
\caption{K-means clustering options}
%\label{fig_sim}
\end{figure}

 From the Fig. 4, five seems to be a good enough cluster choice. At this point, every player in the game will be in a cluster between 1 and 5. For the team analysis now every team will have a score between 5 and 25 by doing the cluster number aggregation. From this number we’ll predict the winner. As the predictors are in higher dimension we’ll use PCA to visualize the data point and which classification method to use. PCA involves all the predictors which constitute to a cooperative gameplay like assists,totalDamageDealt,firstTowerAssist etc. The data points can be seen in Fig. 5.

\begin{figure}[!t]
%\centering
\includegraphics[width=\linewidth]{tab5}
% where an .eps filename suffix will be assumed under latex,
% and a .pdf suffix will be assumed for pdflatex; or what has been declared
% via \DeclareGraphicsExtensions.
\caption{3D representation of data points using PCA}
%\label{fig_sim}
\end{figure}

 From Fig 5, it seems like data points can be separated through a plane, which provokes the idea of using a support vector machine (SVM). SVM has high classification accuracy and has a good theoretical guarantee to over-fitting. Through selecting appropriate kernel function, it can function well even when facing problems that are not linearly separable. Since SVM is good for highly dimensional space data too, it may prove to be a good choice for prediction.

\end{itemize}

\section{Results}

The validation of results is done using 10-fold cross validation method which divides the dataset into 10 subsets, and the holdout method is repeated 10 times. Each time, one of the 10 subsets is used as the test set and the other 9 subsets are put together to form a training set. Then the average error across all 10 trials is computed. The advantage of this method is that it matters less how the data gets divided. Every data point gets to be in a test set exactly once and gets to be in a training set 9 times. In every method, a confusion matrix is created 10 times for each fold. The accuracy in each of the confusion matrix is recorded and the average is considered. This method of validation is propagated across all the methods used.

Since the objective of this analysis is to compare team versus star player gameplay behavior and observe winning 10-fold validation for star player data set needs to be done as well. Every aspect of the process remains the same as above just the data set and model for prediction is changed.
A detailed team versus star player result in is shown in table 1.

% Table generated by Excel2LaTeX from sheet 'Sheet1'
\begin{table}[htbp]
  \centering
  \caption{Comparison of all the models used}
    \begin{tabular}{|l|r|r|}
    \toprule
    Model & \multicolumn{1}{l|}{mean F1 score TEAM} & \multicolumn{1}{l|}{mean F1 score STAR} \\
    \midrule
    LDA   & 0.772 & 0.748 \\
    \midrule
    QDA   & 0.771 & 0.741 \\
    \midrule
    Logistic Regression & 0.769 & 0.747 \\
  \midrule
    Decision Tree & 0.73  & 0.692 \\
    \bottomrule
    \end{tabular}%
  \label{tab:addlabel}%
\end{table}%

The results suggest a higher prediction of winning for a team based gameplay in every method chosen. Team play predictors yield better accuracy in predicting win than star play predictors. Even though the difference might be close in some of the methods it still suggests that a cooperative gameplay when playing league of legends yields better accuracy. League of Legends certainly imposes competition between groups of players ("coalitions") with external enforcement of cooperative behavior by forming a team, including support players and common objective which is the requirement of a cooperative game. Considering league as a cooperative game a team will win if the payoff of a set of players is high by forming a coalition. The payoff for a player is to be determined by forming a team and having a more cooperative gameplay. The intuition of fun is also included in a cooperative gameplay; players will be more involved in the game if they have a better coalition with other players.

\section{Conclusion}

A deeper analysis can be made for team versus star players if champion roles are factored in along with player activities at different moments in the match. Currently, Riot's API only allows to collect data only after the match is finished, it would be interesting to research player activities during the game. Clustering approach doesn’t work as good maybe the columns used to form clusters are not sufficient. We are making clusters of all the players based on their assist measures like “assists”, “firstInhibitorAssist”, “firstTowerAssist”, etc. most of which are discrete and shrinks the dimensions of the clusters. We need more factors that constitute to a player being involved in the cooperative approach. Either from the IPA provided by Riot of forming a measure based on the given dataset. If we can cluster people who are good at cooperative gameplay together we can predict which type of players win better. Riot’s internal mechanism of teaming players may already take this factor into consideration which means that players may be teamed based on their style of gameplay.

% An example of a floating figure using the graphicx package.
% Note that \label must occur AFTER (or within) \caption.
% For figures, \caption should occur after the \includegraphics.
% Note that IEEEtran v1.7 and later has special internal code that
% is designed to preserve the operation of \label within \caption
% even when the captionsoff option is in effect. However, because
% of issues like this, it may be the safest practice to put all your
% \label just after \caption rather than within \caption{}.
%
% Reminder: the "draftcls" or "draftclsnofoot", not "draft", class
% option should be used if it is desired that the figures are to be
% displayed while in draft mode.
%
%\begin{figure}[!t]
%\centering
%\includegraphics[width=2.5in]{myfigure}
% where an .eps filename suffix will be assumed under latex,
% and a .pdf suffix will be assumed for pdflatex; or what has been declared
% via \DeclareGraphicsExtensions.
%\caption{Simulation results for the network.}
%\label{fig_sim}
%\end{figure}

% Note that the IEEE typically puts floats only at the top, even when this
% results in a large percentage of a column being occupied by floats.

% An example of a double column floating figure using two subfigures.
% (The subfig.sty package must be loaded for this to work.)
% The subfigure \label commands are set within each subfloat command,
% and the \label for the overall figure must come after \caption.
% \hfil is used as a separator to get equal spacing.
% Watch out that the combined width of all the subfigures on a
% line do not exceed the text width or a line break will occur.
%
%\begin{figure*}[!t]
%\centering
%\subfloat[Case I]{\includegraphics[width=2.5in]{box}%
%\label{fig_first_case}}
%\hfil
%\subfloat[Case II]{\includegraphics[width=2.5in]{box}%
%\label{fig_second_case}}
%\caption{Simulation results for the network.}
%\label{fig_sim}
%\end{figure*}
%
% Note that often IEEE papers with subfigures do not employ subfigure
% captions (using the optional argument to \subfloat[]), but instead will
% reference/describe all of them (a), (b), etc., within the main caption.
% Be aware that for subfig.sty to generate the (a), (b), etc., subfigure
% labels, the optional argument to \subfloat must be present. If a
% subcaption is not desired, just leave its contents blank,
% e.g., \subfloat[].

% An example of a floating table. Note that, for IEEE style tables, the
% \caption command should come BEFORE the table and, given that table
% captions serve much like titles, are usually capitalized except for words
% such as a, an, and, as, at, but, by, for, in, nor, of, on, or, the, to
% and up, which are usually not capitalized unless they are the first or
% last word of the caption. Table text will default to \footnotesize as
% the IEEE normally uses this smaller font for tables.
% The \label must come after \caption as always.
%
%\begin{table}[!t]
%% increase table row spacing, adjust to taste
%\renewcommand{\arraystretch}{1.3}
% if using array.sty, it might be a good idea to tweak the value of
% \extrarowheight as needed to properly center the text within the cells
%\caption{An Example of a Table}
%\label{table_example}
%\centering
%% Some packages, such as MDW tools, offer better commands for making tables
%% than the plain LaTeX2e tabular which is used here.
%\begin{tabular}{|c||c|}
%\hline
%One & Two\\
%\hline
%Three & Four\\
%\hline
%\end{tabular}
%\end{table}

% Note that the IEEE does not put floats in the very first column
% - or typically anywhere on the first page for that matter. Also,
% in-text middle ("here") positioning is typically not used, but it
% is allowed and encouraged for Computer Society conferences (but
% not Computer Society journals). Most IEEE journals/conferences use
% top floats exclusively.
% Note that, LaTeX2e, unlike IEEE journals/conferences, places
% footnotes above bottom floats. This can be corrected via the
% \fnbelowfloat command of the stfloats package.

% conference papers do not normally have an appendix

% use section* for acknowledgment
\section*{Acknowledgment}

The authors would like to thank...

% trigger a \newpage just before the given reference
% number - used to balance the columns on the last page
% adjust value as needed - may need to be readjusted if
% the document is modified later
%\IEEEtriggeratref{8}
% The "triggered" command can be changed if desired:
%\IEEEtriggercmd{\enlargethispage{-5in}}

% references section

\medskip

\bibliographystyle{plain}
\bibliography{mypaper_references}

% can use a bibliography generated by BibTeX as a .bbl file
% BibTeX documentation can be easily obtained at:
% http://mirror.ctan.org/biblio/bibtex/contrib/doc/
% The IEEEtran BibTeX style support page is at:
% http://www.michaelshell.org/tex/ieeetran/bibtex/
%\bibliographystyle{IEEEtran}
% argument is your BibTeX string definitions and bibliography database(s)
%\bibliography{IEEEabrv,../bib/paper}
%
% <OR> manually copy in the resultant .bbl file
% set second argument of \begin to the number of references
% (used to reserve space for the reference number labels box)

%\begin{thebibliography}{1}

%\end{thebibliography}

% that's all folks
\end{document}

max_stars_repo_path: FDG March Paper/fdg_paper2017.tex

max_stars_repo_name: gautambaghel/Research

max_issues_repo_path: FDG March Paper/fdg_paper2017.tex

max_issues_repo_name: gautambaghel/Research

max_forks_repo_path: FDG March Paper/fdg_paper2017.tex

max_forks_repo_name: gautambaghel/Research


text:
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Freeman Curriculum Vitae
% XeLaTeX Template
% Version 3.0 (September 3, 2021)
%
% This template originates from:
% https://www.LaTeXTemplates.com
%
% Authors:
% Vel (vel@LaTeXTemplates.com)
% Alessandro Plasmati
%
% License:
% CC BY-NC-SA 4.0 (https://creativecommons.org/licenses/by-nc-sa/4.0/)
%
%!TEX program = xelatex
% NOTE: this template must be compiled with XeLaTeX rather than PDFLaTeX
% due to the custom fonts used. The line above should ensure this happens
% automatically, but if it doesn't, your LaTeX editor should have a simple toggle
% to switch to using XeLaTeX.
%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%----------------------------------------------------------------------------------------
%	PACKAGES AND OTHER DOCUMENT CONFIGURATIONS
%----------------------------------------------------------------------------------------

\documentclass[
	10pt, % Default font size, can be between 8pt and 12pt
]{../templates/FreemanCV}

\columnratio{0.55, 0.45} % Widths of the two columns, specified here as a ratio summing to 1 to correspond to percentages; adjust as needed for your content

% Headers and footers can be added with the following commands: \lhead{}, \rhead{}, \lfoot{} and \rfoot{}
% Example right footer:
%\rfoot{\textcolor{headings}{\sffamily Last update: \today. Typeset with Xe\LaTeX}}

%----------------------------------------------------------------------------------------

\begin{document}

\begin{paracol}{2} % Begin two-column mode

%----------------------------------------------------------------------------------------
%	YOUR NAME AND CURRICULUM VITAE TITLE
%----------------------------------------------------------------------------------------

\parbox[][0.09\textheight][c]{\linewidth}{ % Box to hold your name and CV title; change the fixed height as needed to match the colored box to the right
	\centering % Horizontally center text

	{\sffamily\Huge Edoardo Ghini} % Your name

	\medskip % Vertical whitespace

	{\Huge\textcolor{headings}{Robotics Engineer}}

	\vfill % Push content to the top of the box
}

%----------------------------------------------------------------------------------------
%	Brief personal description
%----------------------------------------------------------------------------------------
\section{Brief description}

  Curious and \textbf{self-confident} person, level-headed and quite an experimenter.
Passionate about programming and believing it to be a form of art.
  Fascinated by mysteries of \textbf{science} and firm believer in technological progress.
Enthusiastic about the latest academic discoveries in my field of expertise.
  Looking forward to learning more about Neuroscience and Human Consciousness and combine them together with \textbf{Robotics} and \textbf{Artificial Intelligence}.

%----------------------------------------------------------------------------------------
%     WORK EXPERIENCE
%----------------------------------------------------------------------------------------

\section{Work Experience}

% Each job is added with a \jobentry command. Below is an empty one to use as a template:

%\jobentry
%	{} % Duration
%	{} % FT/PT (full time or part time)
%	{} % Employer
%	{} % Job title
%	{} % Description

% All 5 parameters must be supplied but any can be empty if you don't need them

%------------------------------------------------

\jobentry
	{Current, from Oct 2020} % Duration
	{FT} % FT/PT (full time or part time)
        {INRIA, French national research institute} % Employer
	{Robotics Engineer} % Job title
	{
          Developed a system from the ground up to \textbf{teleoperate} an industrial robot in hazardous environments.
          Each module of the pipeline is written in C++ and it is containerized with \textbf{Docker} and communicate through \textbf{ROS} middleware.
          Dynamics of the system is simulated in a \textbf{digital twin} using \textit{dart} and \textit{gazebo}.
          Joint-space and Cartesian control of the robot through \textit{pinocchio} and \textit{tsid} libraries.
          Designed a \textbf{GUI} for teleoperation with C++ library \textit{ImGui} that introduces interactive \textbf{automation} of the task.
          Experience in URDF creation, modern C++ frameworks and libraries interfacing and
          acquaintance with robots of the lab: \textit{franka}  manipulator \& \textit{talos} humanoid robot.
        }
%------------------------------------------------

\jobentry
	{Feb 2019 -- Oct 2019} % Duration
	{FT} % FT/PT (full time or part time)
	{La Sapienza, University of Rome} % Employer
	{Master's Thesis} % Job title
        {Implemented a robotic system to achieve autonomous navigation (\textbf{SLAM}) in an urban environment of a mobile robot equipped with a \textbf{3D-LIDAR} laser sensor.
         The whole project has been implemented in \textbf{C++} adopting the ROS build system.
         High-level features are extracted from the 3D-point cloud and categorized in geometric primitives.
         The sensor data is processed using the primitives in order to compute the trajectory of the robot.
         Usesd a probabilistic approach that involves using the \textbf{Gaussian assumption} and a \textbf{Least Square} formulation.
         The work has been developed in collaboration with the Robotics Laboratory of La Sapienza University.\\
         \href{https://github.com/dinies/MasterThesis-ArtificialIntelligence-Robotics/blob/master/MaterThesis_Edoardo_Ghini.pdf}{\textbf{Master thesis link}}
         }

%------------------------------------------------

\jobentry
	{Mar 2016 -- Jul 2016} % Duration
	{FT} % FT/PT (full time or part time)
	{Translated} % Employer
	{Back-end developer} % Job title
	{
          During this internship, I was responsible for the codebase of a web application: \textbf{Matecat}, written in PHP.
          I developed unit-tests to certify the correctness of the core of the application.
          Brought code coverage percentage from 0\% to 25\%.
          Worked with databases and client-server communications: \textbf{MySQL} and \textbf{Apache}.
          Learned how to work in \textbf{agile} teams, following \textbf{scrum} principles.
          Acquired deep knowledge of advanced testing techniques: \textbf{mock objects}, \textbf{reflection}, and \textbf{TDD}.\\
          \href{https://github.com/dinies/BachelorThesis/blob/master/EdoardoGhiniThesis.pdf}{\textbf{Bachelor thesis link}}
        }

\switchcolumn % Switch to the second (right) column

%----------------------------------------------------------------------------------------
%	COLORED CONTACT DETAILS BOX
%----------------------------------------------------------------------------------------

\definecolor{Sky}{RGB}{204,230,255}
\parbox[top][0.11\textheight][c]{\linewidth}{ % Box to hold the colored box; change the fixed height as needed to match the box to the left
	\colorbox{White}{ % Create colored box and specify background color
		\begin{supertabular}{@{\hspace{3pt}} p{0.05\linewidth} | p{0.775\linewidth}} % Start a table with two columns, the table will ensure everything is aligned
			\raisebox{-1pt}{\faHome} & Nancy, France \\ % Address
			\raisebox{-1pt}{\faPhone} & +33 6 73 03 31 71  (FR) \\ % Phone number
			\raisebox{-1pt}{\small\faEnvelope} & \href{mailto:ghiniedoardo@gmail.com}{ghiniedoardo@gmail.com} \\ % Email address
			%\raisebox{-1pt}{\small\faDesktop} & \href{https://www.LaTeXTemplates.com}{https://www.LaTeXTemplates.com} \\ % Website
			\raisebox{-1pt}{\faGithub} & \href{https://github.com/dinies}{github.com/dinies} \\ % GitHub profile
			\raisebox{-1pt}{\faLinkedinSquare} & \href{https://www.linkedin.com/in/dinies/}{linkedin.com/in/dinies} \\ % LinkedIn profile
			% See fontawesome.pdf in the Fonts folder for all icons you can use
		\end{supertabular}
	}
	\vfill % Push content to the top of the box
}

%----------------------------------------------------------------------------------------
%	EDUCATION
%----------------------------------------------------------------------------------------

\section{Education}

% Each qualification entry is added with a \qualificationentry command. Below is an empty one to use as a template:

%\qualificationentry
%	{} % Duration
%	{} % Degree
%	{} % Honors, achievements or distinctions (e.g. first class honors)
%	{} % Department
%	{} % Institution

% All 5 parameters must be supplied but any can be empty if you don't need them

%------------------------------------------------

\begin{supertabular}{r l} % Start a table with two columns, the table will ensure everything is aligned

	%------------------------------------------------

	\qualificationentry
		{2016 -- 2019} % Duration
		{MScEng} % Degree
		{final grade 103 /110} % Honors, achievements or distinctions (e.g. first class honors)
		{Master in Artificial Intelligence and Robotics} % Department
		{La Sapienza, University of Rome} % Institution

	%------------------------------------------------

	\qualificationentry
		{2013 -- 2016} % Duration
		{BSc} % Degree
		{final grade 95 /110} % Honors, achievements or distinctions (e.g. first class honors)
		{Computer Engineering} % Department
		{Roma Tre University} % Institution

\end{supertabular}

%----------------------------------------------------------------------------------------
%	COMPUTER SKILLS
%----------------------------------------------------------------------------------------

\section{Programming Skills}

% This section is laid out using a table. A \tableentry command adds lines with the following parameters:

%\tableentry{Heading}{Content}{spaceafter}
% All 3 parameters must be supplied but any can be empty if you don't need them
% A "spaceafter" value in the third parameter will add some vertical space -- this is to be used between headings, leave it empty for no extra space

%------------------------------------------------

\begin{supertabular}{r l} % Start a table with two columns, the table will ensure everything is aligned

	\tableentry{Languages}{C++,\hspace{0.05cm} python,\hspace{0.05cm} \LaTeX,\hspace{0.05cm} Javascript }{}
	\tableentry{}{ Java,\hspace{0.05cm} bash,\hspace{0.05cm} MATLAB,\hspace{0.05cm} PHP }{spaceafter}
	%------------------------------------------------
	\tableentry{C++20}{ variadic templates,\hspace{0.05cm} move semantic }{}
	\tableentry{}{ smartpointers,\hspace{0.05cm} concepts,\hspace{0.05cm} lambdas }{spaceafter}
	%------------------------------------------------
        \tableentry{Design}{OOP,\hspace{0.05cm} polymorphism,\hspace{0.05cm} functional programming }{spaceafter}
	%------------------------------------------------
	\tableentry{Testing}{TDD,\hspace{0.05cm} reflection,\hspace{0.05cm} mock objects,\hspace{0.05cm} googletest }{spaceafter}
	%------------------------------------------------
	\tableentry{Libraries}{OpenCV,\hspace{0.05cm} tensoflow,\hspace{0.05cm} OpenGL,\hspace{0.05cm} dart,\hspace{0.05cm} ImGui }{spaceafter}
	%------------------------------------------------
	\tableentry{DevOps}{ cmake,\hspace{0.05cm} Docker,\hspace{0.05cm} git,\hspace{0.05cm} vim,\hspace{0.05cm} gdb,\hspace{0.05cm} valgrind}{spaceafter}
	%------------------------------------------------
\end{supertabular}

%----------------------------------------------------------------------------------------
%	THEORETICALSKILLS
%----------------------------------------------------------------------------------------

\section{Theoretical Skills}

% This section is laid out using a table. A \tableentry command adds lines with the following parameters:

%\tableentry{Heading}{Content}{spaceafter}
% All 3 parameters must be supplied but any can be empty if you don't need them
% A "spaceafter" value in the third parameter will add some vertical space -- this is to be used between headings, leave it empty for no extra space

%------------------------------------------------

\begin{supertabular}{r l} % Start a table with two columns, the table will ensure everything is aligned

	%------------------------------------------------

	\tableentry{Robotics }{ dynamic systems evolution,\hspace{0.05cm} quaternions }{}
	\tableentry{Control }{inverse dynamics,\hspace{0.05cm} robust control }{spaceafter}

	%------------------------------------------------

	\tableentry{Robotic }{ SLAM,\hspace{0.05cm} trajectory planning}{}
	\tableentry{Navigation }{ obstacle avoidance,\hspace{0.05cm} filtering }{spaceafter}

	%------------------------------------------------

	\tableentry{Machine}{ bioinspired networks,\hspace{0.05cm} CNN }{}
	\tableentry{Learning}{ spiking neurons,\hspace{0.05cm} LSTM }{spaceafter}

	%------------------------------------------------
        \tableentry{artificial}{ multiagent systems,\hspace{0.05cm} reinforcement learning}{}
	\tableentry{intelligence}{ first order logic,\hspace{0.05cm} planning and reasoning}{spaceafter}

        \tableentry{computer}{ operative systems,\hspace{0.05cm} network protocols }{}
	\tableentry{science}{ algorithms design,\hspace{0.05cm} databases }{spaceafter}

\end{supertabular}

%----------------------------------------------------------------------------------------
%	REFERENCES
%----------------------------------------------------------------------------------------

\section{References}

%\textit{References available on request} % Uncomment if you'd rather not include references and remove the section below

% This section is laid out using a table. A \tableentry command adds lines with the following parameters:

%\tableentry{Heading}{Content}{spaceafter}
% All 3 parameters must be supplied but any can be empty if you don't need them
% A "spaceafter" value in the third parameter will add some vertical space -- this is to be used between headings, leave it empty for no extra space

\begin{supertabular}{r l} % Start a table with two columns, the table will ensure everything is aligned
        \tableentry{}{\href{https://members.loria.fr/SIvaldi/}{\textbf{Dr. Serena Ivaldi}}}{}
	\tableentry{Position}{Research scientist}{}
	\tableentry{Employer}{\href{https://www.inria.fr/}{INRIA}}{}
        \tableentry{Email}{serena.ivaldi@inria.fr}{spaceafter}
        \tableentry{}{\href{https://sites.google.com/dis.uniroma1.it/grisetti/home}{\textbf{Dr. Giorgio Grisetti}}}{}
	\tableentry{Position}{Professor}{}
	\tableentry{Employer}{\href{https://www.uniroma1.it/}{La Sapienza, University of Rome}}{}
        \tableentry{Email}{grisetti@diag.uniroma1.it}{}
\end{supertabular}

\end{paracol} % End two-column mode

\textcolor{headings}{Languages:} \qquad \textbf{Italian:}  native \qquad
                                \textbf{English:}  IELTS academic cert. Overall band score \textbf{7.0} CEFR level \textbf{C1}\qquad
                                \textbf{French:} level \textbf{A2}
\smallskip

\textcolor{headings}{Privacy:}\quad"In compliance with the GDPR and Italian Legislative Decree no. 196 dated 30/06/2003, I hereby authorize the recipient of this document to use and process my personal details for the purpose of recruiting and selecting staff and I confirm to be informed of my rights in accordance to art. 7 of the above mentioned Decree".

\end{document}

ext: tex

max_stars_repo_name: dinies/CV

max_issues_repo_name: dinies/CV

max_forks_repo_name: dinies/CV


text:
\chapter*{Honor Code}
We certify that we have properly cited any material taken from other sources and have obtained permission for any copyrighted material included in this report. We take full responsibility for any code submitted as part of this  project and the contents of this report.\\
% This space is for putting the signatures.
\vspace*{15mm}

\begin{flushright}
Author-1 (Entry No.)\\
\end{flushright}

\vspace*{15mm}

\begin{flushright}
Author-2 (Entry No.)\\
\end{flushright}

\vspace*{15mm}

\begin{flushright}
Author-3 (Entry No.)\\
\end{flushright}

\addcontentsline{toc}{chapter}{Honor Code}


text:
\chapter{Introduction}

{\red Intro paragraph here.}

\section{Motivation}
\label{section:Motivation}

\subsection{Threat Model}
From the perspective of verification, we would like to have confidence
that the file system is secure purely based on the file system's security
specification.  This means that we have to treat the developer of the
file system with an adversarial mindset. More specifically, we assume the developer may be malicious and intentionally deliver an implementation that can be exploited in the future, which we call \emph{an adversarial implementation}.
This subsumes all possible bugs that a well-meaning but error-prone developer might introduce into the implementation as well as any implementation that is designed to be exploited.

As a result, our threat model is that the adversary both develops the
file system and runs an adversarial application on top of the file system
in an attempt to obtain confidential file data.  However, the adversary
does provide a proof that their file-system implementation meets our
security specification.  The potential victim runs on top of the same
file system but sets their permissions so that the confidential files
are not accessible to the adversary's process.  Our goal is to ensure
that the security specification is so strong that it prevents leaks even
when the file-system developer is colluding with adversarial processes
running on top of the file system.

Our threat model is focused on proving that the file-system implementation has
no confidentiality bugs, rather than proving the absence of bugs in the
environment outside of the file system. Thus, we assume that our model
of how the file-system implementation executes is correct.  That is, we are not
concerned with bugs in unverified software or hardware outside of the file
system, or users mounting malicious disk images.  We do prove that
\texttt{mkfs} produces a correct image, but ensuring confidentiality on top of an
intentionally corrupted file system image is difficult, even without formal
verification. We also do not reason about timing channels, as we do not model time.

\subsection{Challenges}
\label{s:goal:chal}

A difficult aspect of formally proving the security of a file system lies
in guaranteeing confidentiality.  This is difficult because of four challenges:

\paragraph{1. Two-safety.}
First, proving confidentiality is more difficult than
proving functional correctness: because, confidentiality
is a two-safety property.  Functional correctness is a one-safety
property because a violation of functional correctness can be demonstrated
by a single execution.  For instance, if an application wrote one byte to
a file and then read back a different byte, this single execution shows
that the file system is incorrect.  Thus, functional correctness
of a file system is a theorem that says that all executions meet the
spec (i.e., there are no such violations).  Integrity properties,
such as ensuring that one user cannot corrupt another user's data,
are an example of a one-safety functional-correctness property and can
be handled using standard verification techniques.

In contrast, demonstrating a violation of confidentiality requires
two executions, where the results observed by an adversary differ depending on
the secret data.
%% %% TODO: We don't do this though. Maybe find a better example for this?
For instance, consider a file system with block-level deduplication that
also exposes the number of free blocks.  An adversary who wants to
learn the contents of a victim's file could write their guess for the
victim's block into the adversary's own file and then check whether
the number of free blocks stayed the same or decreased.  If the file
system implemented deduplication across users, this attack allows an
adversary to learn whether their guess block was already present in the
file system, thus inferring whether the victim has that data.

In the above example, looking at a single execution does not allow one
to directly conclude that data was leaked, because the system appears
to be functioning correctly.  Determining that data is leaking requires
one to consider a pair of executions, in which the adversary performs
the same operations, but the confidential user data is different.
If these two executions produce different adversary-observable results,
the adversary is able to infer information about confidential data.

By stating confidentiality as a two-safety property, the above
deduplication example would violate confidentiality, and thus could not
appear in an implementation that was proven to achieve confidentiality.
Specifically, suppose the starting states of the two executions differed
in the contents of a confidential file, where in one execution the file
matched the adversary's guess and in the other execution it didn't match.
In this case, the number of free blocks returned by the adversary
would differ in the two executions, which would not be allowed by the
confidentiality definition.

\paragraph{2. Nondeterministic specifications.}
Another challenge in proving confidentiality lies in the fact
that many specifications, including those in the file system, are
nondeterministic.  Some nondeterminism is unavoidable because file
systems must deal with crashes (e.g., due to power failure), which can
occur at any time.  Thus, it is impossible to
know what are the exact contents of the disk after a crash; the on-disk
state could reflect any prefix of the writes issued by the file system.
Modern disks complicate this situation even further by buffering writes
in memory inside the disk controller; as a result, the writes can be
made durable out-of-order, and the state of the disk after a crash might
reflect some out-of-order writes.  Even in the absence of crashes, the
file system implementation may want to use randomness (e.g., to randomize
directory hash tables), which makes the execution non-deterministic.

Other nondeterminism comes from specifications that hide irrelevant
details.  For instance, the inode allocator in the file system does
not specify which precise inode number will be returned; instead,
its specification simply states that it will return
\emph{some} inode number that is not already in use.

Any nondeterminism is a potential leak of confidential data.  The
nondeterministic specification of the block allocator from above does not
preclude the allocator from leaking confidential data, because it could,
in theory, choose the next inode number based on the confidential contents
of files, without violating its specification (i.e., still returning some
unused inode number).

Even the nondeterminism associated with the state of the disk
after a crash can be taken advantage of by an adversarial file-system
implementation to leak data.  For instance, a high-performance
file-system specification allows the file system to delay flushing data
to disk.  An adversarial implementation could choose whether to flush
data immediately or defer the flush based on one bit of confidential
data from a victim's file.  To take advantage of this, an adversary
could wait for the system to crash and, after the crash, check whether
any writes appear to have been lost.  If so, the adversary concludes
the file system must have deferred the writes, which would have only
happened if the confidential bit was zero.  This, in turn, can allow
the adversary to infer confidential bits.

\paragraph{3. Non-uniform outcome probabilities.}
Another challenge arises because an adversary may obtain
more precise information about the system by executing the same program repeatedly.
Such an action will allow the adversary to approximate \emph{frequencies} of
different outcomes of a program. which some confidential information may be inferred from. A simple example of this challenge can be seen in figure \ref{fig:Frequency_Leaking_Program}.

\begin{figure}[H]
\centering
    \begin{verbatim}
    if (get_random_bit() == 1)
      return secret_bit
    else
      return get_random_bit()
    \end{verbatim}
\caption{Example of a program that leaks information via return value frequencies}
\label{fig:Frequency_Leaking_Program}
\end{figure}

This code leaks the secret bit 50\% of the time and outputs a random bit 50\% of the time. It is also important to note that it can output 0 or 1 independently of the secret value. This way, any (state, return) pair represents a successful execution. Therefore, by observing just a single return value, an adversary cannot infer the value of the secret bit. However, the frequencies of the output values in table \ref{table:Return_value_distribution} shows that they correlate with the value of the secret bit.

\begin{figure}[H]
    \centering
\begin{tabular}{| c | c | c |}
	\hline
	Secret bit & Output \% 0 & Output \% 1 \\
	\hline
	0 &	75\% & 25\% \\
	\hline
	1 &	25\% & 75\% \\
	\hline
\end{tabular}
\caption{Distributions of return values for each state.}
\label{table:Return_value_distribution}
\end{figure}

Any adversary who can observe the output of this program sufficiently many times can infer the value of the secret bit with high confidence. These types of vulnerabilities are not limited to usage of randomization. They also manifest themselves when there are random events such as crashes that can affect the behavior of the system.

\paragraph{4. Indirect disclosure.}
Yet another challenge is that an adversarial
file system might not immediately leak confidential data.  For example,
an adversarial file system may wait for a legitimate user to read
confidential data, at which point the file system would be allowed to
access this data, since it has to return it to the user.  However, in
addition to returning this data, an adversarial file system could also
stash away a copy of it, so that the adversary can later retrieve it.
For instance, the file system could change the order of entries in an
on-disk directory structure, or change the allocated inode numbers or
block numbers, based on the confidential data that it wants to leak.
Preventing this attack is difficult because the adversarial file system
appears to have legitimate access to the user's data when operating on
behalf of that user.

\paragraph{5. File-system complexity.}
Finally, file systems are complex software. Linux ext4, for
instance, consists of approximately 50,000 lines of code.  Even the simple
verified DFSCQ file system consists of thousands of lines of executable
code~\cite{chen:dfscq}.  The proofs of functional correctness for DFSCQ
are already tens of thousands of lines of Coq code. The complexity of
proving two-safety, which is a more challenging property, could easily
spiral out of control.

\section{State of the Art: Information Flow Control}
De facto approach to specifying confidentiality is through the information flow control. An information flow control policy restricts and regulates transfer of information between different parts of the system.

One widely used confidentiality specification in information flow control literature is called \emph{noninterference}. Informally, noninterference states that "unprivileged users (a.k.a. low users) should observe the same behavior from the system regardless of a privileged users' (a.k.a. high users) actions in the system". Noninterference is formalized in many different computation models. In this thesis, we use the state-machine model since it fits better to the systems we create.

Although its widespread usage, noninterference is not suitable for many storage systems. The reason for that is it prohibits any transfer of information, both direct and indirect. However, storage systems sometimes expose effects of privileged users indirectly via metadata or some public information of the system like available free space. For example, in a file system, if a privileged user creates a file and writes to it, other users of the file system may see that he created a file, even though they may not see the file's contents. For many applications, this behavior is completely acceptable, even though noninterference prohibits it. Because of this, storage systems require a more flexible confidentiality specification.

\section{Solution Approaches}
We took two different approaches to address the mentioned challenges: (1) sealed blocks and data noninterference, and (2) nondeterminism oracles, abstractions and refinements. These approaches complement each other, and together, offer a solution to each of the challenges.

Our first approach sealed blocks and data noninterference addresses challenges 1, 2, 4, and partially 5. Sealed blocks reduce the two-execution property to a trace property, which is a one-execution property. Data noninterference allows nondeterministic specifications while preventing exploitation of such nondeterminism by implementation. Both of them reduced required proof effort significantly but required us to make simplifications in our implementation.

Second approach solves the challenges that first approach falls short.Nondeterminism oracles enable reasoning of individual nondeterministic events. This ability leads to a stricter confidentiality specification that prevents challenge 3, while still being flexible enough to prevent overly-verbose specifications. Abstractions and refinements encapsulate the complexity in small components and allow complex systems to be implemented in a modular fashion while keeping proof complexity in check.

We briefly explain all of the approaches below. We present more detailed explanations in the following chapters.

\subsection{Sealed Blocks and Data Noninterference}
Sealed blocks and data noninterference are our first attempt at addressing the challenges. Our implementation of these approaches address many of the challenges but also reveal the intricacies of specifying and proving confidentiality of storage systems, most notably challenge 3. Sealed blocks and data noninterference is briefly explained below.

\paragraph{Sealed Blocks}
We used sealed blocks approach to address challenge 1, that confidentiality proofs being harder and more complex than integrity proofs by turning two-execution proofs into trace properties, which require one-execution proofs. Key idea behind sealed blocks is that if a program's behavior does not depend on confidential data, then it is not possible for it to leak confidential data; since it will behave the same no matter what the data is. Sealed blocks achieve this via two mechanisms: (1) providing a way to handle data without accessing its contents, and (2) enforcing access control when the contents are accessed.

First mechanism achieved via an operation we call \emph{sealing}. It takes a piece of data and "seals" it with the owner of the data, by turning it into an abstract object that does not provide any functionality other than \emph{unsealing} it. This way, showing that a program's behavior does not depend on confidential data reduces into showing that it only handles the sealed data. Which can be done by a static analysis of the program.

However there is still fair amount of functionality that requires inspecting the contents of the data, especially for systems that uses on-disk data structures. An example of this is the bitmap of an allocator. To be able to allocate or free any resources,  it has to inspect and modify the contents of a bitmap. Second mechanism allows that while ensuring the program does not access any data that it is not permitted to access. Since sealed data require unsealing to access to the contents, each unseal operation can be detected and recorded during the execution, creating an \emph{unseal trace}. With unseal traces, showing that a program does not leak confidential data reduces to showing that its unseal trace only contains unseals that it is permitted to do so. This turns a two-execution proof into a one-execution proof because a program's unseal trace can be obtained by examining a single execution.

\paragraph{\red Data Noninterference}
We defined data noninterference as a solution to traditional noninterference being too strong for storage systems confidentiality. Data noninterference embodies the insight "if a program's behavior doesn't depend on confidential data, then it cannot leak confidential data via its return value".

\iffalse
{\red Not sure where to put this following part. Probably will be here so I am keeping it here for now.}\\
{\red .....}\\
At the core of the two-execution style noninterference definition lies the notion of "equivalent states" and preservation of that equivalence throughout the execution of the system. An informal description of noninterference can be stated as "a program is noninterfering when the program is executed from equivalent states, it preserves the equivalence of the resulting states and returns the same values". This description ensures two things: (1) states cannot be distinguished from a program's return values, (2) after-execution states cannot be distinguished in the future by running other noninterfering programs. A formalism of two-execution style noninterference can be seen in figure \ref{fig:NI_Definition}.

\begin{figure}[H]
    \centering
    \begin{verbatim}
    Definition Noninterference
        {T} (p: prog T)
       (R: state -> state -> Prop):=
      forall (s1 s2: state) (r1: T),
        exec s1 p (s1', r1) ->
        R s1 s2 ->
        exists s2' r2,
            exec s2 p (s2', r2) /\
            R s1' s2' /\
            r1 = r2.
    \end{verbatim}
    \caption{Formalization of two-executions noninterference}
    \label{fig:NI_Definition}
\end{figure}
{\red .....}\\

{\red .....}\\
A good way define equivalence of the states is "two states are equivalent if they are the same for their non secret parts". This definition makes all states equivalent to each other in our example, because the state is a single secret bit. Since any pair of state and return value is a valid execution, it is possible to find another execution from a related state with same return value. Therefore, this implementation satisfies the noninterference definition.

Figure \ref{fig:NI_Matching_Paths} illustrates how each execution matches with another from an equivalent state. Each arrow represents a possible execution of the program. On the labels, numbers in the brackets represent generated random bits, and the number following the brackets denotes the return value. Executions are colored based on their return values.
We can see that, for each execution, there is an execution with the same color  from the equivalent state.

\begin{figure}[H]
    \centering
    \includegraphics[scale=0.5]{templates/figures/matching-paths.png}
    \caption{Visualisation of \ref{fig:Frequency_Leaking_Program} satisfying noninterference.}
    \label{fig:NI_Matching_Paths}
\end{figure}

Although our example satisfies noninterference, the secret bit can be determined via the observed frequency of repeated calls.
{\red .....}\\
\fi

\subsection{Nondeterminism Oracles, Abstractions and Refinements}
Our second group of approaches addresses the challenges that is left unresolved by the first group. Nondeterminism oracles, abstractions and refinements incorporate the insights we obtained from our first attempt to obtain stronger specifications.

\paragraph{Nondeterminism Oracles}
Our approach to addressing challenge 3 is developing a technique to reason about each possible nondeterministic event individually. Such a technique enables confidentiality specifications that can require return value equality to hold for each possible nondeterministic event. If the return value equality holds for each nondeterministic event, then there are equal number of executions from equivalent states that leads to a particular return value, which implies that observed frequencies of return values will be preserved.

We achieved this via a technique we call \emph{nondeterminism oracles}. A nondeterminism oracle is an abstract object that, whenever the execution needs to make a nondeterministic choice, it "asks" oracle and chooses based on the oracle's answer. Therefore different oracles lead to different executions of the same program. Similarly, for a fixed oracle, execution becomes deterministic. This allows us to enforce return value frequencies to be the same by requiring return value equality for each oracle.

\paragraph{Abstractions and Refinement}
To tackle the complexity of file systems, we use abstractions. Being able to define abstractions at a desired points help containing and compartmentalizing the complexity in the system and reduces the proof complexity as implementations stack on top of each other. In our work, we use refinement for connecting abstractions to implementations where correction of the refinement is established by simulation proofs.

One possible complication is that it is known that noninterference is not necessarily preserved under simulations \ref{}. However nondeterminism oracles lead to a confidentiality specification that is preserved under simulations given that refinement satisfies a certain property. This condition will be explained in more detail in the following chapters.

\subsection{Implementations}
We implement our solution approaches in two frameworks: sealed blocks and data noninterference are implemented in DiskSec, and nondeterminism oracles, abstractions and refinements are implemented in ConFrm. To test the frameworks, We implement two file systems: SFSCQ for DiskSec, and ConFs for ConFrm. All the frameworks and systems are implemented in Coq proof assistant. They are extracted to Haskell to produce runnable code. Details of these frameworks and file systems will be explained in their respective chapters.

\section{Contributions}
There are four categories of contributions of this thesis: (1) proof strategies, (2) confidentiality specifications, (3) implementations of frameworks for confidentiality reasoning, and (4) confidential file systems with machine-checkable proofs.

\subsubsection*{Proof Strategies}
\begin{itemize}
\item Sealed blocks, a proof approach that factors out reasoning about confidentiality
  from most of the storage system code.

\item Oracles, a proof approach for reasoning about specific series of nondeterministic events.

\item Reboot functions, a proof approach for reasoning about specific outcome of a nondeterministic reboot process.

\item A meta-theory for preservation of RDNI through abstractions, including a modified simulation definition that incorporates oracles, reboot functions, and crash-reboot-recovery process.
\end{itemize}

\subsubsection*{Confidentiality Specifications}
\begin{itemize}
\item Data Noninterference, a confidentiality specification based on noninterference that captures discretionary access control and deals with nondeterminism due to crashes.

\item RDNI, a confidentiality specification based on noninterference that incorporates oracles, and reboot functions, and crash-reboot-recovery process. RDNI provides stronger guarantees than data noninterference under nondeterminism.
\end{itemize}

\subsubsection*{Framework Implementations}
\begin{itemize}
\item DiskSec, a framework for specifying and proving confidentiality
for storage systems that reduces proof effort by using sealed block approach.

\item ConFrm a framework for specifying and proving confidentiality that implements RDNI and its meta-theory. ConFrm provides support for implementing systems as layers of abstractions, defining refinements, and proving simulations.

\end{itemize}

\subsubsection*{Confidential File Systems}
\begin{itemize}
\item SFSCQ, the first file system with a machine-checked proof of
  confidentiality. SFSCQ uses data noninterference as its specification,
  and DiskSec for proving its confidentiality

\item ConFs, a first file system that uses checksum-based, encrypted logging with a machine-checked confidentiality proof. ConFs is implemented in ConFrm and uses RDNI as its confidentiality specification.

\item An evaluation that compares SFSCQ and ConFs to demonstrate the performance overheads of each approach.
\end{itemize}

\subsection{Limitations}
Both of our systems have certain limitations such as:

\begin{itemize}
    \item Both systems have termination insensitive specifications.
    \item DiskSec does not allow comparison of confidential data.
    \item SFSCQ has to execute recovery as the super user.
    \item ConFrm does not provide a program logic to help with proving properties of programs.
    \item ConFrm does not provide any help for proving confidentiality of the highest abstraction layer.
    \item ConFs does not have a buffer cache for fast reads and writes,
          indirect block pointers in inodes, or file names and directory structures.
    \item Both SFSCQ and ConFs has simple access control mechanisms.
\end{itemize}

\section{Outline}
Chapter \ref{chapter:Related_work} presents the related work in the literature. Chapter \ref{chapter:Disksec} explains proof ideas behind Disksec and its implementation details. Chapter \ref{chapter:SFSCQ} presents SFSCQ, first formally verified file system with a confidentiality specification. Chapter \ref{chapter:ConFrm} describes ConFrm, a confidentiality framework for implementing systems modularly and with strong guarantees regarding nondeterminism. Chapter \ref{chapter:ConFs} presents the structure and implementation of ConFs. Chapter \ref{chapter:Evaluation} evaluates the performance of both file systems. Chapter \ref{chapter:Conclusion} concludes the thesis.

\iffalse
%%%%Explain the reason why there are two and how they compare to each other.

%%%% Whole story here security expensive etc...
{\red From Proposal}
As computation and storage shift toward the cloud, the safety of computation and data is becoming increasingly important. Users expect their data stored in such systems to stay secret against malicious third parties. Precise descriptions of how such a system should behave to ensure confidentiality of the stored data are called confidentiality specifications. A confidentiality specification of a system both forces a system to maintain certain properties, and informs users about the safety guarantees that system provides.

Writing a confidentiality specification is generally more difficult than writing a correctness specification. To demonstrate the possible hardships of writing a specification that can prevent malicious implementations, we can look at a specification for the create() operation from our confidential file system ConFs. create() takes an owner and creates an empty file owned by the provided owner. Upon successful completion, it returns the inode number that identifies the file. A natural correctness specification for its return value could be “create() returns the index of the previously unused inode that now corresponds to the newly created file.” If we were only interested in functional correctness, this would be an acceptable specification. However, there is a substantial confidentiality problem associated with it. create() is allowed to return any inode number as long as it was unused at the time of the call. A malicious implementation of the file system can take advantage of this nondeterminism in the specification to pick the returned inode number and subsequently leak confidential data, e.g., last byte of the return value being equal to the first byte of a block that belongs to another user.

This problem, and others of the same nature, could be solved by writing a fully deterministic specification for create() that exactly pinpoints what it should return and what the file-system state should be after its completion. However, such a specification runs the risk to be overly verbose to a degree that specification is the implementation, obscuring the important parts of the specification, making it difficult to read and comprehend, and defeating one of the key purposes of writing a specification. Therefore, a good confidentiality specification should address such vulnerabilities in its scope, but should also abstract implementation details so it can be read, understood, and reviewed by humans. Finding the right balance between these conflicting requirements is what makes writing a confidentiality specification challenging.

Our proposed solution to the above problems is ConFrm, a framework for
implementing and proving the confidentiality of storage systems in a modular fashion. ConFrm provides a noninterference definition with better guarantees for nondeterministic behavior, as well as the required tools and necessary conditions for safety-preserving abstractions. These two components of ConFrm enable us to overcome the limitations of previous works and provide a simple yet powerful tool for implementing safe storage systems out of composable components..

To test the capabilities of ConFrm, we implemented ConFS, a confidential file system that is crash-resistant via checksum logging, transactional operations, and coarse-grained discretionary access control.

Both ConFrm and ConFS are implemented in Coq. All proofs are fully machine-checked to ensure their correctness.

{\color{red}From Disksec}
Many security problems today stem from bugs in software.  Although there
has been significant effort in reducing bugs through better testing,
fuzzing, model checking, and so on, subtle bugs remain and continue
to be exploited.  Machine-checked verification is a powerful approach
that can eliminate a large class of bugs by proving that an
implementation meets a precise specification.

Prominent examples of machine-checked security proofs include verification of
strict isolation (with confidentiality) for an OS kernel in CertiKOS~\cite{costanzo:certikos-infoflow},
seL4~\cite{murray:sel4-infoflow}, and Komodo~\cite{ferraiuolo:komodo}, as well as security proofs in Ironclad~\cite{hawblitzel:ironclad} about applications
like a password hasher and a notary service.  However, proving the
security of systems with rich sharing semantics, such as file systems,
is an open problem.  For example, unlike prior examples that focus on
strict isolation without controlled sharing, users in a file system
can share files with one another, and the underlying implementation
has shared data structures (such as a buffer cache or write-ahead log)
that contain data from different users.

Proving security for a file system requires addressing two key challenges.
The first challenge lies in \emph{specifying} security. Integrity can be
expressed as simply as a functional correctness property. Confidentiality is more
challenging to specify. For example, consider
a natural specification for \cc{readdir}, which allows the file system to return
the names in a directory in any order.  This nondeterminism could be
abused by a buggy or malicious file system to leak confidential file
data through careful manipulation of the order of \cc{readdir} results.
Furthermore, nondeterminism is essential to a file system, because file
systems must deal with crashes, which can occur nondeterministically
at any time.

One approach to specifying confidentiality is to formulate it as a
noninterference property, such as in most information-flow-control
systems.  This means that the execution of one process (a potential victim
processing confidential data) cannot influence the execution of another
process (an adversary trying to learn that data).  Noninterference can
be stated concisely, and is easy for applications to use.  However,
information-flow-control style guarantees are stronger than what file
systems aim for.  Instead, file systems aim for weaker notions of
confidentiality, along the lines of discretionary access control on
files that reveal some metadata, such as file lengths.

A second challenge lies in proving confidentiality.  Confidentiality is a
``two-safety'' property~\cite{terauchi:safety}, which requires reasoning
about \emph{pairs} of executions to show that an adversary cannot observe
any differences correlated with confidential data.  However, reasoning
about pairs of executions is more complicated than reasoning about a
single execution, which is sufficient for proving integrity and functional correctness.

% note: recent paper on this, Cartesian Hoare Logic for Verifying k-Safety
% Properties from PLDI 2016. There are other attempts at this that are simpler
% and targetted towards security.

This paper presents \sys, an approach for proving the security, and
specifically confidentiality, for storage systems, such as file systems.
The paper demonstrates the benefits of \sys by developing, specifying,
and proving the security of a file system in a prototype called \sfscq,
based on the DFSCQ file system~\cite{chen:dfscq}.

\sys addresses the specification challenge by using a notion of \emph{data
noninterference} that both matches what file systems aim to provide
and is concise and easy to use for applications.  Data noninterference
requires that an adversary's execution be independent of the contents of
individual files, but it allows the adversary to observe other metadata,
such as file length and directory entries, and allows for discretionary
access control (i.e., a user can choose to disclose their data).

To address the challenge of proving security, \sys factors out reasoning
about confidentiality from all other properties, such as functional
correctness.  \sys does so by introducing a notion of sealed blocks.
This builds on the intuition that file systems do not look inside of the
blocks that represent user file contents.  As a result, \sys is able to
treat confidential file blocks as opaque in much of the file-system code,
greatly reducing the need for manual proofs of two-safety that consider
pairs of executions.  The only manual proofs of two-safety are in the
top-level \cc{read} and \cc{write} system calls.

We implemented \sys and \sfscq in the Coq proof assistant~\cite{coq}.  All proofs of security are
machine-checked by Coq, eliminating the possibility of bugs that
violate \sfscq's specification.  An evaluation of \sfscq shows that its
specifications are complete enough to prove confidentiality of a simple
application.  The evaluation also shows that \sys's approach allowed us
to develop \sfscq with a modest amount of effort, and that \sfscq achieves
comparable performance to the DFSCQ file system that it is based on.

The contributions of this paper are:

\begin{CompactItemize}

\item \sfscq, the first file system with a machine-checked proof of
  confidentiality.  \sfscq has a concise specification that captures
  discretionary access control using data noninterference, and deals
  with nondeterminism due to crashes.

\item \sys, an approach for specifying and proving confidentiality
  for storage systems that reduces proof effort.  \sys uses the
  idea of sealed blocks to factor out reasoning about confidentiality
  from most of the file system code.

\item An evaluation that demonstrates that \sys's approach leads to
  negligible performance overheads in \sfscq, that it precludes the
  possibility of confidentiality bugs that have been found in existing
  file systems, and that \sfscq's specification allows applications to
  reason about their confidentiality.

\end{CompactItemize}

Our \sfscq prototype has several limitations.
Since it relies on Coq's extraction to Haskell, inherited from DFSCQ,
its trusted computing base (TCB) includes the Haskell runtime and
compiler.
The version of \sfscq with fully machine-checked proofs does not support
changing permissions.
A newer version of \sfscq supports dynamic permissions but has a
few proofs that have not been repaired to reflect this change.
Finally, \sfscq's access-control mechanisms are relatively simple,
supporting owned and public files but not groups or separate read and
write permissions.

\fi

max_stars_repo_name: Atalay-Ileri/Disksec-Doc

max_issues_repo_name: Atalay-Ileri/Disksec-Doc

max_forks_repo_name: Atalay-Ileri/Disksec-Doc