From 9a18b40dadc10c86e77a63db1a4735260073c184 Mon Sep 17 00:00:00 2001 From: Stefan Junker Date: Wed, 5 Apr 2017 16:39:52 +0200 Subject: [PATCH 1/7] thesis: topic refinement --- src/docs/thesis.tex | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/docs/thesis.tex b/src/docs/thesis.tex index 6fdaf4c..01a169d 100644 --- a/src/docs/thesis.tex +++ b/src/docs/thesis.tex @@ -20,7 +20,7 @@ \usepackage[numberedsection,toc,numberline,nopostdot]{glossaries} \makenoidxglossaries -\newcommand{\topic}{Leveraging Static Code Analysis To Improve The Memory Safety For Kernel Tasks} +\newcommand{\topic}{Ensuring Memory-Safety within Address Spaces Using Rust's Static Code Analysis} \newcommand{\authorOne}{Stefan Junker} \newcommand{\authorOneInit}{SJ} From 15629798225a73b1949a6c533ff7e0d3d004c3e2 Mon Sep 17 00:00:00 2001 From: Stefan Junker Date: Wed, 5 Apr 2017 18:51:19 +0200 Subject: [PATCH 2/7] refine topic --- src/docs/thesis.tex | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/docs/thesis.tex b/src/docs/thesis.tex index 01a169d..33efc9f 100644 --- a/src/docs/thesis.tex +++ b/src/docs/thesis.tex @@ -12,7 +12,7 @@ \usepackage{ctable,multirow} \usepackage{cite} -\bibliographystyle{plain} +\bibliographystyle{ieeetr} \usepackage[hyphens]{url} \Urlmuskip = 0mu plus 1mu @@ -20,7 +20,7 @@ \usepackage[numberedsection,toc,numberline,nopostdot]{glossaries} \makenoidxglossaries -\newcommand{\topic}{Ensuring Memory-Safety within Address Spaces Using Rust's Static Code Analysis} +\newcommand{\topic}{Guaranteeing In-Kernel Memory-Safety Using Rust's Static Code Analysis} \newcommand{\authorOne}{Stefan Junker} \newcommand{\authorOneInit}{SJ} From ec720b119000b8ef4f4a9f8d4c1e41686662546e Mon Sep 17 00:00:00 2001 From: Stefan Junker Date: Wed, 5 Apr 2017 18:51:02 +0200 Subject: [PATCH 3/7] context: working on intro --- src/docs/glossary.tex | 21 +++++++++++++++++++++ src/docs/parts/context/context.tex | 13 ++++++++++--- 2 files changed, 31 insertions(+), 3 deletions(-) diff --git a/src/docs/glossary.tex b/src/docs/glossary.tex index e0d379c..131d44a 100644 --- a/src/docs/glossary.tex +++ b/src/docs/glossary.tex @@ -1,5 +1,26 @@ % // vim: set ft=tex: +\newglossaryentry{rustlang}{ + name = Rust, + description = { + The Rust Programming Language. + }, +} + +\newglossaryentry{compiler}{ + name = compiler, + description = { + A program that can transform software source code to executable machine code. + }, +} + +\newglossaryentry{addrspace}{ + name = memory address space, + description = { + A logical entity that represents parts of the virtual memory, specified with a starting address and the length in a standardize unit + }, +} + \newglossaryentry{API}{ name = API, description = { diff --git a/src/docs/parts/context/context.tex b/src/docs/parts/context/context.tex index 5475720..c194baa 100644 --- a/src/docs/parts/context/context.tex +++ b/src/docs/parts/context/context.tex @@ -1,15 +1,22 @@ % // vim: set ft=tex: \chapter{Introduction} +This thesis studies the feasibility of using static code analysis, as found in the \gls{rustlang}'s \gls{compiler}, to ensure memory safety within an \gls{OS} kernel. -\section{Purpose of the Study} % 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 purpose of this study is to evaluate Rust's feasibility to guarantee memory safety when it's used for \gls{OS} development. + +% Scope +In the general sense an \gls{OS} is a \gls{app} that runs within one \gls{addrspace} and is able to run on the hardware platform without any abstraction. +This study could be applied to all \glspl{app}, but the focus is on the implementation of \glspl{OS}. +The main reason for this is that the due to its nature, the \gls{OS} is the only \gls{app} that has unrestricted access to the system's hardware, which makes it the most important \gls{app} to maintain secure. -\section{Significance of the Study} % 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. +The current de-facto standard language for \gls{OS} development appears to be the C, a very popular \gls{OS} example is \gls{Linux}. +Recent years have shown how prone it is to security vulnerabilities, which is covered by exemplary details within this study. (TODO reference) + -\section{Primary Research Questions} % 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. From fa009e54276e31f9b537ca502c2da45932624a32 Mon Sep 17 00:00:00 2001 From: Stefan Junker Date: Thu, 6 Apr 2017 16:41:01 +0200 Subject: [PATCH 4/7] bib: intermittent removal --- src/docs/thesis.bib | 39 ++++++++++++++++++++++++++++++++++++++- 1 file changed, 38 insertions(+), 1 deletion(-) mode change 120000 => 100644 src/docs/thesis.bib diff --git a/src/docs/thesis.bib b/src/docs/thesis.bib deleted file mode 120000 index 9a0ca81..0000000 --- a/src/docs/thesis.bib +++ /dev/null @@ -1 +0,0 @@ -/home/steveej/src/mendeley/Static-Code-Analysis-Kernel-Memory-Saftey.bib \ No newline at end of file diff --git a/src/docs/thesis.bib b/src/docs/thesis.bib new file mode 100644 index 0000000..3d952b5 --- /dev/null +++ b/src/docs/thesis.bib @@ -0,0 +1,38 @@ +Automatically generated by Mendeley Desktop 1.17.8 +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 + +@misc{Endler, +author = {Endler, Matthias}, +title = {{A curated list of static analysis tools, linters and code quality checkers for various programming languages}}, +url = {https://github.com/mre/awesome-static-analysis} +} +@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.}, +author = {Dhurjati, D and Kowshik, S and Adve, V and Lattner, C}, +doi = {10.1145/780742.780743}, +file = {:home/steveej/src/github/steveej/msc-thesis/docs/Memory Safety Without Runtime Checks or Garbage.pdf:pdf}, +isbn = {0362-1340}, +issn = {03621340}, +journal = {Acm Sigplan Notices}, +keywords = {automatic pool allocation,compilers,embedded systems,languages,programming languages,region management,security,static analysis}, +number = {7}, +pages = {69--80}, +title = {{Memory safety without runtime checks or garbage collection}}, +volume = {38}, +year = {2003} +} +@article{Levy2015a, +abstract = {Rust, a new systems programming language, provides compile-time memory safety checks to help eliminate runtime bugs that manifest from improper memory management. This feature is advantageous for operating system development, and especially for embedded OS development, where recovery and debugging are particularly challenging. However, embedded platforms are highly event-based, and Rust's memory safety mechanisms largely presume threads. In our experience developing an operating system for embedded systems in Rust, we have found that Rust's ownership model prevents otherwise safe resource sharing common in the embedded domain, conflicts with the reality of hardware resources, and hinders using closures for programming asynchronously. We describe these experiences and how they relate to memory safety as well as illustrate our workarounds that preserve the safety guarantees to the largest extent possible. In addition, we draw from our experience to propose a new language extension to Rust that would enable it to provide better memory safety tools for event-driven platforms.}, +author = {Levy, Amit and Andersen, Michael P. and Campbell, Bradford and Culler, David and Dutta, Prabal and Ghena, Branden and Levis, Philip and Pannuto, Pat}, +doi = {10.1145/2818302.2818306}, +file = {:home/steveej/src/github/steveej/msc-thesis/docs/tock-plos2015.pdf:pdf}, +isbn = {9781450339421}, +journal = {PLOS: Workshop on Programming Languages and Operating Systems}, +keywords = {embedded operating systems,linear types,ownership,rust}, +pages = {21--26}, +title = {{Ownership is Theft: Experiences Building an Embedded OS in Rust}}, +url = {http://dl.acm.org/citation.cfm?id=2818302.2818306}, +year = {2015} +} From a15d58dd73199467a6dfa8c700fc78de98e50942 Mon Sep 17 00:00:00 2001 From: Stefan Junker Date: Thu, 6 Apr 2017 16:44:13 +0200 Subject: [PATCH 5/7] bib: add back with content From 927c80710358e37cfd66b57878ecd94a64925fec Mon Sep 17 00:00:00 2001 From: Stefan Junker Date: Thu, 6 Apr 2017 16:47:25 +0200 Subject: [PATCH 6/7] context: fix typos --- src/docs/parts/context/context.tex | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/docs/parts/context/context.tex b/src/docs/parts/context/context.tex index c194baa..a4b1be0 100644 --- a/src/docs/parts/context/context.tex +++ b/src/docs/parts/context/context.tex @@ -1,6 +1,6 @@ % // vim: set ft=tex: \chapter{Introduction} -This thesis studies the feasibility of using static code analysis, as found in the \gls{rustlang}'s \gls{compiler}, to ensure memory safety within an \gls{OS} kernel. +This thesis studies the feasibility of using static code analysis, as found in the \gls{rustlang} \gls{compiler}, to ensure memory safety within an \gls{OS} kernel. % 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. @@ -15,7 +15,6 @@ The main reason for this is that the due to its nature, the \gls{OS} is the only % 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. The current de-facto standard language for \gls{OS} development appears to be the C, a very popular \gls{OS} example is \gls{Linux}. Recent years have shown how prone it is to security vulnerabilities, which is covered by exemplary details within this study. (TODO reference) - % 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. From 091c720cb853401970899e231536ced701ef60d2 Mon Sep 17 00:00:00 2001 From: Stefan Junker Date: Thu, 6 Apr 2017 17:08:46 +0200 Subject: [PATCH 7/7] shell/vim: copy bib file from mendeley on save --- shell.nix | 2 ++ 1 file changed, 2 insertions(+) diff --git a/shell.nix b/shell.nix index afe99db..2d262af 100644 --- a/shell.nix +++ b/shell.nix @@ -130,6 +130,8 @@ in pkgs.stdenv.mkDerivation { endfunction 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' ''; vam.knownPlugins = pkgs.vimPlugins;