diff --git a/.github/workflows/compile.yml b/.github/workflows/compile.yml index 53151451..14a19213 100644 --- a/.github/workflows/compile.yml +++ b/.github/workflows/compile.yml @@ -58,4 +58,3 @@ jobs: asset_path: ./${{ env.doc_name }}.pdf asset_name: ${{ env.doc_name }}-snapshot-${{ github.sha }}.pdf asset_content_type: application/pdf - diff --git a/abstract.tex b/abstract.tex index 78a8ffbf..523b565b 100644 --- a/abstract.tex +++ b/abstract.tex @@ -43,10 +43,10 @@ \section*{Abstract} CHERI's hybrid approach allows incremental adoption of capability-oriented design: critical components can be ported and recompiled to use capabilities throughout, providing fine-grain memory protection, or be largely unmodified but encapsulated in ways that permit -only controlled interaction. +only controlled interaction. Potential early deployment scenarios include low-level software Trusted Computing Bases (TCBs) such as separation kernels, hypervisors, and operating-system -kernels, userspace TCBs such as language runtimes and web browsers, +kernels, userspace TCBs such as language runtimes and web browsers, and particularly high-risk software libraries such as data compression, protocol parsing, and image processing (which are concentrations of both complex and historically diff --git a/app-exp-peripherals.tex b/app-exp-peripherals.tex index 9b908c95..9d55e513 100644 --- a/app-exp-peripherals.tex +++ b/app-exp-peripherals.tex @@ -95,7 +95,7 @@ \subsection{Implementation outline} matches the current one, and causes an exception if mismatched \item A privileged instruction takes two capabilities, an input capability and an authorization capability. The output of the instruction is the input -capability with the color changed to match the authorization capability. +capability with the color changed to match the authorization capability. \tmnote{Is this something that should be restricted by a permission? Or by a mode?} \item Checks may be necessary to verify the input capability is a subset of the diff --git a/app-versions.tex b/app-versions.tex index 976ea85d..6c9ac971 100644 --- a/app-versions.tex +++ b/app-versions.tex @@ -207,8 +207,8 @@ \section{Detailed CHERI ISA Version Change History} Satisfyingly, many `future work' items in earlier versions of the report were becoming completed work in this version! -\item[1.3] The fourth version of the architecture document was released - while +\item[1.3] The fourth version of the architecture document was released + while the first functional CHERI prototype was in testing. It reflects on initial experiences adapting a microkernel to exploit CHERI capability features. @@ -400,7 +400,7 @@ \section{Detailed CHERI ISA Version Change History} A new \insnref{CIncOffset} instruction has been added, which avoids the need to read the offset into a general-purpose integer register for frequent arithmetic operations on pointers. - + Interactions between \EPC{} and \EPCC{} are now better specified, including that use of untagged capabilities has undefined behavior. \insnnoref{CBTS} and \insnnoref{CBTU} are now defined to use @@ -918,7 +918,7 @@ \section{Detailed CHERI ISA Version Change History} A new \insnnoref{CCall} selector 1 has been added that provides a jump-like domain transition without use of an architectural exception. In this mode of operation, \insnnoref{CCall} unseals the sealed code and - data capabilities to enter the new domain, offering a different set of + data capabilities to enter the new domain, offering a different set of hardware and software tradeoffs from the existing selector-0 semantics. For example, complex exception-related mechanism is avoided in hardware for domain switches, with the potential to substantially improve performance. diff --git a/chap-assurance.tex b/chap-assurance.tex index 09d68337..b2050a28 100644 --- a/chap-assurance.tex +++ b/chap-assurance.tex @@ -12,21 +12,21 @@ \chapter{CHERI in High-Assurance Systems} \section{Unpredictable Behavior} In the semantics for the CHERI instructions -we try -to avoid defining behavior as ``unpredictable''. There were several reasons +we try +to avoid defining behavior as ``unpredictable''. There were several reasons for avoiding unpredictable behavior, including the difficulty it creates for formal verification. -Although CHERI is based on the MIPS ISA, +Although CHERI is based on the MIPS ISA, the MIPS ISA specification (e.g., for the R4000) makes extensive use of ``unpredictable''. If ``unpredictable'' is modeled as ``anything could happen'', then clearly the system is not secure. -As a +As a concrete example, imagine a hypothetical CHERI implementation that contains a Trojan horse such that when a sandboxed program executes an arithmetic instruction whose result is ``unpredictable'', it also changes the capability registers so that a capability granting access to the entire virtual address space is placed in a capability register. If ``unpredictable'' means that -anything could happen, then this is compliant with the MIPS ISA; it is also +anything could happen, then this is compliant with the MIPS ISA; it is also obviously insecure. Later versions of the MIPS ISA (e.g., MIPS64 volume I) make it clear that ``unpredictable'' is more restrictive than this, saying that ``\emph{unpredictable} operations must not read, write, or modify the contents of @@ -61,7 +61,7 @@ \section{Bypassing the Capability Mechanism Using the TLB} In CheriBSD, user-space programs are unable to modify the TLB (except through system calls such as \ccode{mmap}), and thus cannot carry out this attack. This security argument makes it explicit that the security of the capability -mechanism depends on the correctness of the underlying operating system. +mechanism depends on the correctness of the underlying operating system. However, this may not be adequate for high-assurance systems. \item Similarly, a high-assurance microkernel could run untrusted code in user @@ -92,7 +92,7 @@ \section{Malformed Capabilities} 128-bit capabilities, there are bit patterns corresponding to \cbase{} $+$ \clength{} $> 2^{64}$. The capability registers are initialized on reset, so there will -never be malformed capabilities in the initial register contents, and +never be malformed capabilities in the initial register contents, and a CHERI instruction will never create malformed capabilities from well-formed ones. However, DRAM is not cleared on system reset, so that it is possible that the initial memory might contain malformed capabilities with the @@ -107,7 +107,7 @@ \section{Malformed Capabilities} There are (at least) two implementation choices. An implementation of the CHERI instructions could perform access-control checks in a way that would -work on both well-formed and malformed capabilities. +work on both well-formed and malformed capabilities. Alternatively, the hardware could be slightly simplified by performing the checks in a way that might behave unexpectedly on malformed capabilities, and then rely on the capability @@ -118,7 +118,7 @@ \section{Malformed Capabilities} presents special difficulties in testing. No program whose behavior is defined by the ISA specification will ever trigger the case of encountering a malformed capability. (Programs whose behavior is ``unpredictable'', because -they access uninitialized memory, may encounter them). +they access uninitialized memory, may encounter them). However, some approaches to automatic test generation may have difficulty constructing such tests. @@ -142,7 +142,7 @@ \section{Constants in the Formal Model} \section{Outline of Security Argument for a Reference Monitor} The CHERI ISA can be used to provide several different security properties (for -example, control-flow integrity or sandboxing). This section provides the +example, control-flow integrity or sandboxing). This section provides the outline of a security argument for how the CHERI instructions can be used to implement a reference monitor. @@ -170,7 +170,7 @@ \section{Outline of Security Argument for a Reference Monitor} We are assuming that the system operates in an environment where the attacker does not have physical access to the hardware, so that hardware-level attacks such as introducing memory errors~\cite{Govinda+03} -are not applicable. +are not applicable. %%%% WE MIGHT ALSO MENTION the A2 best paper from IEEE SS&P 2016 on %%%% injecting analog circuit malware into the hardware. @@ -193,7 +193,7 @@ \section{Outline of Security Argument for a Reference Monitor} memory addresses ($S_K$) for the data, code, and stack segments of the trusted code, together with the CHERI reserved registers. -Our security requirement of the hardware is that the untrusted code will run +Our security requirement of the hardware is that the untrusted code will run for a while, eventually returning control to the trusted code; and when the trusted code is re-entered, (a) it will be reentered at one of a small number of known entry points; (b) its code, data and stack will not have been modified @@ -210,7 +210,7 @@ \section{Outline of Security Argument for a Reference Monitor} reference monitor's reserved memory or the reserved registers. That is, all memory accesses are checked against a capability register, and do not succeed unless the capability permits them. The untrusted code can access memory without -returning control to the trusted code; +returning control to the trusted code; however, all of its memory access are mediated by the capability hardware, which is considered to be part of the reference monitor. Tampering with the reference monitor by making physical modifications @@ -253,7 +253,7 @@ \section{Outline of Security Argument for a Reference Monitor} this probably can't be used to attack a real system, any unpredictable behavior has to prevent for provable security). \item -All capability registers have \cbase{} $+$ \clength{} $\leq 2^{64}$ +All capability registers have \cbase{} $+$ \clength{} $\leq 2^{64}$ \algorithmicor{} \ctag{} $=$ \algorithmicfalse{}. \item The above is also true of all capabilities contained within the set of memory @@ -293,10 +293,10 @@ \section{Outline of Security Argument for a Reference Monitor} We assume that \emph{SecureState} is true initially (i.e., a requirement of the trusted code is that it puts the CPU into this state before calling the -untrusted code). +untrusted code). We then wish to show that \emph{SecureState} $\Rightarrow$ \textbf{X} (\emph{SecureState} \algorithmicor{} \emph{TCBEntryState}) (where \textbf{X} is -the next operator in linear temporal logic). By induction on states, +the next operator in linear temporal logic). By induction on states, \emph{SecureState} $\Rightarrow$ \emph{TCBEntryState} \textbf{R} \emph{SecureState} (where \textbf{R} is the release operator in linear temporal logic). @@ -308,7 +308,7 @@ \section{Outline of Security Argument for a Reference Monitor} Given that CP0.Status.KSU $\neq$ 0, CP0.Status.CU0 = \algorithmicfalse{}, CP0.Status.EXL = \algorithmicfalse{} and CP0.Status.ERL = \algorithmicfalse{}, all instructions will either raise an exception (\textbf{X} -\emph{TCBEntryState}) or leave CP0 registers unchanged, leaving this +\emph{TCBEntryState}) or leave CP0 registers unchanged, leaving this part of the \emph{SecureState} invariant unchanged. \item Given that CP0.Status.KSU $\neq$ 0 (etc.), all instructions will @@ -347,7 +347,7 @@ \section{Outline of Security Argument for a Reference Monitor} The theorem \emph{SecureState} $\Rightarrow$ \emph{TCBEntryState} \textbf{R} \emph{SecureState} uses the \textbf{R} operator, which is a weak form of ``until'': the system might continue in \emph{SecureState} indefinitely. -Sometimes it is desirable to have the stronger property that +Sometimes it is desirable to have the stronger property that \emph{TCBEntryState} is guaranteed to be reached eventually. This can be ensured by having the trusted code enable timer interrupts, and use a timer interrupt to force return to \emph{TCBEntryState} if the untrusted @@ -378,7 +378,7 @@ \section{Outline of Security Argument for a Reference Monitor} \emph{SecureStateTimer} $\Rightarrow$ \textbf{F} \emph{TCBEntryState} -It then follows that \emph{SecureStateTimer} $\Rightarrow$ +It then follows that \emph{SecureStateTimer} $\Rightarrow$ \emph{SecureStateTimer} \textbf{U} \emph{TCBEntryState}, where \textbf{U} is the until operator in linear temporal logic. diff --git a/chap-historical.tex b/chap-historical.tex index 19583e9c..86eae398 100644 --- a/chap-historical.tex +++ b/chap-historical.tex @@ -45,8 +45,8 @@ \chapter{Historical Context and Related Work} as overarching emergent system properties~\cite{LevesonYoung14}, and allows the threat model to fall out of the top-down analysis, rather than driving it. This work in some sense -unifies a long thread of work that considers trustworthiness as a property -encompassing security, integrity, reliability, survivability, human safety, +unifies a long thread of work that considers trustworthiness as a property +encompassing security, integrity, reliability, survivability, human safety, and so on (e.g.,~\cite{Neumann06holistic,PSOS}, among others). The Security Research community also blossomed outside of MIT: @@ -96,7 +96,7 @@ \chapter{Historical Context and Related Work} language-based constraints. These apparently disparate areas of research are linked by a duality, observed by Jim Morris -in 1973, between the enforcement of data types and safety goals in programming languages on one hand, +in 1973, between the enforcement of data types and safety goals in programming languages on one hand, and the hardware and software protection techniques explored in operating systems~\cite{morris:protectionprogramming} on the other hand. Each of these approaches blends a combination of limits defined by static analysis @@ -463,7 +463,7 @@ \section{Microkernels} % <<< message passing between separate tasks stood in for hardware-assisted security domain crossings at capability invocation. HYDRA developed a number of ideas, including the relationship between -capabilities and object references, refined the {\em object-capability} paradigm, +capabilities and object references, refined the {\em object-capability} paradigm, and further pursued the separation of policy and mechanism.\footnote{Miller has expanded on the object-capability philosophy in considerable depth in his 2006 PhD dissertation, @@ -545,7 +545,7 @@ \section{Microkernels} % <<< NSA and SCC eventually migrated FLASK to the FLUX microkernel developed by the University of Utah in the search for improved performance. Invigorated by the rise of -microkernels and their congruence with security kernels, +microkernels and their congruence with security kernels, this flurry of operating system security research also faced the limitations (and eventual rejection) of the microkernel approach by the computer industry -- which perceived the performance overheads as too great. @@ -571,8 +571,8 @@ \section{Microkernels} % <<< General-purpose systems also have adopted elements of the microkernel capability design philosophy, such as Apple's Mac OS X~\cite{apple:macosx} (which uses Mach interprocess communication (IPC) -objects as capabilities) and -Cambridge's Capsicum~\cite{Watson10} research project +objects as capabilities) and +Cambridge's Capsicum~\cite{Watson10} research project (which attempts to blend capability-oriented design with UNIX). More influentially, Morris's suggestion of capabilities at the programming language @@ -592,7 +592,7 @@ \section{Microkernels} % <<< % >>> \section{Language and Runtime Approaches} % <<< -Direct reliance on hardware for enforcement (which is central to both historic +Direct reliance on hardware for enforcement (which is central to both historic and current systems) is not the only approach to isolation enforcement. The notion that limits on expressibility in a programming language can be used to enforce security properties is frequently deployed in contemporary systems to @@ -621,8 +621,8 @@ \section{Language and Runtime Approaches} % <<< properties of machine code are enforced through instrumentation to ensure no unsafe access, and Proof-Carrying Code (PCC), in which the safe properties of code are demonstrated through attached and easily verifiable proofs~\cite{necula:pcc}. -As mentioned in the previous section, the -Java Virtual Machine (JVM) model is similar; +As mentioned in the previous section, the +Java Virtual Machine (JVM) model is similar; it combines runtime execution constraints of a restricted, capability-oriented bytecode with a static verifier run over Java classes before they can be loaded into the execution environment; this @@ -631,14 +631,14 @@ \section{Language and Runtime Approaches} % <<< Ruby~\cite{ruby}, offer similar safety guarantees, which can be leveraged to provide security confinement of potentially malicious code without hardware support. -These techniques offer a variety of trade-offs relative to CPU enforcement -of the process model. For example, some (BPF, D) limit expressibility that +These techniques offer a variety of trade-offs relative to CPU enforcement +of the process model. For example, some (BPF, D) limit expressibility that may prevent potentially useful constructs from being used, such as loops -bounded by invariants rather than instruction limits; in doing so, -this can typically impose potentially significant performance overhead. -Systems such as FreeBSD often support just-in-time compilers (JITs) that -convert less efficient virtual-machine bytecode into native code subject to -similar constraints, addressing performance but not expressibility +bounded by invariants rather than instruction limits; in doing so, +this can typically impose potentially significant performance overhead. +Systems such as FreeBSD often support just-in-time compilers (JITs) that +convert less efficient virtual-machine bytecode into native code subject to +similar constraints, addressing performance but not expressibility concerns~\cite{mckusick:freebsd}. Systems like PCC that rely on proof techniques have had limited impact in @@ -668,8 +668,8 @@ \section{Influences of Our Own Past Projects} % <<< transfer, and to allow us to incrementally apply ideas in CHERI to large-scale contemporary applications such as office suites. CHERI's hybrid approach allows a gradual transition from virtual address separation to capability-based -separation within a single address space, -thus +separation within a single address space, +thus restoring programmability and performance so as to facilitate fine-grained compartmentalization throughout the system and its applications. @@ -701,7 +701,7 @@ \section{Influences of Our Own Past Projects} % <<< % >>> \paragraph{PSOS} % <<< SRI's Provably Secure Operating System hardware-software design was formally -specified in a single language (SPECIAL), +specified in a single language (SPECIAL), with encapsulated modular abstraction, interlayer state mappings, and abstract programs relating each layer to those on which it depended~\cite{PSOS,NeumannFeiertag03}. @@ -711,7 +711,7 @@ \section{Influences of Our Own Past Projects} % <<< few primitive types, application-specific object types could be defined and their properties enforced with the hardware assistance provided by the capability-based access controls. The design allowed application layers to -efficiently execute instructions, with object-oriented +efficiently execute instructions, with object-oriented capability-based addressing directly to the hardware -- despite appearing at a much higher layer of abstraction in the design specifications. @@ -727,7 +727,7 @@ \section{Influences of Our Own Past Projects} % <<< Developed in the DARPA CHATS program, the MAC Framework allows static and dynamic extension of the kernel's access-control model, supporting implementation of {\em security localization} -- -that is, +that is, %%% IS THIS CORRECT? IT WAS UNGRAMMATICAL AND AMBIGUOUS the adaptation of the OS security to product and deployment-specific requirements. @@ -735,15 +735,15 @@ \section{Influences of Our Own Past Projects} % <<< control models) found significant use in application sandboxing, especially in Junos, Mac OS X, and iOS. One key lesson from this work is the importance of longer-term thinking about -security-interface design, +security-interface design, including interface stability and support for multiple policy models; these are especially important in instruction-set design. Another important lesson is the increasing criticality of extensibility of not just the access-control model, but also the means by which remote principals -are identified and execute within local systems: -not only is consideration of classical UNIX users inadequate, +are identified and execute within local systems: +not only is consideration of classical UNIX users inadequate, but also there is a need to allow widely varying policies and notions of remote users executing local code across systems. These lessons are taken to heart in capability systems, which carefully @@ -781,18 +781,18 @@ \section{A Fresh Opportunity for Capabilities} % <<< ideas, albeit through the lens of contemporary problems and with insight gained through decades of research into security and systems design. As described in Chapter~\ref{chap:introduction}, a transformed threat environment deriving from ubiquitous computing and networking, and the -practical reality of widespread exploitation of software vulnerabilities, +practical reality of widespread exploitation of software vulnerabilities, both provide a strong motivation to investigate improved processor foundations for software security. -This change in environment has coincided with improved +This change in environment has coincided with improved and more rapid hardware prototyping techniques and higher-level hardware-definition languages that facilitate academic hardware-software system research at larger scales; without them we would have been unable to explore the CHERI approach in such detail. Simultaneously, our understanding of operating-system and programming-language -security has been vastly enhanced by several decades of research; +security has been vastly enhanced by several decades of research; in particular, recent development of the hybrid capability-system Capsicum model suggests a strong alignment between capability-based techniques and successful mitigation approaches that can be diff --git a/chap-model.tex b/chap-model.tex index 2f896e8b..2a5b92dd 100644 --- a/chap-model.tex +++ b/chap-model.tex @@ -75,7 +75,7 @@ \section{Underlying Principles} \end{description} \noindent -These principles, which offer +These principles, which offer substantial mitigations against software vulnerabilities or malicious code, guide the integration of a capability-system model with the general-purpose instruction set -- and @@ -138,7 +138,7 @@ \section{CHERI Capabilities: Strong Protection for Pointers} Consequently, \textit{CHERI capabilities} are designed to represent language-level pointers with additional metadata to protect their integrity and provenance, enforce bounds checks and permissions (and their -monotonicity), and hold additional fields supporting undereferenceable +monotonicity), and hold additional fields supporting undereferenceable (i.e., sealed) software-defined pointers suitable to implement higher-level protection models such as separation and efficient compartmentalization. @@ -157,7 +157,7 @@ \section{CHERI Capabilities: Strong Protection for Pointers} virtual-memory models -- which see wide use today and continue to operate on CHERI-enabled systems. This is possible by virtue of CHERI having a \textit{hybrid capability model} -that +that securely composes a capability-system model with conventional architectural features and programming-language pointer interpretation. @@ -406,7 +406,7 @@ \subsection{Tags for Pointer Integrity and Provenance} identified in the address space, which can help support techniques such as garbage collection. -Our CHERI +Our CHERI prototypes implement tagged memory using partitioned memory, with tags and associated capability-sized units linked close to the memory controller, and propagated by the cache hierarchy in order to provide strong atomicity with @@ -463,7 +463,7 @@ \subsection{Permissions on Capabilities} permissions so that pointers to data cannot be reused for instruction fetch, or so that pointers to code cannot be used to store data. Further permissions control the ability to load and store capabilities -themselves, allowing the compiler to implement policies such as +themselves, allowing the compiler to implement policies such as \textit{dereferenceable code and data pointers cannot be loaded from character strings.} Permissions can also be made accessible to higher-level aspects of the @@ -521,7 +521,7 @@ \subsection{Capability Monotonicity via Guarded Manipulation} % defining what ``vast majority'' means, \textit{capability % monotonicity} could also be replaced by \textit{capability bounds % monotonicity} and \textit{capability permission monotonicity}.} -%by +%by %\psnote{think we can just delete this: ``virtue of \textit{guarded manipulation}: they cannot %represent non-monotonic transformations. %This is accomplished via''. I don't see a need to introduce the @@ -825,7 +825,7 @@ \subsection{Capability Flow Control} be used only for data access -- if suitably configured. This can be used to create regions of shared memory within an address space through which capabilities cannot flow. - For example, it can + For example, it can prevent two separated compartments from delegating access to one another's memory regions, instead limiting @@ -867,7 +867,7 @@ \subsection{Capability Flow Control} bits due to a non-propagation goal) can simply remove the load-capability permission from the source capability before beginning a memory copy. %%%% THIS only SEEMS TO BE IN THE RIGHT PLACE: only specific data, -%%%% RATHER THAN data only from a source capability!!! +%%%% RATHER THAN data only from a source capability!!! On the other hand, it is often desirable to detect stripping of a capability on store\psnote{this may also appear cryptic} via a hardware exception, to ease debugging. @@ -885,7 +885,7 @@ \subsection{Capability Flow Control} a capability-oblivious memory copy via a capability that does not authorize capability store, or the ability to transparently strip tags on store to a shared memory page. -However, we have not yet found these particular combinations valuable in our software experimentation, +However, we have not yet found these particular combinations valuable in our software experimentation, \subsection{Capability Compression} \label{sec:model-compression} @@ -1065,7 +1065,7 @@ \subsection{Capability Revocation, Garbage Collection, and Flow Control} capability mechanism. Combined with a policy of either non-reuse of virtual address space (as distinct from non-reuse of physical address space), sweeping revocation, or - garbage collection, this + garbage collection, this allows all outstanding capabilities (and any further capabilities derived from them) to be revoked without the need to search for those capabilities in the register file or memory. @@ -1220,11 +1220,11 @@ \section{Software Protection and Security Using CHERI} by the ISA and how they are mapped into programmer-visible constructs such as C-language features. The description in this chapter is intended to be agnostic to the specific -Instruction-Set Architecture (ISA) in which CHERI is implemented. +Instruction-Set Architecture (ISA) in which CHERI is implemented. In particular, it is important that programmers be able to rely on the properties described in this chapter -- regardless of the ISA-level -implementation -- -and that software abstractions built over these properties have +implementation -- +and that software abstractions built over these properties have consistent behavior that can be depended upon to mitigate vulnerabilities. \subsection{Abstract Capabilities} @@ -1281,8 +1281,8 @@ \subsection{C/C++ Language Support} \item[Software compartmentalization] CHERI provides hardware foundations for highly efficient \textit{software compartmentalization}, the fine-grained decomposition of -larger software packages into -smaller isolated components that are +larger software packages into +smaller isolated components that are granted access only to the memory (and also software-defined) resources they actually require. @@ -1296,13 +1296,13 @@ \subsection{C/C++ Language Support} \end{description} \noindent -CHERI protections are implemented by a blend of +CHERI protections are implemented by a blend of functionality: \begin{description} \item[Compiler and linker] responsible for generating code that manipulates - and dereferences code and data pointers, compile-time linkage, and + and dereferences code and data pointers, compile-time linkage, and stack allocation. \item[Language runtime] responsible for ensuring that program run-time @@ -1324,8 +1324,8 @@ \subsection{C/C++ Language Support} \subsubsection{Data-Pointer Protection} -Depending on -the desired +Depending on +the desired compilation mode, some or all data pointers will be implemented using capabilities. We anticipate that memory allocation (whether from the stack or heap, or via @@ -1414,7 +1414,7 @@ \subsection{Protecting Non-Pointer Types} \begin{itemize} \item Using CHERI capabilities to represent hardware resources such as physical addresses, interrupt numbers, and so on, where software will - provide implementation (e.g., allocation, mapping, masking), but + provide implementation (e.g., allocation, mapping, masking), but where capabilities can be stored and delegated. @@ -1440,7 +1440,7 @@ \subsection{Protecting Physical Addresses} additional permissions would be necessary (e.g. dirty). \paragraph{Synergy with linear capabilities and enclaves} -Linear physical capabilities could support low-overhead enclaves. +Linear physical capabilities could support low-overhead enclaves. If a physical capability could be linear, such that each instance is guaranteed to be the unique reference to that physical memory, an enclave could be certain that its virtual memory mapping is the only route to access that @@ -1709,7 +1709,7 @@ \subsection{Operating-System Support} processor, initializes register state during context creation, and saves/restores capability state during context switches, with the goal of supporting use of capabilities in userspace. - Virtual memory is extended to maintain tag + Virtual memory is extended to maintain tag integrity across swapping, and to prevent tags from being used with objects that cannot support them persistently @@ -1723,7 +1723,7 @@ \subsection{Operating-System Support} programs. \item[Capability domain switching in userspace] Similar - to the minimally modified kernel model, + to the minimally modified kernel model, only modest changes are made to the kernel itself. However, some additional extensions are made to the process model in order to support multiple mutually distrusting security domains within user diff --git a/chap-research.tex b/chap-research.tex index 62cd0e5b..805db493 100644 --- a/chap-research.tex +++ b/chap-research.tex @@ -10,7 +10,7 @@ \section{Motivation} The CHERI protection model provides a sound and formally based architectural foundation for the principled development of highly trustworthy systems. -The CHERI approach builds on and extends decades of research into hardware and +The CHERI approach builds on and extends decades of research into hardware and operating-system security.\footnote{Levy's {\em Capability-Based Computer Systems}~\cite{levy:capabilities} provides a detailed history of segment- and capability-based designs through the early 1990s~\cite{levy:capabilities}. @@ -19,11 +19,11 @@ \section{Motivation} well as capability-influenced virtual machines such as the Java Virtual Machine~\cite{Gong99}, begins. Chapter~\ref{chap:historical} discuss historical influences on our work in greater detail.} -However, some of the historic approaches that CHERI incorporates (especially capability architectures) +However, some of the historic approaches that CHERI incorporates (especially capability architectures) have not been adopted in commodity hardware designs. -In light of these past transition failures, a reasonable question +In light of these past transition failures, a reasonable question is ``Why now?'' -What has changed that could allow CHERI to succeed where +What has changed that could allow CHERI to succeed where so many previous efforts have failed? Several factors have motivated our decision to begin and carry out this project: @@ -31,7 +31,7 @@ \section{Motivation} \item Dramatic changes in threat models, resulting from ubiquitous connectivity and pervasive uses of computer technology in many diverse and widely used applications such as wireless mobile -devices, automobiles, and critical infrastructure. +devices, automobiles, and critical infrastructure. In addition, cloud computing and storage, robotics, software-defined networking. safety of autonomous systems, and the Internet of Things have significantly widened the range of vulnerabilities that can be exploited. @@ -72,11 +72,11 @@ \section{Motivation} much more diverse, running on a wide variety of instruction set architectures (especially ARM and MIPS). -\item Similarly, +\item Similarly, new diversity in operating systems has arisen, in which commercial products such as Apple's iOS and Google's Android extend open-source systems such as FreeBSD, Mach~\cite{accetta:mach}, and Linux. -These new platforms abandon many traditional constraints, requiring +These new platforms abandon many traditional constraints, requiring that rewritten applications conform to new security models, programming languages, hardware architectures, and user-input modalities. @@ -126,7 +126,7 @@ \subsection{C-Language Trusted Computing Bases (TCBs)} The results present not only significant risks of compromise that lead to financial loss or disruption of critical infrastructure, but also frequent occurrences of such events. -Software vulnerabilities appear inevitable; +Software vulnerabilities appear inevitable; indeed, an arms race has arisen in new (often probabilistic) software-based mitigation techniques and exploit techniques that bypass them. @@ -152,13 +152,13 @@ \subsection{The Software Compartmentalization Problem} software. Historically, compartmentalization of TCB components such as operating system kernels and central system services has caused significant -difficulty for software developers -- which limits its applicability for large-scale, +difficulty for software developers -- which limits its applicability for large-scale, real-world applications, and leads to the abandonment of promising research such as 1990s {\em microkernel} projects. A recent resurgence of compartmentalization, applied in userspace to system software and applications such as OpenSSH~\cite{provos:preventingprivesc} and Chromium~\cite{reis:chromium}, and more recently in our own Capsicum project~\cite{Watson10}, has been motivated by a -critical security need; however it has seen success only at very coarse separation granularity due to +critical security need; however it has seen success only at very coarse separation granularity due to the challenges involved. A more detailed history of work in this area can be found in Chapter~\ref{chap:historical}. @@ -172,7 +172,7 @@ \subsection{The Software Compartmentalization Problem} critically, security. These problems occur because current hardware provides strong separation -only at coarse granularity via rings and virtual address spaces, making +only at coarse granularity via rings and virtual address spaces, making the isolation of complete applications (or even multiple operating systems) a simple task, but complicates efficient and easily expressed separation between tightly coupled software @@ -190,7 +190,7 @@ \subsection{The Software Compartmentalization Problem} requiring multiple TLB entries, one for each authorized security domain. High-end server CPUs typically have TLB entries in the low hundreds, and -even recent network embedded devices reach +even recent network embedded devices reach the low thousands; the TLB footprint of fine-grained, compartmentalized software increases with the product of in-flight security domains and objects due to TLB aliasing, which may easily require @@ -472,7 +472,7 @@ \section{Research and Development} \noindent Another key early design choice was the goal of using capabilities to implement C-language pointers -- initially discretionarily (i.e., as annotated -in the language), and later ubiquitously (i.e., for all virtual addresses in a +in the language), and later ubiquitously (i.e., for all virtual addresses in a more-secure program). This required an inevitable negotiation between C-language semantics and the capability-system model, in order to ensure strong compatibility with current @@ -533,7 +533,7 @@ \section{Research and Development} directly supports the construction of confined components within address spaces. Using this approach, we can place code in execution with only limited -access to virtual memory, constructing ``sandboxes'' (and other more complex +access to virtual memory, constructing ``sandboxes'' (and other more complex structures) within conventional processes. The CHERI exception model permits transition to a more privileged component -- e.g., the operating-system kernel or language runtime -- allowing the @@ -545,7 +545,7 @@ \section{Research and Development} no hardware interpretation (i.e., cannot be dereferenced), and also strong encapsulation (i.e., whose fields are immutable). Other aspects of the model include a type mechanism allowing sealed code and -data capabilities to be inextricably linked; pairs of sealed code +data capabilities to be inextricably linked; pairs of sealed code capabilities and data capabilities can then be used to efficiently describe protection domains via an object-capability model. @@ -778,9 +778,9 @@ \section{Threat Model} of privilege within a framework for controlled separation and communication. Code in execution can represent the focus of many potentially malicious parties: subversion of legitimate code in violation of security policies, injection of malicious -code via back doors, Trojan horses, and malware, and also +code via back doors, Trojan horses, and malware, and also denial-of-service attacks. -CHERI's fine-grained memory protection mitigates +CHERI's fine-grained memory protection mitigates many common attack techniques by implementing bounds and permission checks, reducing opportunities for the conflation of code and data, corruption of control flow, and also catches many common exploitable programmer bugs; @@ -791,7 +791,7 @@ \section{Threat Model} although CHERI CPUs might easily be used in the context of tamper-evident or tamper-resistant systems. Similarly, no special steps have been taken in our design to counter undesired -leakage of electromagnetic emanations and certain other side channels such as acoustic inferences: +leakage of electromagnetic emanations and certain other side channels such as acoustic inferences: we take for granted the presence of an electronic foundation on which CHERI can run. CHERI will provide a supportive framework for a broad variety of security-sensitive @@ -804,7 +804,7 @@ \section{Threat Model} protection within a system, the greater the potential impact of unauthorized communication channels. As such, we hope side-channel attacks are a topic that we will be able to -explore in future work. +explore in future work. Overall, we believe that our threat model is realistic and will lead to systems that can be substantially more trustworthy than today's commodity systems -- while recognizing that ISA-level protections must @@ -840,7 +840,7 @@ \section{Formal Methodology} % These tools will allow us to verify low-level properties of the hardware design % and use the power of model checking and satisfiability solvers to analyze % related properties. -% Ideally they will also help link ISA-level specifications with the CPU implementation. +% Ideally they will also help link ISA-level specifications with the CPU implementation. \item We then developed more complete CHERI-MIPS ISA models, @@ -861,7 +861,7 @@ \section{Formal Methodology} % PS: this is pasted from new intro text L3 and Sail support automatic generation of versions of the models in the definition languages of (variously) the -HOL4, Isabelle, and Coq theorem provers. +HOL4, Isabelle, and Coq theorem provers. Key architectural verification goals including proving not just low-level properties, such as the monotonicity of each individual instruction and properties of the CHERI capability compression schemes, but also @@ -881,7 +881,7 @@ \section{Formal Methodology} \item From Sail, we also automatically generate SMT problems, which we have used to check properties of our capability compression - schemes. + schemes. \item We have explored how CHERI impacts a formal specification of C-language diff --git a/cheri.bib b/cheri.bib index 9f737494..14ee80fb 100644 --- a/cheri.bib +++ b/cheri.bib @@ -16547,7 +16547,7 @@ @inproceedings{DBLP:conf/esop/BauereissCSAESB22 {ESOP} 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, {ETAPS} 2022, Munich, Germany, April 2-7, 2022, Proceedings}, - booktitle = {31st European Symposium on Programming, {ESOP} 2022}, + booktitle = {31st European Symposium on Programming, {ESOP} 2022}, series = {Lecture Notes in Computer Science}, volume = {13240}, pages = {174--203}, diff --git a/glossary.tex b/glossary.tex index 004c5f17..80fd0863 100644 --- a/glossary.tex +++ b/glossary.tex @@ -14,7 +14,7 @@ maintenance of capability lifespan across operations that violate architectural \gls{capability provenance}. For example, if an OS kernel - swaps a page containing a capability to and from disk, + swaps a page containing a capability to and from disk, it will have to have its \gls{capability tag} restored through re-derivation, so there is no longer an architectural provenance relationship between the two, but for @@ -134,13 +134,13 @@ that any requested manipulation of a \gls{capability}, whether in a \gls{capability register} or in memory, either leads to strictly non-increasing rights, clearing of the \gls{capability tag}, or a - hardware exception. + hardware exception. \knnote{I presume that the ``rights'' of a capability are determined by its permissions and its bounds, but not by its sealedness. In other words, increasing the permissions or bounds of a capability would increase its rights, but unsealing a capability would not increase its right. If this is correct, - perhaps it could help to explicitly state this here.} + perhaps it could help to explicitly state this here.} Controlled violation of monotonicity can be achieved via the exception delivery mechanism, which grants rights to additional capability register, and also by the \gls{CInvoke} instruction, which may @@ -213,15 +213,15 @@ % PS: not totally clear what a ``valid capability operation'' is. An % execution of a capability instruction that doesn't raise an exception? Provenance is implemented using a \gls{capability tag} combined with - \gls{capability monotonicity}, + \gls{capability monotonicity}, % PS: the text (both previous version and mine) defines provenance as % a property of the architecture, not ``the provenance of a % capability'' as the source capability or derivation chain, so we -% can't say ``will be preserved'' like the text did. +% can't say ``will be preserved'' like the text did. % Maybe we should define that more explicit notion of provenance, and % replace this glossary entry with one for ``capability provenance -% preservation'', but I've not for now. -irrespective of +% preservation'', but I've not for now. +irrespective of % whether a capability is held in a \gls{capability register} or \gls{tagged memory}} @@ -256,7 +256,7 @@ \glslink{dereference}{dereferenced} via the ISA. If the tag is clear, then the capability is invalid and cannot be dereferenced via the ISA. - Tags are preserved + Tags are preserved by ISA operations that conform to \gls{capability provenance} and \gls{capability monotonicity} rules -- for example, @@ -728,7 +728,7 @@ { name=sealing capability, plural=sealing capabilities, - description={A sealing capability is one with the \cappermSeal + description={A sealing capability is one with the \cappermSeal permission, allowing it to be used to create \glspl{sealed capability} using a \gls{capability object type} set to the sealing capability's \gls{address}, and subject to its bounds}