3 Nov
2015
3 Nov
'15
11:38 a.m.
Hi,
I have a few questions about network stack in sel4.
Is network stack implemented in the kernel or user level?
If in user level, are different protocols (IP/TCP) implemented in a
single server or different servers?
If in different servers, how do they communicate with each other?
Is there any example code to show how to use network? How to send and
receive TCP or UDP packets?
How can I set up the network environment on bare metal machine? Is
there documentation or instruction?
Thanks a lot!
Yuxin
3 Nov
3 Nov
12:48 p.m.
seL4 does not provide a network stack or even
network device drivers. An OS on top of seL4
would have to provide their own drivers and stack
and is free to put them in a single server or in
different servers and choose how to communicate
between them.
On Mon, Nov 2, 2015 at 2:38 PM, Yuxin Ren <ryx(a)gwmail.gwu.edu> wrote:
Hi,
I have a few questions about network stack in sel4.
Is network stack implemented in the kernel or user level?
If in user level, are different protocols (IP/TCP) implemented in a
single server or different servers?
If in different servers, how do they communicate with each other?
Is there any example code to show how to use network? How to send and
receive TCP or UDP packets?
How can I set up the network environment on bare metal machine? Is
there documentation or instruction?
Thanks a lot!
Yuxin
_______________________________________________
Devel mailing list
Devel(a)sel4.systems
https://sel4.systems/lists/listinfo/devel
12:58 p.m.
So basically L4 grants IO caps to the network card's io ports to whatever
task acts as the network driver, and it's the driver task's job to bang on
the card's I/O and hook up with whatever other tasks represent
packet/protocol/whatever layers of the ISO 7 layer stack.
On Mon, Nov 2, 2015 at 5:48 PM, Tim Newsham <tim.newsham+sel4(a)gmail.com>
wrote:
seL4 does not provide a network stack or even
network device drivers. An OS on top of seL4
would have to provide their own drivers and stack
and is free to put them in a single server or in
different servers and choose how to communicate
between them.
On Mon, Nov 2, 2015 at 2:38 PM, Yuxin Ren <ryx(a)gwmail.gwu.edu> wrote:
Hi,
I have a few questions about network stack in sel4.
Is network stack implemented in the kernel or user level?
If in user level, are different protocols (IP/TCP) implemented in a
single server or different servers?
If in different servers, how do they communicate with each other?
Is there any example code to show how to use network? How to send and
receive TCP or UDP packets?
How can I set up the network environment on bare metal machine? Is
there documentation or instruction?
Thanks a lot!
Yuxin
_______________________________________________
Devel mailing list
Devel(a)sel4.systems
https://sel4.systems/lists/listinfo/devel
_______________________________________________
Devel mailing list
Devel(a)sel4.systems
https://sel4.systems/lists/listinfo/devel
2:05 p.m.
On 3 Nov 2015, at 12:58 , Raymond Jennings
<shentino@gmail.com<mailto:shentino@gmail.com>> wrote:
So basically L4 grants IO caps to the network card's io ports to whatever task acts
as the network driver, and it's the driver task's job to bang on the card's
I/O and hook up with whatever other tasks represent packet/protocol/whatever layers of the
ISO 7 layer stack.
More precisely: seL4 hands all rights to all resources to the initial process, whose job
is then to initialise the desired system. It would be that process that hands caps to
drivers etc.
Gernot
________________________________
The information in this e-mail may be confidential and subject to legal professional
privilege and/or copyright. National ICT Australia Limited accepts no liability for any
damage caused by this email or its attachments.
2:46 p.m.
So the kernel itself doesn't actually "own" any capabilities, just does
the
bookkeeping and enforcement?
On Mon, Nov 2, 2015 at 7:05 PM, Gernot Heiser <gernot(a)nicta.com.au> wrote:
On 3 Nov 2015, at 12:58 , Raymond Jennings
<shentino(a)gmail.com> wrote:
So basically L4 grants IO caps to the network card's io ports to whatever
task acts as the network driver, and it's the driver task's job to bang on
the card's I/O and hook up with whatever other tasks represent
packet/protocol/whatever layers of the ISO 7 layer stack.
More precisely: seL4 hands all rights to all resources to the initial
process, whose job is then to initialise the desired system. It would be
that process that hands caps to drivers etc.
Gernot
------------------------------
The information in this e-mail may be confidential and subject to legal
professional privilege and/or copyright. National ICT Australia Limited
accepts no liability for any damage caused by this email or its attachments.
2:54 p.m.
On 3 Nov 2015, at 14:46 , Raymond Jennings
<shentino(a)gmail.com> wrote:
So the kernel itself doesn't actually "own" any capabilities, just does
the bookkeeping and enforcement?
Caps are like keys: they authenticate access. The kernel doesn’t need them for its own
purposes. However, our integrity and confidentiality proofs show that the kernel will not
on its own access user memory, unless on behalf of a thread who demonstrates that it is
authorised by presenting an appropriate caps.
Gernot
________________________________
The information in this e-mail may be confidential and subject to legal professional
privilege and/or copyright. National ICT Australia Limited accepts no liability for any
damage caused by this email or its attachments.
4 Nov
4 Nov
4:32 a.m.
Thank you all.
But are there any projects on top of sel4 microkernel which implement
network functionality?
I don't think I need to build the whole network stack from bare metal.
It is best for me to just refer some existing projects and run simple
network application on top of it.
Yuxin
On Mon, Nov 2, 2015 at 10:54 PM, Gernot Heiser <gernot(a)nicta.com.au> wrote:
On 3 Nov 2015, at 14:46 , Raymond Jennings
<shentino(a)gmail.com> wrote:
So the kernel itself doesn't actually "own" any capabilities, just does
the bookkeeping and enforcement?
Caps are like keys: they authenticate access. The kernel doesn’t need them for its own
purposes. However, our integrity and confidentiality proofs show that the kernel will not
on its own access user memory, unless on behalf of a thread who demonstrates that it is
authorised by presenting an appropriate caps.
Gernot
________________________________
The information in this e-mail may be confidential and subject to legal professional
privilege and/or copyright. National ICT Australia Limited accepts no liability for any
damage caused by this email or its attachments.
_______________________________________________
Devel mailing list
Devel(a)sel4.systems
https://sel4.systems/lists/listinfo/devel 
10:13 a.m.
Hi Yuxin,
The AOS project includes a serial console and file system over
Ethernet. The target platform for this project is the SabreLite:
http://www.cse.unsw.edu.au/~cs9242/current/
Project source files are available here:
https://bitbucket.org/kevinelp/unsw-advanced-operating-systems
Keep in mind that this project represents a simple application of IP
stack and network drivers. In your system, you may want to isolate the
DMA capable driver from the IP stack and the server/client components.
- Alex Kroh
On Tue, 2015-11-03 at 12:32 -0500, Yuxin Ren wrote:
Thank you all.
But are there any projects on top of sel4 microkernel which implement
network functionality?
I don't think I need to build the whole network stack from bare metal.
It is best for me to just refer some existing projects and run simple
network application on top of it.
Yuxin
On Mon, Nov 2, 2015 at 10:54 PM, Gernot Heiser <gernot(a)nicta.com.au> wrote:
_______________________________________________
Devel mailing list
Devel(a)sel4.systems
https://sel4.systems/lists/listinfo/devel
On 3 Nov 2015, at 14:46 , Raymond Jennings
<shentino(a)gmail.com> wrote:
So the kernel itself doesn't actually "own" any capabilities, just does
the bookkeeping and enforcement?
Caps are like keys: they authenticate access. The kernel doesn’t need them for its own
purposes. However, our integrity and confidentiality proofs show that the kernel will not
on its own access user memory, unless on behalf of a thread who demonstrates that it is
authorised by presenting an appropriate caps.
Gernot
________________________________
The information in this e-mail may be confidential and subject to legal professional
privilege and/or copyright. National ICT Australia Limited accepts no liability for any
damage caused by this email or its attachments.
_______________________________________________
Devel mailing list
Devel(a)sel4.systems
https://sel4.systems/lists/listinfo/devel
2434
days inactive
2434
days old
7 comments
5 participants
participants (5)
-
Alexander Kroh -
Gernot Heiser -
Raymond Jennings -
Tim Newsham -
Yuxin Ren