Index: doc/theses/mike_brooks_MMath/background.tex =================================================================== --- doc/theses/mike_brooks_MMath/background.tex (revision f2b74e3f78b66c01e00cabbc247f8b063ae7696a) +++ doc/theses/mike_brooks_MMath/background.tex (revision fe6047c9f454f4896c388e4012c6958cf83004c7) @@ -620,6 +620,12 @@ In fact, the outermost type constructor (syntactically first dimension) is really the one that determines the parameter flavour. -\PAB{TODO: add examples of mycode/arrr/bugs/c-dependent/x.cfa:v5102,5103, -which are shocking how much C ignores.} +C ignores length information given in parameter declarations entirely, when determining a function's type. +For example, it accepts this pair of declarations +\begin{cfa} + void f( int, float[][42] ); $\C{// array of len-42 arrays}$ + void f( int n, float[][n] ); $\C{// array of VLAs}$ +\end{cfa} +as a repeat, without an error about conflicting types for @f@. +Yet, entirely different stride calculations would occur in a function body whose parameters were declared in each of the two styles. \begin{figure} @@ -668,5 +674,5 @@ An array parameter declaration can specify the outermost dimension with a dimension value, @[10]@ (which is ignored), an empty dimension list, @[ ]@, or a pointer, @*@, as seen in \VRef[Figure]{f:ArParmEquivDecl}. The rationale for rejecting the first invalid row follows shortly, while the second invalid row is nonsense, included to complete the pattern; its syntax hints at what the final row actually achieves. -Note, in the leftmost style, the typechecker ignores the actual value even in a dynamic expression. +Note, in the leftmost style, the typechecker ignores the actual value, even for a dynamic expression. \begin{cfa} int N; Index: doc/theses/mike_brooks_MMath/intro.tex =================================================================== --- doc/theses/mike_brooks_MMath/intro.tex (revision f2b74e3f78b66c01e00cabbc247f8b063ae7696a) +++ doc/theses/mike_brooks_MMath/intro.tex (revision fe6047c9f454f4896c388e4012c6958cf83004c7) @@ -1,16 +1,34 @@ \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-lists are built from (recursive) pointer types, and strings from a combination of array and linked-list. -For all three types, languages and/or their libraries supply varying degrees of high-level mechanisms for manipulating these objects at the bulk and component level, such as copying, slicing, extracting, and iterating among elements. +All modern programming languages provide at least these three high-level containers (collections): array, linked-list, and string. +Often, the array is part of the programming language, while linked lists are built from (recursive) pointer types, and strings from arrays and/or linked lists. +For all three types, languages and/or their libraries supply varying degrees of high-level mechanisms for manipulating these objects at the bulk and component levels, such as copying, slicing, extracting, and iterating among elements. -Unfortunately, these three aspects of C cause a significant number of memory errors~\cite{Oorschot23}. +Unfortunately, memory misuse under C-idiomatic programming causes a significant number of errors~\cite{Oorschot23}. Estimates suggest 50\%~\cite{Mendio24} of total reported open-source vulnerabilities occurring in C result from errors using these facilities (memory errors). For operating system and browser vendors, who heavily use systems languages, 60\%--70\% of reported software vulnerabilities involved memory errors~\cite{Kehrer23}. For Microsoft, 70\% of vulnerabilities addressed via security updates between 2006--2018 are memory safety issues~\cite[slide 10]{Miller19}. -In a study of software exploits in the U.S. National Vulnerability Database over 2013--2017, the top reported vulnerability is (memory) buffer errors, among 19 vulnerability categories~\cite{Cifuentes19}. -Therefore, hardening these three C types goes a long way to make the majority of C programs safer and eliminating major hacker attack-vectors. +In a study of software exploits in the U.S. National Vulnerability Database over 2013--2017, the top reported vulnerability is buffer errors (in the sense of misused array bounds), among 19 vulnerability categories~\cite{Cifuentes19}. -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. +While these figures address memory errors, defined without limit to the three primary collections, these authors' explanations of memory errors, among other C analysis efforts, suggest improving on C's language/library options for working with these three collections would be widely beneficial. +Every one of the safety-statistic sources above includes array bounds in its first characterization of unsafe programming-language features. +Of the four studies that deal exclusively with memory safety (excluding~\cite{Cifuentes19}), all put @malloc@--@free@ upfront as well. +The one that specifically surveys C features, \cite{Oorschot23}, also has similarly prominent blame on both of: the null-terminated text idiom, with its support/mandate in the C standard library; the unprotected nature of C pointers. +An effort at translating C to safe Rust~\cite{Emre2022} has pointers as the stand-out difficult aspect to analyze.\footnote{ + \cite{Emre2022} demonstrates the difficulty of analyzing C pointers for safety (while tacking some of this difficult problem). + It first puts a corpus of C programs through a naive Rust translation, which ``succeeds'' by leaving many uses of Rust's \lstinline{unsafe} marker. + Then, it analyzes these uses and presents a technique for reducing those uses that hinge exclusively on referenced object lifetime. + Pointer dereference accounts for 80\% of the cases that the naive translation did not make safe (Table 3.2, p33). + Of these, 10\% are eligible for the work's own safety improvement technique, while this filtering leaves 75\% with no single cause of unsafety determined (Table 3.5, p39). + The presented technique succeeds at making 75\% of the eligible initially unsafe dereferences safe, by inferring the necessary lifetime annotations (Table 4.2, p83). + This result leaves, per 1000 LOC, 3.3 unremovable unsafe dereferences that are understood to evade lifetime analysis, among 220 gross unsafe dereferences (Tables 3.5, 4.2 and 3.1, p27). + % 3.3 = 1398/413,428 * 1000 + % 220 ~= (99,101 [@tab3.5] - 9631 [@tab4.2] ) / 413,428 [@tab 3.1] * 1000 +} +A tool for analyzing C code's use of linked data structures (including, \eg skip list and binary tree) found variations of the linked-list shape to be present in most of the programs in its corpus~\cite{White2016}. +So, C's array unsafety is infamous, its string pattern necessitates explicit storage management (also infamous), and user-written linked lists are an attrictively recognizable player in the arena of (infamously) unsafe raw pointer uses. +Therefore, hardening the three primary collections goes a long way to making the majority of C programs safer, and eliminating major hacker attack vectors. + +This work looks at extending these 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. @@ -30,5 +48,6 @@ C provides a simple array type as a language feature. -However, it adopts the controversial position of treating pointer and array as duals, leading to multiple problems. +However, it adopts the controversial position of treating pointer and array as twins, leading to multiple problems. +The way that arrays are typicaly passed around a program removes the information necessary to do bound checks. @@ -41,5 +60,5 @@ otherwise, elements are heap allocated with internal or external link fields. -C provides a few simple, polymorphic, library data-structures (@glibc@): +C provides a few simple, library data-structures (@glibc@): \begin{itemize} \item @@ -48,5 +67,5 @@ hash search table consisting of a key (string) with associated data (@@) \end{itemize} -Because these container libraries can be restrictive, awkward to use, and unsafe, C programmers often build bespoke linked data-structures, which further increases the potential for memory errors. +Because these container libraries can be restrictive or awkward to use, C programmers often build bespoke linked data-structures, which further increases the potential for memory errors. Index: doc/theses/mike_brooks_MMath/uw-ethesis-frontpgs.tex =================================================================== --- doc/theses/mike_brooks_MMath/uw-ethesis-frontpgs.tex (revision f2b74e3f78b66c01e00cabbc247f8b063ae7696a) +++ doc/theses/mike_brooks_MMath/uw-ethesis-frontpgs.tex (revision fe6047c9f454f4896c388e4012c6958cf83004c7) @@ -131,18 +131,18 @@ \CFA strives to fix mistakes in C, chief among them, safety. This thesis presents a significant step forward in \CFA's goal to remove unsafe pointer operations. -The thesis presents improvements to the \CFA language design, both syntax and semantics, to support advanced container features. -These features are implemented across the \CFA compiler, libraries, and runtime system. -The results maintain another \CFA goal of remaining 99\% backwards compatible with C. -This thesis leverages preexisting work within the compiler's type and runtime systems generated by prior students working on the \CFA project. - -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-lists are built from (recursive) pointer types, and strings from a combination of array and linked-list. -For all three types, languages and/or their libraries supply varying degrees of high-level mechanisms for manipulating these objects at the bulk and component level, such as copying, slicing, extracting, and iterating among elements. -Unfortunately, these three aspects of C cause 60\%--70\% of the reported software vulnerabilities involving memory errors, and 70\%--80\% of hacker attack-vectors target these types. +It describes improvements to the \CFA language design to support advanced container features. +These features are implemented across the \CFA compiler and runtime libraries. +The results maintain another \CFA goal of offering strong backwards compatibility with C. +This work leverages preexisting \CFA contributiongs of prior students working on the \CFA project, particularly through novel applications of the compiler's type system. + +All modern programming languages provide at least these three high-level containers (collections): array, linked-list, and string. +Often, the array is part of the programming language, while linked lists are built from (recursive) pointer types, and strings from arrays and/or linked lists. +For all three types, languages and/or their libraries supply varying degrees of high-level mechanisms for manipulating these objects at the bulk and component levels, such as copying, slicing, extracting, and iterating among elements. +Unfortunately, typical solutions for the the key types in C cause 60\%--70\% of the reported software vulnerabilities involving memory errors; 70\%--80\% of hacker attack vectors target these types. Therefore, hardening these three C types goes a long way to make the majority of C programs safer. Specifically, an array utility is provided that tracks length internally, relieving the user of managing explicit length parameters and stopping buffer-overrun errors. This feature requires augmenting the \CFA type system, making array length available at compile and runtime. -A linked-list utility is provided, which obviates many explicit recursive pointers by catering directly to system-programming uses (intrusive lists) for which a library solution is often dismissed. +A linked-list utility is provided, which obviates many user-managed recursive pointers by catering directly to system-programming uses (intrusive linking, ad-hoc listing) for which a library solution is often dismissed. Finally, a string utility is provided with implicit memory management of text in a specialized heap, relieving error-prone buffer management, including overrun, and providing a copy-on-write speed boost. For all three utilities, performance is argued to be on-par with, and occasionally surpassing relevant comparators. Index: doc/theses/mike_brooks_MMath/uw-ethesis.bib =================================================================== --- doc/theses/mike_brooks_MMath/uw-ethesis.bib (revision f2b74e3f78b66c01e00cabbc247f8b063ae7696a) +++ doc/theses/mike_brooks_MMath/uw-ethesis.bib (revision fe6047c9f454f4896c388e4012c6958cf83004c7) @@ -94,4 +94,7 @@ } +% ------------------------------------------------- +% Safety + @article{Blache19, author = {Gunter Blache}, @@ -122,4 +125,31 @@ } +@phdthesis{Emre2022, + author = "Mehmet Emre", + title = "Translating C to Safe Rust: Reasoning about Pointer Types and Lifetimes", + school = "UC Santa Barbara", + year = "2022" +} + +@inproceedings{White2016, + author = {White, David H. and Rupprecht, Thomas and L\"{u}ttgen, Gerald}, + title = {DSI: an evidence-based approach to identify dynamic data structures in C programs}, + year = {2016}, + isbn = {9781450343909}, + publisher = {Association for Computing Machinery}, + address = {New York, NY, USA}, + url = {https://doi.org/10.1145/2931037.2931071}, + doi = {10.1145/2931037.2931071}, + booktitle = {Proceedings of the 25th International Symposium on Software Testing and Analysis}, + pages = {259–269}, + numpages = {11}, + keywords = {Data structure identification, dynamic data structures, pointer programs, program comprehension}, + location = {Saarbr\"{u}cken, Germany}, + series = {ISSTA 2016} +} + +% ----------------------------------------------- +% Misc + @misc{RVO20, contributer = {pabuhr@plg}, @@ -149,2 +179,3 @@ howpublished= {\url{https://c-faq.com/decl/spiral.anderson.html}}, } +