I've been investigating how capd-loader works and have some questions. My
apologies if these were previously discussed.
1. CDL_Model is mutable. The capDL specification looks like a perfect
candidate for being in .rodata but it's stored+treated as mutable. Why? I
see capdl-loader uses the mutability to store mapped page frame caps and,
for risc-v, VSpace roots, but both can be easily handled w/o modifying the
spec. Having this immutable has many benefits.
2. All page frames are treated as shared. CAPDL_SHARED_FRAMES is #define'd
in the code so every frame is treated as shared. This inflates the size of
the orig_caps array and the kernel capabilities table but seems
unnecessary. Why? I've verified that instead of doing the Copy op on each
page you can just check the return of the seL4_Page_Map call and if
necessary clone the cap. Better would be for camkes to identify shared page
frames so this doesn't require 2x syscalls (which spam's the console w/
CONFIG_PRINTING enabled).
3. Why does copy_addr_with_pt exist? There are two memory regions created
for mapping page frames into the rootserver address space for doing fill
ops. One is 64KB and the other is 1 page (nominally 4KB). init_frame tries
the 4KB region first then falls back to the 64K region if mapping into the
4KB region fails. Why (i.e. why would the 1st mapping call fail)? On my
risc-v system I never use the 64K region and I'm not sure when it might be
used? Even if it were used, why is 64K always allocated; seems like the
region should be sized according to the target platform. Having this extra
region has a cost that can be significant on small systems.
4. console output. Why is sel4_DebugPutChar (or similar) not a standard
part of the kernel? This forces capdl-loader to depend on
libsel4platsupport for console output which in turn affects cap space. I
can't imagine an seL4 system that cannot write to the console and I think
it's entirely reasonable to have a critical system service like the
rootserver use that.
5. duplicate_caps. The scheme for constructing a running system from a
spec is straightforward except for duplicating caps. Why are all TCB's and
CNode caps dup'd? Why does init_tcbs call init_tcb on the original object
but immediately configure_tcb on the dup? There are other places where the
dup cap is used instead of the original cap (e.g. init_cnode_slot). None of
this seems to matter on risc-v; maybe this matters on some other
architectures?
6. On risc-v all pages appear to be marked executable--including ipc
buffers! This seems just wrong and a potential security hole.
7. Why does seL4_TCB_WriteRegisters take a _mutable_ seL4_UserContext? I'm
guessing this is a mistake in the xml spec (but haven't looked).
8. init_cspaces mystifies me. There are two loops over all CNodes; one that
does "COPY" operations and one that does "MOVE" operations. I see nothing
explaining what's happening. I've read this code many times and still don't
get it; please explain.
9. According to comments, the use of a global static to setup the
UserContext for a new TCB is done because one cannot take the address of a
local variable. On what architecture is this true? On risc-v the context is
copied into "registers" before calling the kernel so this doesn't appear to
be an issue with crossing the user-kernel protection boundary.
10. Memory reclamation. I'm unclear what happens to the memory used by
capdl-loader. The process does a TCB_Suspend call when it's done. Does this
cause the CSpace & VSpace to be reclaimed? For CAmkES this doesn't matter
as there's no support for allocating memory but I'm building a system where
this isn't true. How do I release memory (in particular) back to the
untyped pool?
I have a bunch of niggly code complaints/questions but let's start with the
above.
-Sam
Hello all,
I recently spent a lot of time getting the camkes-vm-linux tutorial to
work, because it is the only example I could find of compiling a kernel
module for the linux vm as a part of the camkes build process.
Unfortunately, the kernel module doesn't seem to work. For more
information, see the previous email chain as well as
https://github.com/NeisesResearch/vm_measure/wiki/Building-the-camkes_vm_li…
.
In lieu of doing things the right way, I believe I could compile a kernel
module for the linux kernel that is provided as part of the camkes build
system. I believe this is how the introspect-app accomplishes its work.
However, I need to have the exact kernel and exact configuration in order
to compile the kernel module correctly.
Can anyone point me to the correct kernel version and configuration, so
that I can target the provided linux kernel for module compilation?
Or if there's a better way to get a kernel module in there, please let me
know.
Cheers,
Michael Neises
Hi:
In our ARMv8 platform，we access secure world not only from the VM guest OS， but also form native compont like config clk register
In ARMv8 platform, SMC instructions are not allowed from EL0.
So in camkes-vm project, I create a new smc capability and a new syscall as a temporary solution, like below:
"LIBSEL4_INLINE seL4_ARM_SMC_CallFunc_t seL4_ARM_SMC_CallFunc(seL4_ARM_SMC _service, seL4_Word function_id, seL4_Word arg0, seL4_Word arg1, seL4_Word arg2)"
But I did not pay much attention to security, it is just meet our current work.
I didnot really understand the essence of kernel whitelist mentioned by "https://sel4.atlassian.net/browse/RFC-9"? I have some question below, I feel the smc cap should like schedcontrol cap belong every core.
1. what is the whiltelist describe ? sip command smc function id?
2. how are the members of whilelist represented in the kernel , check the invLabel of syscall in kernel if we provide one smc cap not every function id? or just check the range of function id ?
3. Does each TCB have its own whitelist or does the entire system have a whitelist?
thank you very much.
-----邮件原件-----
发件人: devel-request(a)sel4.systems [mailto:devel-request@sel4.systems]
发送时间: 2021年11月10日 9:00
收件人: devel(a)sel4.systems
主题: Devel Digest, Vol 124, Issue 1
Send Devel mailing list submissions to
devel(a)sel4.systems
To subscribe or unsubscribe via email, send a message with subject or body 'help' to
devel-request(a)sel4.systems
You can reach the person managing the list at
devel-owner(a)sel4.systems
When replying, please edit your Subject line so it is more specific than "Re: Contents of Devel digest..."
Today's Topics:
1. RFC-9: new capability for seL4 SMC Forwarding on Arm
(Gerwin Klein)
----------------------------------------------------------------------
Message: 1
Date: Tue, 9 Nov 2021 21:52:58 +0000
From: Gerwin Klein <kleing(a)unsw.edu.au>
Subject: [seL4] RFC-9: new capability for seL4 SMC Forwarding on Arm
To: devel <devel(a)sel4.systems>
Message-ID: <613858AC-3DB1-4D7C-A892-9ABDB5B31D58(a)unsw.edu.au>
Content-Type: text/plain; charset="utf-8"
I’d like to solicit discussion on the new RFC on forwarding Secure Monitor Calls on Arm:
https://sel4.atlassian.net/browse/RFC-9
Relevant Arm documentation (SMC calling conventions):
https://developer.arm.com/documentation/den0028/latest?_ga=2.116565828.3903…
Any opinions, concerns, alternative designs?
Cheers,
Gerwin
------------------------------
Subject: Digest Footer
_______________________________________________
Devel mailing list -- devel(a)sel4.systems To unsubscribe send an email to devel-leave(a)sel4.systems
------------------------------
End of Devel Digest, Vol 124, Issue 1
*************************************
-----邮件原件-----
发件人: devel-request(a)sel4.systems [mailto:devel-request@sel4.systems]
发送时间: 2021年11月18日 5:56
收件人: devel(a)sel4.systems
主题: Devel Digest, Vol 125, Issue 2
Send Devel mailing list submissions to
devel(a)sel4.systems
To subscribe or unsubscribe via email, send a message with subject or body 'help' to
devel-request(a)sel4.systems
You can reach the person managing the list at
devel-owner(a)sel4.systems
When replying, please edit your Subject line so it is more specific than "Re: Contents of Devel digest..."
Today's Topics:
1. Re: some question about seL4 performance (Gerwin Klein)
2. Re: some question about seL4 performance (Gernot Heiser)
3. Re: some question about seL4 performance (Gerwin Klein)
----------------------------------------------------------------------
Message: 1
Date: Wed, 17 Nov 2021 21:24:57 +0000
From: Gerwin Klein <kleing(a)unsw.edu.au>
Subject: [seL4] Re: some question about seL4 performance
To: yadong.li <yadong.li(a)horizon.ai>
Cc: "devel(a)sel4.systems" <devel(a)sel4.systems>
Message-ID: <CA210292-C334-42C1-9FB4-48CAFDE8CCC6(a)unsw.edu.au>
Content-Type: text/plain; charset="utf-8"
> On 18 Nov 2021, at 02:06, yadong.li <yadong.li(a)horizon.ai> wrote:
>
> Hi：
> I learn the sel4 performance form
> https://sel4.systems/About/Performance/
> I focus on the ARMv8 platform, from the website, the parameters are as follows:
> ISA Mode Core/SoC/Board Clock IRQ Invoke IPC call IPC reply
> "Armv8a 64 A57/Tx1/Jetson 1.9 GHz 863 (18) 396(15) 397(4)"
>
> I want to know what is the length of IPC for the record provided on the web page , when test IPC call and reply? 0 or 10?
The page reports the 0-length numbers. The idea is that IPC should fit into registers, the 10 case is the one that make it spill into memory deliberately. That number is good to know for development, but should not be the main performance characteristic.
Cheers,
Gerwin
------------------------------
Message: 2
Date: Wed, 17 Nov 2021 21:36:39 +0000
From: Gernot Heiser <gernot(a)unsw.edu.au>
Subject: [seL4] Re: some question about seL4 performance
To: "devel(a)sel4.systems" <devel(a)sel4.systems>
Message-ID: <9885F4AB-61C0-46CD-B239-595E38482673(a)unsw.edu.au>
Content-Type: text/plain; charset="utf-8"
On 18 Nov 2021, at 08:24, Gerwin Klein <kleing(a)unsw.edu.au> wrote:
>
> The page reports the 0-length numbers. The idea is that IPC should fit into registers, the 10 case is the one that make it spill into memory deliberately. That number is good to know for development, but should not be the main performance characteristic.
Note that whether data is transferred solely in registers or using a memory buffer does not make a big difference on contemporary hardware. However, our present implementation reverts to the slow path as soon as the message size overflows the physical message registers, which will make the PIC much slower.
This is something that could be fixed by widening the fastpath conditions without much complications. However, we haven’t yet come across an important use case where this matters, so there isn’t much motivation for investing time in it.
Gernot
------------------------------
Message: 3
Date: Wed, 17 Nov 2021 21:56:06 +0000
From: Gerwin Klein <kleing(a)unsw.edu.au>
Subject: [seL4] Re: some question about seL4 performance
To: Gernot Heiser <gernot(a)unsw.edu.au>
Cc: "devel(a)sel4.systems" <devel(a)sel4.systems>
Message-ID: <FFD95815-9F62-4A90-A3D0-59671152494D(a)unsw.edu.au>
Content-Type: text/plain; charset="us-ascii"
On 18 Nov 2021, at 08:36, Gernot Heiser <gernot(a)unsw.edu.au<mailto:gernot@unsw.edu.au>> wrote:
On 18 Nov 2021, at 08:24, Gerwin Klein <kleing(a)unsw.edu.au<mailto:kleing@unsw.edu.au>> wrote:
The page reports the 0-length numbers. The idea is that IPC should fit into registers, the 10 case is the one that make it spill into memory deliberately. That number is good to know for development, but should not be the main performance characteristic.
Note that whether data is transferred solely in registers or using a memory buffer does not make a big difference on contemporary hardware. However, our present implementation reverts to the slow path as soon as the message size overflows the physical message registers, which will make the PIC much slower.
Yes I should have mentioned that. If you look at the raw numbers for x86, eg. at https://github.com/seL4/sel4bench/actions/runs/1469475721#artifacts, fast path/no fast path is almost equal for length 10. You get a tiny bit better performance for length 10 when the fast path is switched off completely, because it doesn't first have to test whether to take the fast path or not.
Cheers,
Gerwin
------------------------------
Subject: Digest Footer
_______________________________________________
Devel mailing list -- devel(a)sel4.systems To unsubscribe send an email to devel-leave(a)sel4.systems
------------------------------
End of Devel Digest, Vol 125, Issue 2
*************************************
Hi：
I learn the sel4 performance form https://sel4.systems/About/Performance/
I focus on the ARMv8 platform, from the website, the parameters are as follows:
ISA Mode Core/SoC/Board Clock IRQ Invoke IPC call IPC reply
"Armv8a 64 A57/Tx1/Jetson 1.9 GHz 863 (18) 396(15) 397(4)"
I want to know what is the length of IPC for the record provided on the web page , when test IPC call and reply? 0 or 10?
thank you very much
Hi seL4 devs,
a few of us thought it might be nice to talk more directly from time to time rather than only via pull requests, so we're trialling a seL4 developer hangout/video chat.
The idea for this is to be:
- informal, about 1h
- for technical discussions about seL4 and related repositories
- anyone can join
- every two weeks, initially for 3 times, then we can decide how we like it
At least one or two technical steering committee (TSC) members will try to be at every one of these, but these are not TSC meetings where formal decisions are made, just technical discussions about whatever people have on their minds.
To provide a starting topic, one thing we'd be interested in is:
seL4 boot code
There have been quite a few pull requests in that area, and it'd be nice to know what people's plans are and how we can keep this part of seL4 high assurance while making it more flexible. Other topics for future meetings could be better support for other language bindings (e.g. Rust), any RFCs that are open or people are thinking about opening, or just discussions about current pull requests or issues.
The first hangout is on
- Sydney: Wed, Nov 3, 8am
- Central Europe: Tue, Nov 2, 10pm
- US East Coast: Tue, Nov 2, 2pm
Zoom link: https://unsw.zoom.us/j/82640784431
Cheers,
Gerwin
I am running on an i.MX6 the picoserver app https://github.com/seL4/camkes/tree/master/apps/picoserver
Both the echo and listener components print out to serial:
listener instance starting up, going to be listening on 10.0.0.2:4321
echo instance starting up, going to be listening on 10.0.0.2:1234
but only the echo component receives PicoTCP events:
Assigned ipv4 10.0.0.2 to device eth0
IPv6: DAD verified valid address.
echo: Connection established with 10.0.0.1 on socket 1
echo: Received a message on socket 3, going to echo to Listener
echo: Received a message on socket 3, going to echo to Listener
echo: Received a message on socket 3, going to echo to Listener
Note that the listener component does not even print out "Connection established".
I tried to figure out why, and found out that by editing this part of picoserver.camkes:
/*
* The attributes of the *_(control/send/recv) interfaces should be the same and unique between
* different components, this determines the client ID of this component with respect to
* the PicoServer component
*/
echo.echo_control_attributes = "1";
echo.echo_recv_attributes = "1";
echo.echo_recv_shmem_size = 0x1000;
echo.echo_send_attributes = "1";
echo.echo_send_shmem_size = 0x1000;
echo.ip_addr = PICOSERVER_IP_ADDR;
/*
* Listener config
*/
listener.listener_control_attributes = "2";
listener.listener_recv_attributes = "2";
listener.listener_recv_shmem_size = 0x1000;
listener.listener_send_attributes = "2";
listener.listener_send_shmem_size = 0x1000;
listener.ip_addr = PICOSERVER_IP_ADDR;
and changing the attributes to this:
/*
* The attributes of the *_(control/send/recv) interfaces should be the same and unique between
* different components, this determines the client ID of this component with respect to
* the PicoServer component
*/
echo.echo_control_attributes = "0";
echo.echo_recv_attributes = "0";
echo.echo_recv_shmem_size = 0x1000;
echo.echo_send_attributes = "0";
echo.echo_send_shmem_size = 0x1000;
echo.ip_addr = PICOSERVER_IP_ADDR;
/*
* Listener config
*/
listener.listener_control_attributes = "1";
listener.listener_recv_attributes = "1";
listener.listener_recv_shmem_size = 0x1000;
listener.listener_send_attributes = "1";
listener.listener_send_shmem_size = 0x1000;
listener.ip_addr = PICOSERVER_IP_ADDR;
then listener will print that it has connected to echo, but now echo will not print out anything.
How do I make both echo and listener print out on the serial port?
Which part of the code looks at echo.echo_recv_attributes = "1"; and listener.listener_recv_attributes = "2"; in order to determine the client ID of the echo and listener components with respect the PicoServer component? From what I can tell, attributes was not declared as an actual attribute.
Hello. I've been playing around with the camkes Arm VMM. However, the
meaning of some of the configuration fields is not completely clear to
me. For example:
- what is the difference between "linux_ram_base" and
"linux_ram_paddr_base" in the linux_address_config attribute? Are
these supposed to define the virtual and physical addresses of the
guest's ram region base, respectively? If so, can we have non-identity
mappings by setting them to different values? From my experiments
having different addresses on those does not always work (even if both
are aligned to a 2M superpage boundary) .
- what is the difference between the untyped_mmios and mmios
attributes? They seem to serve pretty similar purposes. For example,
in different vm-examples they are both used for assigning the virtual
gic cpu interface to the guest.
I probably have a few other questions. I couldn't find it, but I was
hoping there was more thorough documentation for the vm configuration
detailing the meaning of these fields (and others)?
Best regards,
José
