steveej/msc-thesis
1
0
Fork 0
Code Issues 1 Pull requests Projects Releases 4 Packages Wiki Activity Actions

introduction: explain what memory safety is

Browse source
This commit is contained in:
steveej 2017-08-22 10:41:12 +02:00
parent 948530826f
commit d6009ea334
5 changed files with 165 additions and 59 deletions
Download patch file Download diff file Expand all files Collapse all files

2
shell.nix
View file

@ -142,7 +142,7 @@ in pkgs.stdenv.mkDerivation {
function! ViewerCallback() dict
call self.forward_search(self.out)
endfunction
"let g:vimtex_view_zathura_hook_callback = 'ViewerCallback'
let g:vimtex_view_zathura_hook_callback = 'ViewerCallback'
" }}}
autocmd BufWritePost * execute ':silent ! cp /home/steveej/src/mendeley/Static-Code-Analysis-Kernel-Memory-Saftey.bib /home/steveej/src/steveej/msc-thesis/src/docs/thesis.bib >/dev/null 2>&1'

39
src/docs/glossary.tex
View file

@ -94,6 +94,27 @@
},
}
\newglossaryentry{redoxos}{
name = Redox OS,
description = {
TODO
},
}
\newglossaryentry{blogos}{
name = Blog OS,
description = {
TODO
},
}
\newglossaryentry{tockos}{
name = Tock OS,
description = {
TODO
},
}
\newglossaryentry{rootfs}{
name = RootFS,
description = {
@ -227,9 +248,16 @@
}
\newglossaryentry{C}{
name=C programming language,
name=C,
, description={
TODO C
TODO C programming language,
}
}
\newglossaryentry{asm}{
name=Assembly programming language,
, description={
TODO ASM
}
}
@ -253,3 +281,10 @@
TODO sysadmin
}
}
\newglossaryentry{realtime}{
name=System Administrator
, description={
TODO realtime
}
}

150
src/docs/parts/context/context.tex
View file

@ -1,27 +1,115 @@
% // vim: set ft=tex:
\chapter{Introduction}
\label{context::introduction}
This thesis studies the feasibility of using static code analysis, as found in the \gls{Rust} \gls{compiler}, for ensuring safety within an \gls{OS} kernel.
This thesis studies the feasibility of using compile-time code analysis, as found in the \gls{Rust} \gls{compiler}, for ensuring memory-safety within an \gls{OS} kernel.
Because an \gls{OS} is nothing but a \gls{app}, this study could be applied to all \glspl{app}, but the focus is on the implementation of \glspl{OS} which is the \gls{app} that is responsible for managing the system's resources and provide abstractions for higher level applications.
The \gls{OS} is the only \gls{app} that has unrestricted access to these resources, with the task of managing these safely according to the rules that were set up by the \gls{sysadmin}.
The \gls{OS} is the only \gls{app} that required unrestricted access to these resources, with the task of managing them safely according to the rules that are either hard-coded or set up by the \gls{sysadmin}.
\section{A Definition of Memory Safety In The \gls{OS}}
A clear definition of memory safety is laid out in this section.
For decades computer systems are able to execute instructions that they have previously loaded into their main memory.
The details of loading the instructions for the \gls{OS} are irrelevant for the understanding, but it is assumed that the persistent memory that holds these instructions is the responsibility of the \gls{sysadmin} and not the \gls{OS}.
Once the \gls{OS} is in execution, it is responsible for loading the instructions and data for other \gls{app} into main memory.
This happens either automatically through configured jobs, or based on well-defined events which can be any form of input via the system's interfaces.
The latter is potentially dangerous because it requires an extensive amount of care and foresight from the developers of the \gls{OS} and \glspl{app} to prepare a system for the various events that might possibly occur.
This is not an easy task, especially if the interface or the environment of a system are diverse and complex.
\section{Memory And Safety}
\label{context::introduction::memory-safety}
% In Chapter 1 this is a summary of the methodology and contains a brief outline of three things: (a) the participants in a qualitative study or the subjects of a quantitative study (human participants are referred tyo as participants, non-human subjects are referred to as subjects), (b) the instrumentation used to collect data, and (c) the procedure that will be followed. All of these elements will be reported in detail in Chapter 3. In a quantitative study, the instrumentation will be validated in Chapter 3 in detail. In a qualitative study, if it is a researcher-created questionnaire, validating the correctness of the interview protocol is usually accomplished with a pilot study. For either a quantitative or a qualitative study, using an already validated survey instrument is easier to defend and does not require a pilot study; however, Chapter 3 must contain a careful review of the instrument and how it was validated by the creator.
% In a qualitative study, which usually involves interviews, the instrumentation is an interview protocol – a pre-determined set of questions that every participant is asked that are based on the primary research questions. A qualitative interview should contain no less than 10 open-ended questions and take no less than 1 hour to administer to qualify as “robust” research.
% In the humanities, a demographic survey should be circulated with most quantitative and qualitative studies to establish the parameters of the participant pool. Demographic surveys are nearly identical in most dissertations. In the sciences, a demographic survey is rarely needed.
Memory-safety is a term that is only vaguely defined in general, thus a definition is given for the context of this thesis.
For a thorough understanding of the issues discussed further in this document, it might be helpful to review the basics of how memory is used in current computer systems.
For decades computer systems or more specifically their \glspl{CPU} were designed to execute instructions that were previously loaded into volatile main memory, typically from a secondary, persistent memory.
These instructions are themselves able to alter the very main memory they are stored at, which allows for great flexibility but also involves the risk of corrupting a consistent chain of instructions or other memory content like data.
As any other \gls{app}, the \gls{OS} is executed in form of a set of logically grouped instructions, called a program.
Loading the \gls{OS}'s program into memory is not the responsibility of the \gls{OS}, it belongs to the components earlier in the boot process, namely the boot loader and system firmware.
The \gls{OS} takes over the responsibility to protect the main and secondary memory from the point where it is being handed control over by the bootloader.
Loading further programs into main memory is done by the \gls{OS}, either according to scheduled jobs set up by the \gls{sysadmin}, or based on well-defined events which can be triggered by any form of input via the system's interfaces.
For example, the \gls{OS} can load and execute a program stored on the hard-disk, after the user has gave the appropriate instructions via a terminal.
The execution of other programs is potentially dangerous, because the program might the memory content of other programs and their data.
It is the responsibility of the \gls{OS} to prevent programs from being able to interfere with each other under any circumstances, keeping the memory content in a consistent state at all times.
This requires an extensive amount of care and foresight from the developers of the \gls{OS}, to ensure memory consistency in any of the various events and combinations thereof that might possibly occur at runtime.
\subsection{A Definition Of Memory-Safety}
\label{context::introduction::memory-safety::def}
If the \gls{OS} is memory-safe, any program, whether it is part of the \gls{OS} or any other \gls{app}, memory access is restricted to memory regions that have been allocated for this specific program, preventing it from reading and writing to memory regions of other programs.
\subsection{The Human Aspect}
\label{context::introduction::memory-safety::human-aspect}
Programs are written by humans which is an important aspect against memory-safety.
No human is born as a flawless software engineer.
Beginners will start writing programs before he or she masters this skill in perfection.
Also, with each generation of humans there will always be new beginners that will start learning from scratch.
This requires a sustainable method to prevent mistakes, especially such that have an impact on memory-safety.
Advanced programmers can profit too, as they also make mistakes on a regular basis, depending on their level of focus which can vary momentarily.
\subsection{Detecting Memory-Safety Violations - Before They Occur}
\label{context::introduction::memory-safety::detection}
The human aspect suggests that systems needs to be designed to be testable at first, and then tested thoroughly in order to mitigate the risks of erroneous software being executed by the end-user.
Besides the presence and quality of tests, their point in the software life cycle plays an important role.
The earliest tests can be as soon as the process of software development itself, and the latest ones can be at the time of execution on the production system of the end-user.
It is desirable to place tests as early as possible in the software life cycle, to prevent them from compromising running systems that hold sensitive data and offer important services.
The dimension of time can also be translated to hierarchically lower system components at run-time.
This suggests that the \gls{OS} must be tested before the other executed \glspl{app}, etc.
This can be easily explained.
From a \gls{app} perspective, testing every permutation of \gls{OS} runtime states can be impossible, because the \gls{app} can not freely mutate the system's state.
Even if it could, testing all possible permutations of system state is limited by time and resource restrictions.
That's why even disciplined software engineers write tests that only target common error cases, like system memory exhaustion, and ensure syntactic and semantic correctness for the \gls{app} being developed.
Edge cases that happen only under specific system circumstances, possibly influenced by other components on the system as described in the beginning of \autoref{context::introduction::memory-safety}, are at high risk of remaining untested, and the \gls{app} developer is forced to trust the underlying \gls{OS}.
This puts high importance on the safety of the \gls{OS} design and implementation.
\subsection{Abstraction: Safety vs. Functionality}
\label{context::introduction::memory-safety::abstr-safety-function}
In computer systems, safety and functionality are counter-proportional towards each other, because with increased functionality also grows complexity, and error cases become more difficult to find.
Applying this analogy to software development, during which the errors are created in the first place, might be misleading.
It might seem that the more abstraction is provided by a language, the higher the functionality is.
In fact, the opposite is the case.
Abstraction can be used to impose limits on what the programmer can instruct the system to do.
By defining an abstraction layer in form of a programming language, the language defines which of the underlying functionality will be exposed through it.
In addition, the language can introduce obligated rules that make the written program easier to analyze in an automated fashion, before it gets compiled into the underlying representation.
\section{Safety In Language Compilers And Static Analyzers}
\label{context::introduction::language-compilers-analyzers}
% The theoretical framework is the foundational theory that is used to provide a perspective upon which the study is based. There are hundreds of theories in the literature. For instance, if a study in the social sciences is about stress that may be causing teachers to quit, Apple’s Intensification Theory could be cited as the theory was that stress is cumulative and the result of continuing overlapping, progressively stringent responsibilities for teachers that eventually leads to the desire to quit. In the sciences, research about new species that may have evolved from older, extinct species would be based on the theory of evolution pioneered by Darwin.
% Some departments put the theoretical framework explanation in Chapter 1; some put it in Chapter 2.
In \autoref{context::introduction::memory-safety}, specifically in \autoref{context::introduction::memory-safety::detection}, it was explained that programming languages have direct impact on the memory-safety.
This section gives an example of how severe this impact is and explains the requirements on a \gls{OS} language.
\subsection{\gls{Linux} and \gls{C}: Zero Memory-Safety A Day}
% Significance of the Study
% The significance is a statement of why it is important to determine the answer to the gap in the knowledge, and is related to improving the human condition. The contribution to the body of knowledge is described, and summarizes who will be able to use the knowledge to make better decisions, improve policy, advance science, or other uses of the new information. The “new” data is the information used to fill the gap in the knowledge.
A very popular and widespread \gls{OS} is \gls{Linux} which is written in \gls{C} and some hardware specific \gls{asm} code.
Recent years have shown how prone it is to vulnerabilities that result from programming errors related to memory management.
A very recent and high impact vulnerability is known as CVE-2017-1000364\footnote{http://www.cvedetails.com/cve/CVE-2017-1000364/}, where \textit{"an issue was discovered in the size of the stack guard page on Linux, specifically a 4k stack guard page is not sufficiently large and can be "jumped" over (the stack guard page is bypassed)"}.
With the growing number of vulnerabilities, various solutions have been proposed to increase the safety of C, either with static code analysis or via generated checks imposed at runtime. (TODO: reference).
Static analysis are not very effective on a language that has not been designed to be safety-analyzed. TODO? reference?
For this reason there have been attempts to define subsets of the \gls{C} language that can be safety checked, TODO: refernces of Cyclone, CCured, etc..
Safety checks that are performed at runtime introduce a high degree of overhead, which makes it an nonviable option in the domain of \gls{OS} development, where many code paths must be very fast to ensure the operation of high speed I/O devices\cite{Balasubramanian2017} or tasks with \gls{realtime} requirements. (TODO: explain realtime requirements)
This has been forcing \gls{OS} developers to prioritize performance over safety. (TODO: reference)
Details about the challenge of writing code that does memory management safely, and related vulnerabilities are given further along in \autoref{chap:mmt}.
\subsection{\gls{OS} Language Choices}
Criteria for the choice of language are much different from choosing a language for other types of \glspl{app}.
This is a list of what is required for implementing an \glspl{OS}
\begin{itemize}
\item{Raw access to \gls{CPU} instructions}
\item{Deterministic temporal behavior}
\end{itemize}
* TODO: put in some scientific background about static checks
* affine types
In this context, memory safety is the ability to prevent an alteration of the memory content that would otherwise lead to malfunctioning at best, and malicious behavior at worst.
\section{Academic And Industrial Activities}
% Primary Research Questions
% The primary research question is the basis for data collection and arises from the Purpose of the Study. There may be one, or there may be several. When the research is finished, the contribution to the knowledge will be the answer to these questions. Do not confuse the primary research questions with interview questions in a qualitative study, or survey questions in a quantitative study. The research questions in a qualitative study are followed by both a null and an alternate hypothesis.
% Hypotheses
% A hypothesis is a testable prediction for an observed phenomenon, namely, the gap in the knowledge. Each research question will have both a null and an alternative hypothesis in a quantitative study. Qualitative studies do not have hypotheses. The two hypotheses should follow the research question upon which they are based. Hypotheses are testable predictions to the gap in the knowledge. In a qualitative study the hypotheses are replaced with the primary research questions.
* TODO: mention redox, tockos, intermezzOS and more activities
* TODO: mention paper's by tockos team
* TODO: mention electrolyte, formal verification for Rust
@ -30,40 +118,14 @@ This is to my surprise, because as explained in more details in this chapter the
\gls{OS} is critical and \gls{Rust} offers attractive features to help improve this situation.
However, the hypothesis cannot be trivially approved or denied, which drives the research efforts for my final thesis project.
Besides this specific hypothesis, many implementations of \glspl{OS} with \gls{Rust} have appeared in public.
These range from proof-of-concept and educational work like \gls{imezzos} and \gls{blogos}, to implementations that aim to be production grade software like \gls{redoxos} and \gls{tockos}.
% Purpose of the Study
%The Purpose of the Study is a statement contained within one or two paragraphs that identifies the research design, such as qualitative, quantitative, mixed methods, ethnographic, or another design. The research variables, if a quantitative study, are identified, for instance, independent, dependent, comparisons, relationships, or other variables. The population that will be used is identified, whether it will be randomly or purposively chosen, and the location of the study is summarized. Most of these factors will be discussed in detail in Chapter 3.
The results will be of qualitative nature, captured by analyzing existing and a self-developed \gls{Rust}-implementations of popular memory management techniques.
In addition to the sole analysis of \gls{Rust}-implementations, comparisons will be made, discerning the level of memory safety guarantees gained over similarly intending implementations in \gls{C}.
\section{Status Quo: Zero Memory-Safety A Day}
% Significance of the Study
% The significance is a statement of why it is important to determine the answer to the gap in the knowledge, and is related to improving the human condition. The contribution to the body of knowledge is described, and summarizes who will be able to use the knowledge to make better decisions, improve policy, advance science, or other uses of the new information. The “new” data is the information used to fill the gap in the knowledge.
A very popular and widespread is \gls{OS}, which has been developed with \gls{C} (and some assembly).
Recent years have shown how prone it is to vulnerabilities that result from the unsafe language design and programming errors.
With the growing number of vulnerabilities, various solutions have been proposed to increase the safety of C, either with static code analysis or via checks imposed at runtime. (TODO: reference).
The former is complex to perform on a language that has not been designed to be safety-analysed. TODO? reference?
Despite its complexity, attempts exist to define a subset of the \gls{C} language that can be safety checked, TODO: refernces of Cyclone, CCured, etc..
Safety checks that are performed at runtime introduce a high degree of overhead, which makes it an unviable option in the domain of \gls{OS} development, where many code paths must be very fast to ensure the operation of high speed I/O devices\cite{Balasubramanian2017} or other tasks with hard- or soft-realtime requirements.. (TODO: explain realtime requirements)
This has been forcing \gls{OS} developers to prioritize performance over safety. (TODO: reference)
Details about the challenge of writing code that does memory management safely, and related vulnerabilities are given further along in \autoref{chap:mmt}.
\section{Assessing Memory-Safety}
% In Chapter 1 this is a summary of the methodology and contains a brief outline of three things: (a) the participants in a qualitative study or the subjects of a quantitative study (human participants are referred tyo as participants, non-human subjects are referred to as subjects), (b) the instrumentation used to collect data, and (c) the procedure that will be followed. All of these elements will be reported in detail in Chapter 3. In a quantitative study, the instrumentation will be validated in Chapter 3 in detail. In a qualitative study, if it is a researcher-created questionnaire, validating the correctness of the interview protocol is usually accomplished with a pilot study. For either a quantitative or a qualitative study, using an already validated survey instrument is easier to defend and does not require a pilot study; however, Chapter 3 must contain a careful review of the instrument and how it was validated by the creator.
% In a qualitative study, which usually involves interviews, the instrumentation is an interview protocol – a pre-determined set of questions that every participant is asked that are based on the primary research questions. A qualitative interview should contain no less than 10 open-ended questions and take no less than 1 hour to administer to qualify as “robust” research.
% In the humanities, a demographic survey should be circulated with most quantitative and qualitative studies to establish the parameters of the participant pool. Demographic surveys are nearly identical in most dissertations. In the sciences, a demographic survey is rarely needed.
* TODO: what is memory?
* TODO: when it is considered safe?
* TODO: Explain how memory-safety can be measured
\section{Compilers And Static Code Analysis}
% The theoretical framework is the foundational theory that is used to provide a perspective upon which the study is based. There are hundreds of theories in the literature. For instance, if a study in the social sciences is about stress that may be causing teachers to quit, Apple’s Intensification Theory could be cited as the theory was that stress is cumulative and the result of continuing overlapping, progressively stringent responsibilities for teachers that eventually leads to the desire to quit. In the sciences, research about new species that may have evolved from older, extinct species would be based on the theory of evolution pioneered by Darwin.
% Some departments put the theoretical framework explanation in Chapter 1; some put it in Chapter 2.
* TODO: put in some scientific background about static checks
* affine types
\section{Assumptions, Limitations, and Scope (Delimitations)}
% Assumptions are self-evident truths. In a qualitative study, it may be assumed that participants be highly qualified in the study is about administrators. It can be assumed that participants will answer truthfully and accurately to the interview questions based on their personal experience, and that participants will respond honestly and to the best of their individual abilities.
% Limitations of a study are those things over which the research has no control. Evident limitations are potential weaknesses of a study. Researcher biases and perceptual misrepresentations are potential limitations in a qualitative study; in a quantitative study, a limitation may be the capability of an instrument to accurately record data.
@ -84,9 +146,9 @@ The \autoref{chap:mmt} gives a detailed introduction to memory management in con
* TODO: in the beginnings application software had full control over memory
* TODO: from single-job via batch systems to multiprocessing
As the result of collaborations between hard- and software developers, the memory management task in the \gls{OS} is partially delegated to the \gls{CPU}'s \gls{MMU}.
A complete understand of this task is necessary in order to reason about it's safety.
This chapter starts with the provides a thorough introduction to modern memory management techniques on the x86\_64 architecture.
As the result of collaborations between hard- and software developers, the memory management task in the \gls{OS} can be partially delegated to the \gls{CPU}'s \gls{MMU}.
A complete understanding of this task is necessary in order to reason about it's safety.
This chapter provides an introduction to hardware-supported memory-management and protection techniques for the x86\_64 architecture.
\section{Resource Abstraction: Protection And Efficiency}
* TODO: recap that management has been motivated by multiprocessing without side-effects

25
src/docs/thesis.bib
View file

@ -3,14 +3,14 @@ Any changes to this file will be lost if it is regenerated by Mendeley.
BibTeX export options can be customized via Options -> BibTeX in Mendeley Desktop
@book{AMD64Vol1,
author = {AMD},
file = {:home/steveej/src/github/steveej/msc-thesis/docs/AMD64 Architecture Programmer's Manual Volume 1$\backslash$: Application Programming.pdf:pdf},
keywords = {AMD64,SIMD,extended media instructions,legacy m},
number = {26568},
title = {{AMD64 Architecture Programmer's Manual Volume 1: Application Programming}},
volume = {4},
year = {2012}
@article{Reed2015,
abstract = {Rust is a new systems language that uses some advanced type system features, specifically affine types and regions, to statically guarantee memory safety and eliminate the need for a garbage collector. While each individual addition to the type system is well understood in isolation and are known to be sound, the combined system is not known to be sound. Furthermore, Rust uses a novel checking scheme for its regions, known as the Borrow Checker, that is not known to be correct. Since Rust's goal is to be a safer alternative to C/C++, we should ensure that this safety scheme actually works. We present a formal semantics that captures the key features relevant to memory safety, unique pointers and borrowed references, specifies how they guarantee memory safety, and describes the operation of the Borrow Checker. We use this model to prove the soudness of some core operations and justify the conjecture that the model, as a whole, is sound. Additionally, our model provides a syntactic version of the Borrow Checker, which may be more understandable than the non-syntactic version in Rust.},
author = {Reed, Eric},
file = {:home/steveej/src/github/steveej/msc-thesis/docs/Patina$\backslash$: A Formalization of the Rust Programming Language.pdf:pdf},
number = {February},
pages = {1--37},
title = {{Patina: A Formalization of the Rust Programming Language}},
year = {2015}
}
@article{Dhurjati2003,
abstract = {Traditional approaches to enforcing memory safety of programs rely heavily on runtime checks of memory accesses and on garbage collection, both of which are unattractive for embedded applications. The long-term goal of our work is to enable 100{\%} static enforcement of memory safety for embedded programs through advanced compiler techniques and minimal semantic restrictions on programs. The key result of this paper is a compiler technique that ensures memory safety of dynamically allocated memory without programmer annotations, runtime checks, or garbage collection, and works for a large subclass of type-safe C programs. The technique is based on a fully automatic pool allocation (i.e., region-inference) algorithm for C programs we developed previously, and it ensures safety of dynamically allocated memory while retaining explicit deallocation of individual objects within regions (to avoid garbage collection). For a diverse set of embedded C programs (and using a previous technique to avoid null pointer checks), we show that we are able to statically ensure the safety of pointer and dynamic memory usage in all these programs. We also describe some improvements over our previous work in static checking of array accesses. Overall, we achieve 100{\%} static enforcement of memory safety without new language syntax for a significant subclass of embedded C programs, and the subclass is much broader if array bounds checks are ignored.},
@ -145,6 +145,15 @@ pages = {52--57},
title = {{A dynamic detection method to C/C++ programs memory vulnerabilities based on pointer analysis}},
year = {2013}
}
@book{AMD64Vol1,
author = {AMD},
file = {:home/steveej/src/github/steveej/msc-thesis/docs/AMD64 Architecture Programmer's Manual Volume 1$\backslash$: Application Programming.pdf:pdf},
keywords = {AMD64,SIMD,extended media instructions,legacy m},
number = {26568},
title = {{AMD64 Architecture Programmer's Manual Volume 1: Application Programming}},
volume = {4},
year = {2012}
}
@article{Getreu2016,
author = {Getreu, Jens},
file = {:home/steveej/src/github/steveej/msc-thesis/docs/Embedded System Security with Rust - Case Study of Heartbleed.pdf:pdf},

6
src/docs/thesis.tex
View file

@ -24,7 +24,7 @@
\usepackage{listings}
\newcommand{\topic}{Guaranteed In-Kernel Memory-Safety Using Rust's Static Code Analysis}
\newcommand{\topic}{Guarantees On In-Kernel Memory-Safety Using Rust's Static Code Analysis}
\newcommand{\authorOne}{Stefan Junker}
\newcommand{\authorOneInit}{SJ}
@ -38,7 +38,7 @@
\newcommand{\studies}{Master Information Technology - Embedded And Mobile Systems}
\newcommand{\startdate}{2017/4/1}
\newcommand{\submitdate}{2017/8/31}
\newcommand{\buzzwords}{TODO buzzwords}
\newcommand{\buzzwords}{memory-safety, operating system, rust}
% Numbered Subsubsections
\setcounter{secnumdepth}{3}
@ -125,7 +125,7 @@
\chapter*{Preface}
This thesis is original, unpublished, independent work by the author, \authorOne.
I strongly believe in openness and collaboration in the development of new technology, therefore the development will be based solely on Open-Source software.
The results of this project will be freely available on my personal Gitlab site\footnote{https://gitlab.com/steveeJ/msc-thesis} once the academic process of this project is complete.
The source of this document and the code I have worked on will be freely available on my personal Gitlab site\footnote{https://gitlab.com/steveeJ/msc-thesis} once the academic process of this project is complete.
\tableofcontents