FAQ: sealed capabilities

faq/compiling.rst

@@ -8,29 +8,79 @@ Cross-compilation
 =================
 
 The LLVM compiler runs in cross-compilation mode for CHERI, so you can compile to CHERI targets from a non-CHERI platform like x86_64/linux.
-If you use cheribuild, then by default your CHERI LLVM toolchain will be
-located in the `cheri` directory in your home directory. There is a
-configuration file with the relevant parameters set up to enable cross-compilation. One convenient way to
-invoke the cross-compiler is by defining appropriate environment variables:
 
-.. code-block:: bash
+- If you use cheribuild, then by default your CHERI LLVM toolchain will be
+   located in the `cheri` directory in your home directory. There is a
+   configuration file with the relevant parameters set up to enable cross-compilation. One convenient way to
+   invoke the cross-compiler is by defining appropriate environment variables:
 
-   export CC=~/cheri/output/morello-sdk/bin/clang
-   export CFLAGS="--config cheribsd-morello-purecap.cfg"
+  .. code-block:: bash
 
-You can then invoke the cross-compiler on your non-CHERI platform:
+    export CC=~/cheri/output/morello-sdk/bin/clang
+    export CFLAGS="--config cheribsd-morello-purecap.cfg"
 
-.. code-block:: bash
+  You can then invoke the cross-compiler on your non-CHERI platform:
+
+  .. code-block:: bash
+
+    $CC $CFLAGS test.c
+
+  which will generate an `a.out` executable file that you can copy to a
+  CHERI system to execute.
+
+  Cross-compilation is most useful when you are running a CHERI emulator and
+  the native CHERI compiler runs too slowly on the emulator.
+
+- You can also use some non-official MorelloIE Docker images, such as ``cocoaxu/morelloie-llvm``
+  and ``cocoaxu/morelloie-gcc``. They contain the LLVM-toochain and GCC-toolchain for CHERI, 
+  respectively. You can use them to compile your CHERI programs on your non-CHERI platform.
+
+  Meanwhile, you can also use the ``--volume`` option to mount your source code directory
+  into the container. For example, if your source code is in ``/home/user/src``, you can do
+  the following:
+
+  .. code-block:: shell
+
+    # using LLVM toolchain with musl libc
+    $ docker run -it --rm --volume /home/user/src:/src cocoaxu/morelloie-llvm
+
+    # using GCC toolchain with glibc
+    $ docker run -it --rm --volume /home/user/src:/src cocoaxu/morelloie-gcc
+
+  Then you can compile your CHERI programs inside the container. Inside these Docker images,
+  they both have ``morelloie`` pre-installed while the CHERI compiler is ``clang`` and ``gcc``,
+  respectively. 
+
+  And for the LLVM toolchain specificly, a sysroot directory for Purecap can be found at 
+  ``/root/musl-sysroot-purecap``, which can be used later when compiling Purecap Morello programs
+  with ``clang``.
+
+  - If you're using the LLVM Docker image, ``cocoaxu/morelloie-llvm``, then the 
+    CHREI compiler is ``clang``, and we need to specify the target as 
+    ``aarch64-linux-musl_purecap`` and the sysroot as ``/root/musl-sysroot-purecap``:
+
+  .. code-block:: shell
+
+    $ clang -march=morello \
+      --target=aarch64-linux-musl_purecap \
+      --sysroot=/root/musl-sysroot-purecap \
+      test.c -o test -static
+
+
+  - If you're using the GCC Docker image, ``cocoaxu/morelloie-gcc``, then we can compile
+    the program with ``gcc`` and we don't need to specify the target or sysroot:
+
+    .. code-block:: shell
 
-   $CC $CFLAGS test.c
+      $ gcc -march=morello+c64 -mabi=purecap \
+        test.c -o test -static
 
-which will generate an `a.out` executable file that you can copy to a
-CHERI system to execute.
 
-Cross-compilation is most useful when you are running a CHERI emulator and
-the native CHERI compiler runs too slowly on the emulator.
+  After the compilation, you need to run the program with ``morelloie``. For example:
 
+  .. code-block:: shell
 
+    $ morelloie -- ./test
 
 
 Native compilation

faq/index.rst

@@ -9,7 +9,8 @@ when working with CHERI software?
 .. toctree::
    :maxdepth: 1
 
-   what_is_a_capability      
+   what_is_a_capability_short_answer
+   what_is_a_capability_long_answer
    get_a_board
    compiling
    configure_networking
@@ -20,6 +21,7 @@ when working with CHERI software?
    installing_gdb
    printf
    purecap_or_hybrid_binary
+   sealed_capabilities
    purposes_of_sealed_capabilities
    python
    running

faq/sealed_capabilities.rst

@@ -0,0 +1,161 @@
+===========================
+What is a Sealed Capability
+===========================
+
+This post serves as the second part of the previous post `What is a Capability <https://capabilitiesforcoders.com/faq/capabilities.html>`_,
+and in this post, we will talk about what a sealed capability is in CHERI. Also,
+we will explain sealed capabilities using the example program in the previous post,
+so if you haven't read the previous post, please read it first.
+
+Before we dive into the details of these capabilities in the ``func`` program in the previous post,
+let's talk about what a sealed capability is. In CHERI and Morello, a capability can be sealed,
+and in simple words, a sealed capability is a capability with a non-zero object type.
+
+The object type is a 16-bit field in Morello, and there're 4 special values for the object type:
+
+- ``0x0000``: the capability is not sealed.
+- ``0x0001``: the capability is RB-sealed and used for all conventional register branch.
+- ``0x0002``: the capability is LPB-sealed, which is used for load pair and branch operations (relevant to compartments).
+- ``0x0003``: the capability is LB-sealed and used for load and branch operations (relevant to compartments).
+
+The RB-, LPB- and LB-sealed capabilities are also referred to as "fixed" or "hardware" types.
+
+There are 4 consequences for sealing a capability:
+
+- Once the capability is sealed, it will be immutable. Any operations that modify the capability
+  will result in an invalid capability.
+- A sealed capability cannot be dereferenced, that is, we cannot read or write the memory that
+  the capability points to.
+- Also, branching to an executable but sealed capability will fault. Notice RB-, LPB- and LB-sealed
+  capabilities will be automatically unsealed during the corresponding branch operation.
+- Lastly, a sealed capability cannot be used to seal another capability even when meeting all other
+  requirements for a sealing capability.
+
+There are also other values for the object type, which are used for sealing capabilities, but we
+will not cover them here. 
+
+RB-sealed Capabilities
+----------------------
+
+If we break at the ``printf`` function in the example above and as ``cap1`` is the second parameter 
+for ``printf``, it's stored in the register ``c1``. Hence we can do ``p c1`` to inspect the first 
+capability, ``cap1``, in the debugger:
+
+.. code-block:: shell
+
+    $ morelloie -break printf -- ./func
+    /* next instruction (211c18:printf) */
+    /* 211c18 0280c3ff sub     csp, csp, #48, lsl #0 */
+    [281:211c18] p c1
+    c1 = 0x1:b090c000:8d9f0044:00000000:00211545
+              tag: true
+          address: 0x00000000000211545
+             base: 0x00000000000200200
+            limit: 0x00000000000226cc0
+           bounds: valid
+        in bounds: true
+           length: 158400
+           offset: 70469
+      permissions: GrRM---xES--------
+           sealed: sealed RB (1)
+    ...
+    [281:211bec] c
+    0x211545 [rxRE,0x200200-0x226c80] (sentry)
+
+
+The output shows that if we take the address of a function, it will result in a RB-sealed
+capability (``sealed RB (1)``). And the sentry keyword outputted by printf also suggested 
+that what we see is an executable capability that is sealed with the RB object type.
+
+The second capability ``cap2`` is invalid because it was created by adding 1 to the first
+capability ``cap1``, and once we do any arithmetic operations on a sealed capability, the
+resulting capability will be invalid, as shown in the output above (``(sentry, invalid)``).
+If we try to print the second capability ``cap2`` in the debugger, we will get the following
+output:
+
+.. code-block:: shell
+
+    $ morelloie -break printf -- ./func
+    ...
+    [293:211bc8] p c1
+    c1 = 0x1:dc104000:5f40df30:0000ffff:f063df30
+              tag: true
+          address: 0x00000fffff063df30
+             base: 0x00000fffff063df30
+            limit: 0x00000fffff063df40
+           bounds: valid
+        in bounds: true
+           length: 16
+           offset: 0
+      permissions: GrRMwWL-----------
+           sealed: (not sealed)
+    ...
+    [293:211bc8] c
+    0x211546 [rxRE,0x200200-0x226c40] (invalid,sentry)
+
+
+Notice that the second capability ``cap2`` is not sealed anymore, and its permissions have
+also changed. It's no longer executable, meaning that we cannot jump right in the middle
+of the function ``func``. In this way, we can 
+
+Another example is the capability holding return address (link register), which is the register
+``c30``. If we break at the ``printf`` function and inspect the capability holding the return
+address, we will get the following output:
+
+.. code-block:: shell
+
+    $  morelloie -break printf -- ./func
+    /* next instruction (211bc8:printf) */
+    /* 211bc8 0280c3ff sub     csp, csp, #48, lsl #0 */
+    [294:211bc8] p clr
+    clr = 0x1:b090c000:8d8f0044:00000000:0021159d
+              tag: true
+          address: 0x0000000000021159d
+             base: 0x00000000000200200
+            limit: 0x00000000000226c40
+           bounds: valid
+        in bounds: true
+           length: 158272
+           offset: 70557
+      permissions: GrRM---xES--------
+           sealed: sealed RB (1)
+    ...
+
+
+The output shows that the return address is also a RB-sealed capability. This means that
+the return address is also protected by the sentry. If we try to modify the return address,
+the program will crash. And this is how Morello protects the control flow of a program.
+
+LPB- and LB-sealed Capabilities
+-------------------------------
+
+For LPB- and LB-sealed capabilities, they are used for load pair and branch operations. In
+order to create a LPB- or LB-sealed capability, we need to use inline assembly for this:
+
+.. code-block:: C
+
+    inline __attribute__ ((naked))
+    void *__morello_seal_lpb(void *cap)
+    {
+        void *ret;
+        __asm__ ("seal %0, %1, lpb" : "=C"(ret) : "C"(cap));
+        return ret;
+    }
+
+    inline __attribute__ ((naked))
+    void *__morello_seal_lb(void *cap)
+    {
+        void *ret;
+        __asm__ ("seal %0, %1, lb" : "=C"(ret) : "C"(cap));
+        return ret;
+    }
+
+
+The ``seal`` instruction is used to seal a capability. The first operand is the destination
+register, and the second operand is the source register. The third operand is the sealing
+type, which can be ``lpb`` or ``lb``. These sealing types are used for sealing a capability 
+with the LPB and LB object types, respectively.
+
+You can read the `["Hello World" Example] <https://capabilitiesforcoders.com/compartmentalisation/index.html#morello-compartmentalisation>`_
+in the Morello Compartmentalisation section. It shows how to use LPB- and LB-sealed capabilities
+to compartmentalise a program.