Capability Distribution Language tools for seL4
Home Page: https://sel4.systems
Collection of tools for generating, parsing and loading capdl specifications of systems:
If you believe you have found a security vulnerability in this code, we ask you to follow the seL4 vulnerability disclosure policy.
parse-capDL --dot ...creates invalid dot file. Seems the problem is, that there are lines containing a quoted filename within a quoted string, which dot can't process.
"frame_ticker_group_bin_0000" [label = "{<Object> frame_ticker_group_bin_0000 \n frame (64k, fill: [{0 65536 CDL_FrameFill_FileData "ticker_group_bin" 0}])}"];
The inner quotes must be escaped as \".
The capdl_spec.c file is generated by capDL-tool and is compiled into the capdl-loader-app program to define the system that the loader will load. The file is supposed to only be a C-language representation of the capDL spec for a particular system.
Currently, the header files required to compile this spec file introduces dependencies on a C library, and libraries from seL4/util_libs and seL4/sel4_libs including libsel4utils and libutils (and any libraries they depend on).
The spec itself doesn't inherently require any type definitions other than what's provided by libsel4, and so it shouldn't require these additional dependencies.
The file generated by the capDL-tool only has the following header file dependencies:
capdl_spec.h:
#include <capdl.h>
#include <sel4/sel4.h>capdl.h:
#include <autoconf.h>
#include <capdl_loader_app/gen_config.h>
#include <sel4/types.h>
// These should all be removed
#include <sel4utils/mapping.h>
#include <limits.h>
#include <stdbool.h>
#include <stdlib.h>
#include <utils/util.h>These are the following non-libsel4 types in the capDL spec and how they can be replaced:
uint8_t -> seL4_Uint8bool -> seL4_Booluint64_t -> seL4_Uint64size_t -> seL4_Word (All usages of size_t are for non-negative integers and so unsigned long is safe)uint32_t -> seL4_Uint32seL4_ARCH_VMAttributes -> unsigned (The CDL_Cap struct definition uses an unsigned 3 bitfield definition already.)In addition some constructions the spec uses can be manually defined:
#include <sel4/bootinfo_types.h>
#define BIT(x) (1lu << x)
#define PACKED __attribute__((packed))
#if defined(CONFIG_ARCH_ARM)
#define CDL_VM_CacheEnabled seL4_ARM_Default_VMAttributes
#define CDL_VM_CacheDisabled 0
#elif defined (CONFIG_ARCH_X86)
#define CDL_VM_CacheEnabled seL4_X86_Default_VMAttributes
#define CDL_VM_CacheDisabled seL4_X86_CacheDisabled
#elif defined (CONFIG_ARCH_RISCV)
#define CDL_VM_CacheEnabled seL4_RISCV_Default_VMAttributes
#define CDL_VM_CacheDisabled 0
#else
#error "Unsupported architecture"
#endif
And a small update to the capDL-tool's C generation:
diff --git a/capDL-tool/CapDL/PrintC.hs b/capDL-tool/CapDL/PrintC.hs
index 290b1c8..c058176 100644
--- a/capDL-tool/CapDL/PrintC.hs
+++ b/capDL-tool/CapDL/PrintC.hs
@@ -142,7 +142,7 @@ showCap objs (FrameCap id rights _ cached maybe_mapping) _ is_orig _ =
", .is_orig = " ++ is_orig ++
", .rights = " ++ showRights rights ++
", .vm_attribs = " ++
- (if cached then "seL4_ARCH_Default_VMAttributes" else "CDL_VM_CacheDisabled") ++
+ (if cached then "CDL_VM_CacheEnabled" else "CDL_VM_CacheDisabled") ++
", .mapping_container_id = " ++
(case maybe_mapping of
Just (mapping_container, _) -> showObjID objs mapping_container;
@@ -216,7 +216,7 @@ showSlots objs obj_id (x:xs) irqNode cdt ms =
where
index = fst x
slot = showCap objs (snd x) irqNode is_orig ms
- is_orig = if Map.notMember (obj_id, index) cdt then "true" else "false"
+ is_orig = if Map.notMember (obj_id, index) cdt then "1" else "0"
memberSlots :: Map ObjID Int -> ObjID -> CapMap Word -> IRQMap -> CDT -> ObjMap Word -> String
memberSlots objs obj_id slots irqNode cdt ms =
@@ -451,7 +451,7 @@ showUntypedDerivations :: AllocationType -> Map ObjID Int -> CoverMap -> String
showUntypedDerivations DynamicAlloc{} _ untypedCovers
| all null (Map.elems untypedCovers) =
".num_untyped = 0," +++
- ".untyped = NULL,"
+ ".untyped = 0,"
| otherwise = error $
"refusing to generate spec for dynamic allocation because the " ++
"following untypeds already have children:\n" ++
I'm trying to set the stack, but I get the following error
$ cd tools/capDL
$ make sandbox
stack setup
No information found for ghc-8.0.1.
Supported versions for OS key 'linux64-nopie': GhcVersion 8.0.2, GhcVersion 8.2.1, GhcVersion 8.2.2
Makefile:37: recipe for target 'sandbox' failed
make: *** [sandbox] Error 1
do branch maintenance (update/delete):
The python-capdl-tool uses the package nose for running its (small) test suite. This package is now unmaintained, and as of python 3.10 does not work any more for python-capdl-tool.
This issue is to replace nose with something more recent such as pytest.
PR #30 is temporarily switching off testing on python 3.10, but this is a stop-gap only. As time goes on python >= 3.10 will become the default.
I'm not familiar with Haskell but I would think that it supports compiling static binaries. I tried to do so with stack build --fast --ghc-options '-optl-static' and it resulted in:
Building all executables for `capDL-tool' once. After a successful build of all of them, only specified executables will be rebuilt.
capDL-tool> configure (exe)
Configuring capDL-tool-1.0.0.1...
capDL-tool> build (exe)
Preprocessing executable 'parse-capDL' for capDL-tool-1.0.0.1..
Building executable 'parse-capDL' for capDL-tool-1.0.0.1..
[ 1 of 17] Compiling CapDL.Matrix
[ 2 of 17] Compiling CapDL.Model
[ 3 of 17] Compiling CapDL.AST
[ 4 of 17] Compiling CapDL.ParserUtils
[ 5 of 17] Compiling CapDL.Parser
[ 6 of 17] Compiling CapDL.DumpParser
[ 7 of 17] Compiling CapDL.STCC
[ 8 of 17] Compiling CapDL.State
[ 9 of 17] Compiling CapDL.PrintUtils
[10 of 17] Compiling CapDL.PrintXml
[11 of 17] Compiling CapDL.PrintModel
[12 of 17] Compiling CapDL.PrintJSON
[13 of 17] Compiling CapDL.PrintDot
[14 of 17] Compiling CapDL.PrintC
[15 of 17] Compiling CapDL.PrintIsabelle
[16 of 17] Compiling CapDL.MakeModel
[17 of 17] Compiling Main
Linking .stack-work/dist/x86_64-linux/Cabal-3.6.3.0/build/parse-capDL/parse-capDL ...
/usr/lib/gcc/x86_64-linux-gnu/12/../../../x86_64-linux-gnu/libc.a(pthread_cond_broadcast.o)(.note.stapsdt+0x14): error: relocation refers to local symbol "" [1], which is defined in a discarded section
/usr/lib/gcc/x86_64-linux-gnu/12/../../../x86_64-linux-gnu/libc.a(pthread_cond_destroy.o)(.note.stapsdt+0x14): error: relocation refers to local symbol "" [1], which is defined in a discarded section
/usr/lib/gcc/x86_64-linux-gnu/12/../../../x86_64-linux-gnu/libc.a(pthread_cond_init.o)(.note.stapsdt+0x14): error: relocation refers to local symbol "" [1], which is defined in a discarded section
/usr/lib/gcc/x86_64-linux-gnu/12/../../../x86_64-linux-gnu/libc.a(pthread_cond_signal.o)(.note.stapsdt+0x14): error: relocation refers to local symbol "" [1], which is defined in a discarded section
/usr/lib/gcc/x86_64-linux-gnu/12/../../../x86_64-linux-gnu/libc.a(pthread_cond_wait.o)(.note.stapsdt+0x14): error: relocation refers to local symbol "" [1], which is defined in a discarded section
/usr/lib/gcc/x86_64-linux-gnu/12/../../../x86_64-linux-gnu/libc.a(pthread_cond_wait.o)(.note.stapsdt+0x60): error: relocation refers to local symbol "" [1], which is defined in a discarded section
/usr/lib/gcc/x86_64-linux-gnu/12/../../../x86_64-linux-gnu/libc.a(pthread_cond_wait.o)(.note.stapsdt+0xac): error: relocation refers to local symbol "" [1], which is defined in a discarded section
/usr/lib/gcc/x86_64-linux-gnu/12/../../../x86_64-linux-gnu/libc.a(pthread_join_common.o)(.note.stapsdt+0x14): error: relocation refers to local symbol "" [1], which is defined in a discarded section
/usr/lib/gcc/x86_64-linux-gnu/12/../../../x86_64-linux-gnu/libc.a(pthread_join_common.o)(.note.stapsdt+0x5c): error: relocation refers to local symbol "" [1], which is defined in a discarded section
/usr/lib/gcc/x86_64-linux-gnu/12/../../../x86_64-linux-gnu/libc.a(pthread_mutex_cond_lock.o)(.note.stapsdt+0x14): error: relocation refers to local symbol "" [1], which is defined in a discarded section
/usr/lib/gcc/x86_64-linux-gnu/12/../../../x86_64-linux-gnu/libc.a(pthread_mutex_cond_lock.o)(.note.stapsdt+0x5c): error: relocation refers to local symbol "" [1], which is defined in a discarded section
/usr/lib/gcc/x86_64-linux-gnu/12/../../../x86_64-linux-gnu/libc.a(pthread_mutex_cond_lock.o)(.note.stapsdt+0xa0): error: relocation refers to local symbol "" [1], which is defined in a discarded section
/usr/lib/gcc/x86_64-linux-gnu/12/../../../x86_64-linux-gnu/libc.a(pthread_mutex_destroy.o)(.note.stapsdt+0x14): error: relocation refers to local symbol "" [1], which is defined in a discarded section
/usr/lib/gcc/x86_64-linux-gnu/12/../../../x86_64-linux-gnu/libc.a(pthread_mutex_init.o)(.note.stapsdt+0x14): error: relocation refers to local symbol "" [1], which is defined in a discarded section
collect2: error: ld returned 1 exit status
`gcc' failed in phase `Linker'. (Exit code: 1)
Error: [S-7282]
Stack failed to execute the build plan.
While executing the build plan, Stack encountered the following errors:
[S-7011]
While building package capDL-tool-1.0.0.1 (scroll up to its section to see the error) using:
/home/ivanv/.stack/setup-exe-cache/x86_64-linux/Cabal-simple_SvXsv1f__3.6.3.0_ghc-9.2.8 --verbose=1 --builddir=.stack-work/dist/x86_64-linux/Cabal-3.6.3.0 build exe:parse-capDL --ghc-options " -fdiagnostics-color=always"
Process exited with code: ExitFailure 1
If someone familiar with the tool or Haskell could help that would be great. I cannot find any documentation for building a static binary with stack.
I notice that in
capdl/python-capdl-tool/capdl/Object.py
Lines 375 to 395 in f7ef9ca
fault_ep_slot in the capDL spec generated can be anything.
However, I notice in the capDL initialiser in this repository:
capdl/capdl-loader-app/src/main.c
Line 1044 in f7ef9ca
It is expecting that the fault endpoint is in a specific slot.
Is this a restriction of the initialiser itself or of CapDL in general?
I'm a but confused about what commit e08dbb4 added. Looking at
capdl/capdl-loader-app/include/capdl.h
Lines 169 to 185 in e082ee7
CONFIG_VTX within a CONFIG_ARCH_ARM block. Looks to me as if CDL_VCPU is never declared on CONFIG_ARCH_X86 at all then?I'm getting this warning when compiling a CAmkES system for RISC-V rv32 (spike):
Building C object .../capdl/capdl-loader-app/src/main.c.obj
.../capdl/capdl-loader-app/src/main.c: In function 'init_level_1':
.../capdl/capdl-loader-app/src/main.c:1565:51: warning: left shift count >= width of type [-Wshift-count-overflow]
1565 | uintptr_t base = level_1_base + (obj_slot << (CDL_PT_LEVEL_2_IndexBits + CDL_PT_LEVEL_3_IndexBits + seL4_PageBits));
| ^~
.../capdl/capdl-loader-app/src/main.c: In function 'init_level_0':
.../capdl/capdl-loader-app/src/main.c:1585:52: warning: left shift count >= width of type [-Wshift-count-overflow]
1585 | uintptr_t base = (level_0_base + obj_slot) << (CDL_PT_LEVEL_1_IndexBits + CDL_PT_LEVEL_2_IndexBits +
| ^~
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
Django
The Web framework for perfectionists with deadlines.
Laravel
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
Microsoft
Open source projects and samples from Microsoft.
Google
Google ❤️ Open Source for everyone.
Alibaba
Alibaba Open Source for everyone
D3
Data-Driven Documents codes.
Tencent
China tencent open source team.