Changes in / [774c97e:6abb6dc]

Location:

doc

Files:

• bibliography/pl.bib (modified) (2 diffs)
• theses/mike_brooks_MMath/intro.tex (modified) (3 diffs)
• theses/mike_brooks_MMath/string.tex (modified) (1 diff)
• theses/mike_brooks_MMath/uw-ethesis.bib (modified) (1 diff)

doc/bibliography/pl.bib

@@ -3088 +3088 @@
     note        = {WikipediA},
     howpublished= {\url{http://www.akkadia.org/drepper/tls.pdf}},
-}
-
-@misc{DARPA24,
-    contributer = {pabuhr@plg},
-    title       = {Eliminating Memory Safety Vulnerabilities Once and For All},
-    author      = {Defense Advanced Research Projects Agency},
-    year        = 2024,
-    month       = jul,
-    howpublished= {\url{https://www.darpa.mil/news-events/2024-07-31a}},
 }
 
@@ -7695 +7686 @@
 }
 
-@misc{WhiteHouse24,
-    contributer = {pabuhr@plg},
-    title       = {Part {II}: Securing the Building Blocks of Cyberspace},
-    author      = {U.S. Federal Government},
-    year        = 2024,
-    howpublished= {\url{https://www.whitehouse.gov/wp-content/uploads/2024/02/Final-ONCD-Technical-Report.pdf}},
-}
-
 @inproceedings{Chen07,
     keywords    = {chip multiprocessors, constructive cache sharing, parallel depth first, scheduling algorithms, thread granularity, work stealing, working set profiling},

doc/theses/mike_brooks_MMath/intro.tex

@@ -1 +1 @@
 \chapter{Introduction}
 
-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.
+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.
 
 
 \section{Array}
 
-An array provides a homogeneous container with $O(1)$ access to elements using subscripting.
+An array provides a homogeneous container with $O(1)$ access to elements using subscripting (some form of pointer arithmetic).
 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 (some form of pointer arithmetic).
+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.
 
 
 \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 that normally involve pointer chasing.
+A linked-list provides a homogeneous container often with $O(log N)$/$O(N)$ access to elements using successor and predecessor operations.
 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 with explicitly/implicitly managed.
+otherwise, elements are heap allocated and explicitly/implicitly managed.
 
 
@@ -31 +28 @@
 
 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, \eg @index@ and @substr@.
+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@.
 Subscripting individual elements is often available.
-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.
+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.
 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 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).
+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.
 
 
@@ -64 +46 @@
 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 (@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.
+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.
 These example programs show
-\begin{itemize}[leftmargin=*]
-        \item if the compiler accepts or rejects certain syntax,
+\begin{itemize}
+        \item the compiler accepts or rejects certain syntax,
         \item prints output to buttress a claim of behaviour,
-        \item or executes without triggering any embedded assertions testing pre/post-assertions or invariants.
+        \item 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, it is never clear whether the \emph{truth} lies in the compiler or the C standard.
+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
 
 

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}},
-}