Table of Contents for Programming Languages: a survey
https://en.wikipedia.org/wiki/E_(programming_language)
Links:
http://www.cl.cam.ac.uk/research/security/ctsrd/cheri/ https://www.cl.cam.ac.uk/research/security/ctsrd/pdfs/201406-isca2014-cheri.pdf
current spec: http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-891.pdf
Capability Hardware Enhanced RISC Instructions (CHERI)
" To this end, CHERI blends traditional paged virtual memory with a per-address-space capability model that includes capability registers, capability instructions, and tagged memory that have been added to the 64-bit MIPS ISA. CHERI learns from the C-language fat-pointer literature: its capabilities describe fine-grained regions of memory and can be substituted for data or code pointers in generated code, protecting data and also providing Control-Flow Integrity (CFI). Strong monotonicity properties allow the CHERI capability model to express a variety of protection properties, from valid C-language pointer provenance and bounds checking to implementing the isolation and controlled commu- nication structures required for higher-level models such as software compartmentalization.
...
CHERI sup- ports architectural least privilege through in-address-space memory capabilities , which replace integer virtual-address representations of code and data pointers to allow fine-grained protec- tion of in-memory data, and also control-flow integrity. This application of least privilege provides strong protection against a broad range of memory- and pointer-based vulnerabilities and exploit techniques – buffer overflows, format-string attacks, pointer-corruption attacks, and so on.
...
CHERI capabilities limit how pointers can be used by scoping the ranges of memory (via bounds) and operations that can be performed (via permissions).
...
combining fat pointers with capabilities, allowing capabilities to be substituted for C pointers with only limited changes to program semantics.
...
We do, however, hypothesize that some of the efficiencies and safety features found in the hardware implementation would be difficult to accomplish in a software transformation: for example, automatic and atomic clearing of tags for in-memory pointers during arbitrary memory writes might come at substantial expense in software, but are “free” in hardware.
...
capability registers describe the rights ( protection domain ) of the executing thread to memory that it can access, and to object references that can be invoked to tran- sition between protection domains. We model these registers as a separate capability register file , supplementing the general-purpose file. Over time, we imagine that capa- bility registers will displace general-purpose registers as the preferred means to describe data and object references. Capability registers contain a tag, sealed bit, permission mask, base, length, and offset (allowing the description of not just bounded regions, but also a pointer into that region, improving C-language compatibility). Capability registers are suitable for describing both data and code, and can hence protect both data integrity/con- fidentiality and control flow. Certain registers are reserved for use in exception handling; all others are available to be managed by the compiler using the same techniques used with conventional registers.
...
capability instructions allow executing code to create, constrain (e.g., by increasing the base, decreasing the length, or reducing permissions), manage, and inspect capability register values. Both unsealed (memory) and sealed (object) capabilities can be loaded and stored via memory capability registers (i.e., dereferencing); object capabilities can be invoked, via special instructions, allowing a transition between protection domains, but their fields are given additional integrity protections to provide encapsulation. Capabil- ity instructions implement guarded manipulation
...
Tagged memory associates a 1-bit tag with each capability-aligned and capability-sized word in physical memory, which allows capabilities to be safely loaded and stored in memory without loss of integrity. This functionality expands a thread’s effective pro- tection domain to include the transitive closure of capability values that can be loaded via capabilities via those present in its register file. For example, a capability register representing a C pointer to a data structure can be used to load further capabilities from that structure, referring to further data structures, which could not be accessed without suitable capabilities. Writes to capability values in memory that do not originate from a valid capability in the capability-register file will clear the tag bit associated with that memory, preventing accidental (or malicious) dereferencing of invalid capabilities.
...
Each capability (whether held in a register or stored in memory) has an associated 1-bit tag that consistently tracks pointer validity. In-memory tags are maintained by the memory subsystem as 1 bit for each capability-sized capability-aligned unit of memory (either 128 bits or 256 bits, depending on the ISA variant); they are not directly addressable. Other metadata associated with capabilities (e.g., bounds and permissions) are stored in addressable memory and protected by the corresponding tag bits. Tags follow capabilities into and out of capability registers with corresponding loads and stores. Capabilities are valid for dereference – for load, store, and instruction fetch – only if the tag is set. Dereferencing an untagged capability (i.e., one without a tag set) will cause a hard- ware exception. Tagged capabilities can be constructed only by deriving them from existing tagged capabilities, which ensures pointer provenance . Attempts to overwrite all or a portion of a capability in memory will automatically (and atomically) clear the tag. For example, this prevents arbitrary data received over the network from ever being directly dereferenced as a pointer.
...
Bounds on Pointers Capabilities contain lower and upper bounds for each pointer; while the pointer may move out of bounds (and back in again), attempts to dereference an out-of-bounds pointer will throw a hardware exception
...
Bounds originate in allocation events. The operating system places bounds on pointers ...as new address-space mappings are made available (e.g., via mmap sys- tem calls).
...
Permissions on Pointers Capabilities extend pointers with a permissions mask controlling how a pointer may be used; for example, the compiler may set the permissions so that pointers to data cannot be reused as code pointers, 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 code and data pointers cannot be loaded from character strings.
Permissions can also be made accessible to higher-level aspects of the runtime and programmer model, offering dynamic enforcement of concepts similar to const.
...
The C-language const qualifier conflates several orthogonal properties and thus can not be enforced auto- matically. Our language extensions include more constrained __input and __output qualifiers.
...
Permissions, as with bounds, are linked to allocation events. Initial permissions for memory mappings will be introduced by the kernel via process startup and as new memory mappings are introduced. The run-time linker will be responsible for creating hierarchies of executable capabilities representing code pointers, from which (implicitly), other forms of runtime ad- dresses will be derived, such as return addresses. Read-only and readable/writable capabilities will originate with the run-time linker, heap allocator, and stack allocator. A separate hierarchy of type capabilities, used in sealing, will likely be provided independently via a system-call in- terface, to prevent arbitrary code and data capabilities being used for this purpose
...
Capability Monotonicity via Guarded Manipulation A new capability can be derived from another capability only via valid manipulations that may narrow (but never broaden) rights ascribed to the new capability. This property of capability monotonicity
...
Sealed Capabilities Capability sealing allows capabilities to be marked as immutable and non-dereferenceable , causing hardware exceptions to be thrown if attempts are made to modify or dereference them, or to jump to them. This enables capabilities to be used as unforgeable tokens of authority for higher-level software constructs grounded in encapsulation , while still allowing them to fit within the pointer-centric framework offered by CHERI capabilities. Sealed capabilities are the foundation for building the CheriBSD? object-capability model supporting in-address-space compartmentalization; they can also be used to support other operating-system or language robustness features, such as representing other sorts of delegated (non-hardware-defined) rights, or ensuring that pointers are dereferenced only by suitable code.
Capability Object Types Sealed capabilities contain an additional piece of metadata, an object type , set when a memory capability undergoes sealing. Object types allow multiple sealed capabilities to be indelibly (and indivisibly) linked, so that the kernel or language runtime can avoid expensive checks (e.g., via table lookups) to confirm that they are intended to be used together. For example, for object-oriented compartmentalization models (such as the CheriBSD? object-capability model), pairs of sealed capabilities represent objects: one as the code capability for a class, and the other a data capability representing the data associated with a particular instance of an object. In the CheriBSD? model, these two sealed capabilities have the same value in their object-type field, and two candidate capabilities passed to object invocation will not be accepted together if their object types do not match. The object-type field is set based on a second input capability authorizing use of the type space – itself simply a hardware permission authorizing sealing within a range of values speci- fied by the capability’s bounds. A similar model authorizes unsealing , which permits a sealed capability to be restored to a mutable and dereferenceable state – if a suitable capability to have sealed it is held. This is used in the CheriBSD?