Changeset 16915b1 for doc/theses/mike_brooks_MMath

Timestamp:

Aug 11, 2024, 10:52:44 AM (3 months ago)

Author:

Peter A. Buhr <pabuhr@…>

Branches:

master

Children:

f22d100

Parents:

5ca5263

Message:

proofread intro chapter and add citation

Location:

doc/theses/mike_brooks_MMath

Files:

• intro.tex (modified) (3 diffs)
• string.tex (modified) (1 diff)
• uw-ethesis.bib (modified) (1 diff)

doc/theses/mike_brooks_MMath/intro.tex

@@ -1 +1 @@
 \chapter{Introduction}
 
-All modern programming languages provide three high-level containers (collection): array, linked-list, and string.
-Often array is part of the programming language, while linked-list is built from pointer types, and string from a combination of array and linked-list.
-For all three types, there is some corresponding mechanism for iterating through the structure, where the iterator flexibility varies with the kind of structure and ingenuity of the iterator implementor.
+All modern programming languages provide three high-level containers (collections): array, linked-list, and string.
+Often array is part of the programming language, while linked-list is built from (recursive) pointer types, and string from a combination of array and linked-list.
+For all three types, languages supply varying degrees of high-level mechanism for manipulating these objects at the bulk level and at the component level, such as array copy, slicing and iterating.
+
+This work looks at extending these three foundational container types in the programming language \CFA, which is a new dialect of the C programming language.
+A primary goal of \CFA~\cite{Cforall} is 99\% backward compatibility with C, while maintaining a look and feel that matches with C programmer experience and intuition.
+This goal requires ``thinking inside the box'' to engineer new features that ``work and play'' with C and its massive legacy code-base.
+An additional goal is balancing good performance with safety.
 
 
 \section{Array}
 
-An array provides a homogeneous container with $O(1)$ access to elements using subscripting (some form of pointer arithmetic).
+An array provides a homogeneous container with $O(1)$ access to elements using subscripting.
 The array size can be static, dynamic but fixed after creation, or dynamic and variable after creation.
 For static and dynamic-fixed, an array can be stack allocated, while dynamic-variable requires the heap.
-Because array layout has contiguous components, subscripting is a computation.
-However, the computation can exceed the array bounds resulting in programming errors and security violations~\cite{Elliott18, Blache19, Ruef19, Oorschot23}.
-The goal is to provide good performance with safety.
+Because array layout has contiguous components, subscripting is a computation (some form of pointer arithmetic).
 
 
 \section{Linked list}
 
-A linked-list provides a homogeneous container often with $O(log N)$/$O(N)$ access to elements using successor and predecessor operations.
+A linked-list provides a homogeneous container often with $O(log N)$/$O(N)$ access to elements using successor and predecessor operations that normally involve pointer chasing.
 Subscripting by value is sometimes available, \eg hash table.
 Linked types are normally dynamically sized by adding/removing nodes using link fields internal or external to the elements (nodes).
 If a programming language allows pointer to stack storage, linked-list types can be allocated on the stack;
-otherwise, elements are heap allocated and explicitly/implicitly managed.
+otherwise, elements are heap allocated with explicitly/implicitly managed.
 
 
@@ -28 +31 @@
 
 A string provides a dynamic array of homogeneous elements, where the elements are often human-readable characters.
-What differentiates a string from other types in that its operations work on blocks of elements for scanning and changing the elements, rather than accessing individual elements, \eg @index@ and @substr@.
+What differentiates a string from other types in that its operations work on blocks of elements for scanning and changing, \eg @index@ and @substr@.
 Subscripting individual elements is often available.
-Often the cost of string operations is less important than the power of the operations to accomplish complex text manipulation, \eg search, analysing, composing, and decomposing.
+Therefore, the cost of string operations is less important than the power of the operations to accomplish complex text manipulation, \eg search, analysing, composing, and decomposing.
 The dynamic nature of a string means storage is normally heap allocated but often implicitly managed, even in unmanaged languages.
+Often string management is separate from heap management, \ie strings roll their own heap.
 
 
 \section{Motivation}
 
-The goal of this work is to introduce safe and complex versions of array, link lists, and strings into the programming language \CFA~\cite{Cforall}, which is based on C.
-Unfortunately, to make C better, while retaining a high level of backwards compatibility, requires a significant knowledge of C's design.
-Hence, it is assumed the reader has a medium knowledge of C or \CC, on which extensive new C knowledge is built.
+The primary motivation for this work is two fold:
+\begin{enumerate}[leftmargin=*]
+\item
+These three aspects of C are extremely difficult to understand, teach, and get right because they are correspondingly extremely low level.
+Providing higher-level versions of these containers in \CFA is a major component of the primary goal.
+\item
+These three aspects of C cause the greatest safety issues because there are few or no safe guards when a programmer misunderstands or misuses these features~\cite{Elliott18, Blache19, Ruef19, Oorschot23}.
+Estimates suggest 50\%~\cite{Mendio24} of total reported open-source vulnerabilities occur in C resulting from errors using these facilities (memory errors), providing the major hacker attack-vectors.
+\end{enumerate}
+Both White House~\cite{WhiteHouse24} and DARPA~\cite{DARPA24} recently released a recommendation to move away from C and \CC, because of cybersecurity threats exploiting vulnerabilities in these older languages.
+Hardening these three types goes a long way to make the majority of C programs safer.
+
+
+While multiple new languages purport to be systems languages replacing C, the reality is that rewriting massive C code-bases is impractical and a non-starter if the new runtime uses garage collection.
+Furthermore, these languages must still interact with the underlying C operating system through fragile, type-unsafe, interlanguage-communication.
+Switching to \CC is equally impractical as its complex and interdependent type-system (\eg objects, inheritance, templates) means idiomatic \CC code is difficult to use from C, and C programmers must expend significant effort learning \CC.
+Hence, rewriting and retraining costs for these languages can be prohibitive for companies with a large C software-base (Google, Apple, Microsoft, Amazon, AMD, Nvidia).
 
 
@@ -46 +64 @@
 However, most programming languages are only partially explained by standard's manuals.
 When it comes to explaining how C works, the definitive source is the @gcc@ compiler, which is mimicked by other C compilers, such as Clang~\cite{clang}.
-Often other C compilers must mimic @gcc@ because a large part of the C library (runtime) system contains @gcc@ features.
-While some key aspects of C need to be explained by quoting from the language reference manual, to illustrate definite program semantics, I devise a program, whose behaviour exercises the point at issue, and shows its behaviour.
+Often other C compilers must mimic @gcc@ because a large part of the C library (runtime) system (@glibc@ on Linux) contains @gcc@ features.
+While some key aspects of C need to be explained by quoting from the language reference manual, to illustrate definite program semantics, my approach in this thesis is to devise a program, whose behaviour exercises a point at issue, and shows its behaviour.
 These example programs show
-\begin{itemize}
-        \item the compiler accepts or rejects certain syntax,
+\begin{itemize}[leftmargin=*]
+        \item if the compiler accepts or rejects certain syntax,
         \item prints output to buttress a claim of behaviour,
-        \item executes without triggering any embedded assertions testing pre/post-assertions or invariants.
+        \item or executes without triggering any embedded assertions testing pre/post-assertions or invariants.
 \end{itemize}
 This work has been tested across @gcc@ versions 8--12 and clang version 10 running on ARM, AMD, and Intel architectures.
 Any discovered anomalies among compilers or versions is discussed.
-In all case, I do not argue that my sample of major Linux compilers is doing the right thing with respect to the C standard.
-
-
-\subsection{Ill-typed expressions}
-
-C reports many ill-typed expressions as warnings.
-For example, these attempts to assign @y@ to @x@ and vice-versa are obviously ill-typed.
-\lstinput{12-15}{bkgd-c-tyerr.c}
-with warnings:
-\begin{cfa}
-warning: assignment to 'float *' from incompatible pointer type 'void (*)(void)'
-warning: assignment to 'void (*)(void)' from incompatible pointer type 'float *'
-\end{cfa}
-Similarly,
-\lstinput{17-19}{bkgd-c-tyerr.c}
-with warning:
-\begin{cfa}
-warning: passing argument 1 of 'f' from incompatible pointer type
-note: expected 'void (*)(void)' but argument is of type 'float *'
-\end{cfa}
-with a segmentation fault at runtime.
-Clearly, @gcc@ understands these ill-typed case, and yet allows the program to compile, which seems inappropriate.
-Compiling with flag @-Werror@, which turns warnings into errors, is often too strong, because some warnings are just warnings, \eg unsed variable.
-In the following discussion, ``ill-typed'' means giving a nonzero @gcc@ exit condition with a message that discusses typing.
-Note, \CFA's type-system rejects all these ill-typed cases as type mismatch errors.
-
-% That @f@'s attempt to call @g@ fails is not due to 3.14 being a particularly unlucky choice of value to put in the variable @pi@.
-% Rather, it is because obtaining a program that includes this essential fragment, yet exhibits a behaviour other than "doomed to crash," is a matter for an obfuscated coding competition.
-
-% A "tractable syntactic method for proving the absence of certain program behaviours by classifying phrases according to the kinds of values they compute"*1 rejected the program.
-% The behaviour (whose absence is unprovable) is neither minor nor unlikely.
-% The rejection shows that the program is ill-typed.
-% 
-% Yet, the rejection presents as a GCC warning.
-% *1  TAPL-pg1 definition of a type system
+In all case, it is never clear whether the \emph{truth} lies in the compiler or the C standard.
 
 

doc/theses/mike_brooks_MMath/string.tex

@@ -1 +1 @@
 \chapter{String}
 
-\section{String}
+
+
+
 
 \subsection{Logical overlap}

doc/theses/mike_brooks_MMath/uw-ethesis.bib

@@ -114 +114 @@
     pages       = {53-60},
 }
+
+
+@misc{Mendio24,
+    contributer = {pabuhr@plg},
+    title       = {What are the most secure programming languages?},
+    author      = {Mend.io (White Source Ltd.)},
+    year        = 2024,
+    howpublished= {\url{https://www.mend.io/most-secure-programming-languages}},
+}