31 Aug
2015
31 Aug
'15
4:57 a.m.
Is there an easy way for one task to share address space with another task
directly or does it have to go through the kernel/os and be emulated?
I noticed that support for mapping memory is mostly low level assignment of
physical frames to virtual frames via page tables, unlike Mach which uses
memory objects.
31 Aug
31 Aug
5:28 a.m.
On 31 Aug 2015, at 18:57 , Raymond Jennings
<shentino@gmail.com<mailto:shentino@gmail.com>> wrote:
Is there an easy way for one task to share address space with another task directly or
does it have to go through the kernel/os and be emulated?
there’s nothing stopping you mapping the same frame into two different address spaces
(provided you have the rights to do so).
I noticed that support for mapping memory is mostly low level assignment of physical
frames to virtual frames via page tables, unlike Mach which uses memory objects.
Yes, a microkernel’s job is to provide low-level abstractions. Mach-style memory objects
isn’t one of them. See
https://ssrg.nicta.com.au/publications/nictaabstracts/Elphinstone_Heiser_13…
for an explanation of the philosophy.
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.
10:30 p.m.
On Mon, Aug 31, 2015 at 2:28 AM, Gernot Heiser <gernot(a)nicta.com.au> wrote:
On 31 Aug 2015, at 18:57 , Raymond Jennings
<shentino(a)gmail.com> wrote:
Is there an easy way for one task to share address space with another task
directly or does it have to go through the kernel/os and be emulated?
there’s nothing stopping you mapping the same frame into two different
address spaces (provided you have the rights to do so).
I noticed that support for mapping memory is mostly low level assignment
of physical frames to virtual frames via page tables, unlike Mach which
uses memory objects.
IPC using shared memory policy needs to be considered and established.
Shared read-write both processes need to have the (exact?) same levels.
Shared rw --> ro is one way and the sender needs to be trusted
to do the correct things with data it has access to.
There is more to be considered... in a machine eyes-only needs
a policy where a decision can be made but no other output
is permitted policy.
Without a policy and strategy things get unsecured in a hurry.
One might simply use files and allow page cache to accelerate
communication.
Device drivers... ?
--
T o m M i t c h e l l
10:34 p.m.
On 08/31/15 19:30, Tom Mitchell wrote:
On Mon, Aug 31, 2015 at 2:28 AM, Gernot Heiser
<gernot(a)nicta.com.au
<mailto:gernot@nicta.com.au>> wrote:
On 31 Aug 2015, at 18:57 , Raymond Jennings <shentino(a)gmail.com
<mailto:shentino@gmail.com>> wrote:
I suppose if you wanted to use shared memory for IPC you could
always
make a call to the designated "virtual memory" server to create a
mappable object whose capability you could then pass to the target
server to allow it to ask to be mapped.
Given the recent commentary that the OS needs to implement virtual
memory itself you could say that it should also handle shared memory for
IPC between "userspace" processes that depend on the server as well as
the microkernel.
Is there an easy way for one task to share address space with
another task directly or does it have to go through the kernel/os
and be emulated?
there’s nothing stopping you mapping the same frame into two
different address spaces (provided you have the rights to do so).
I noticed that support for mapping memory is
mostly low level
assignment of physical frames to virtual frames via page tables,
unlike Mach which uses memory objects.
IPC using shared memory policy needs to be considered and established.
Shared read-write both processes need to have the (exact?) same levels.
Shared rw --> ro is one way and the sender needs to be trusted
to do the correct things with data it has access to.
There is more to be considered... in a machine eyes-only needs
a policy where a decision can be made but no other output
is permitted policy.
Without a policy and strategy things get unsecured in a hurry.
One might simply use files and allow page cache to accelerate
communication.
Device drivers... ? --
T o m M i t c h e l l
5:33 a.m.
In seL4, capabilities are used to refer to blocks of memory. You can
delegate access to parts of your address space simply by passing the
capability to another process. You can also implement nested processes, by
providing them with only the capabilities to talk to you. Memory in seL4 is
typed. For example, some memory regions hold capabilities; to preserve the
unforgeable guarantee, they can only be modified by the microkernel. On
boot, the kernel reserves some memory for itself and then delegates the
remainder of the memory to a process as an untyped memory (UM) capability.
-- http://www.informit.com/articles/article.aspx?p=1994798
On Mon, Aug 31, 2015 at 3:57 AM, Raymond Jennings <shentino(a)gmail.com>
wrote:
Is there an easy way for one task to share address
space with another task
directly or does it have to go through the kernel/os and be emulated?
I noticed that support for mapping memory is mostly low level assignment
of physical frames to virtual frames via page tables, unlike Mach which
uses memory objects.
_______________________________________________
Devel mailing list
Devel(a)sel4.systems
https://sel4.systems/lists/listinfo/devel
--
Jeroen "Slim" van Gelderen
7:46 a.m.
On 31 Aug 2015, at 19:33 , Jeroen Slim van Gelderen
<askslim@gmail.com<mailto:askslim@gmail.com>> wrote:
In seL4, capabilities are used to refer to blocks of memory. You can delegate access to
parts of your address space simply by passing the capability to another process. You can
also implement nested processes, by providing them with only the capabilities to talk to
you. Memory in seL4 is typed. For example, some memory regions hold capabilities; to
preserve the unforgeable guarantee, they can only be modified by the microkernel. On boot,
the kernel reserves some memory for itself and then delegates the remainder of the memory
to a process as an untyped memory (UM) capability. --
http://www.informit.com/articles/article.aspx?p=1994798
Thanks for the pointer to this article, I hadn’t seen it.
It has a lot of informed content, but also some some confusion, so take it with a grain of
salt.
Among the things I noticed:
- this is the first time I hear about doubling access-rights check in Mach being a major
issue. Maybe it was, but it hasn’t figured in the literature or discussions with Jochen
Liedtke. Other comments about Mach I can confirm.
- I have no idea where this factor 25 comes from: "The numbers produced by NICTA
indicate that it costs around 25 times as much to develop a system this way as to develop
one with no verification, testing, or QA.” OK, writing an OS with “cat >” is going to
be faster, but also utterly useless, so what’s the point? Our more detailed analysis
paints a completely different picture: we’re a factor 2–3 *cheaper* than traditional
"high-assurance” software (which still has no guarantee of correctness), and a factor
2–4 more expensive than traditional low-assurance software (which doesn’t even pretend to
make any claims of correctness). For details, check the peer-reviewed literature:
https://ssrg.nicta.com.au/publications/nictaabstracts/Klein_AEMSKH_14.abstr…
- the comments about preemtability (or not) miss the point. The continuation-passing style
is a result of seL4 being an event-based design (as opposed to the traditional
process-oriented L4 kernels), a decision which was made *before* any thought of
verification (to reduce memory usage) but turned out to be an enabler. The mechanism for
achieving good interrupt latencies are preemption points, which aren’t new, the UNSW
L4/MIPS kernel had them 18 years ago. See
ttps://ssrg.nicta.com.au/publications/nictaabstracts/Elphinstone_Heiser_13.abstract.pml<https://ssrg.nicta.com.au/publications/nictaabstracts/Elphinstone_Heiser_13.abstract.pml>
for details.
- TrustZone actually adds *nothing* that can’t be achieved with just seL4. Its continued
existence is a result of established players not wanting to change their (broken) security
model.
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.
8:04 a.m.
Interesting article. I’d add one more point to Gernot’s:
- seL4 does have a test suite, and the verifiers are very happy about that. :-)
Even though it is proved correct, the proof does have assumptions and you can can validate
those by test. For maintenance, finding simple obvious mistakes can be quick in a
regression test suite, saving you time in verification. The problem with test is just that
you don't know when you have tested enough. That’s what the proof is good at.
Cheers,
Gerwin
On 31.08.2015, at 21:46, Gernot Heiser
<gernot@nicta.com.au<mailto:gernot@nicta.com.au>> wrote:
On 31 Aug 2015, at 19:33 , Jeroen Slim van Gelderen
<askslim@gmail.com<mailto:askslim@gmail.com>> wrote:
In seL4, capabilities are used to refer to blocks of memory. You can delegate access to
parts of your address space simply by passing the capability to another process. You can
also implement nested processes, by providing them with only the capabilities to talk to
you. Memory in seL4 is typed. For example, some memory regions hold capabilities; to
preserve the unforgeable guarantee, they can only be modified by the microkernel. On boot,
the kernel reserves some memory for itself and then delegates the remainder of the memory
to a process as an untyped memory (UM) capability. --
http://www.informit.com/articles/article.aspx?p=1994798
Thanks for the pointer to this article, I hadn’t seen it.
It has a lot of informed content, but also some some confusion, so take it with a grain of
salt.
Among the things I noticed:
- this is the first time I hear about doubling access-rights check in Mach being a major
issue. Maybe it was, but it hasn’t figured in the literature or discussions with Jochen
Liedtke. Other comments about Mach I can confirm.
- I have no idea where this factor 25 comes from: "The numbers produced by NICTA
indicate that it costs around 25 times as much to develop a system this way as to develop
one with no verification, testing, or QA.” OK, writing an OS with “cat >” is going to
be faster, but also utterly useless, so what’s the point? Our more detailed analysis
paints a completely different picture: we’re a factor 2–3 *cheaper* than traditional
"high-assurance” software (which still has no guarantee of correctness), and a factor
2–4 more expensive than traditional low-assurance software (which doesn’t even pretend to
make any claims of correctness). For details, check the peer-reviewed literature:
https://ssrg.nicta.com.au/publications/nictaabstracts/Klein_AEMSKH_14.abstr…
- the comments about preemtability (or not) miss the point. The continuation-passing style
is a result of seL4 being an event-based design (as opposed to the traditional
process-oriented L4 kernels), a decision which was made *before* any thought of
verification (to reduce memory usage) but turned out to be an enabler. The mechanism for
achieving good interrupt latencies are preemption points, which aren’t new, the UNSW
L4/MIPS kernel had them 18 years ago. See
ttps://ssrg.nicta.com.au/publications/nictaabstracts/Elphinstone_Heiser_13.abstract.pml<https://ssrg.nicta.com.au/publications/nictaabstracts/Elphinstone_Heiser_13.abstract.pml>
for details.
- TrustZone actually adds *nothing* that can’t be achieved with just seL4. Its continued
existence is a result of established players not wanting to change their (broken) security
model.
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@sel4.systems<mailto:Devel@sel4.systems>
https://sel4.systems/lists/listinfo/devel
9:02 a.m.
On 31/08/2015 9:46 pm, Gernot Heiser wrote:
On 31 Aug 2015, at 19:33 , Jeroen Slim van Gelderen
<<mailto:askslim@gmail.com>askslim@gmail.com<mailto:askslim@gmail.com>>
wrote:
<http://www.informit.com/articles/article.aspx?p=1994798>http://www.informit.com/articles/article.aspx?p=1994798
Thanks for the pointer to this article, I hadn’t seen it.
It has a lot of informed content, but also some some confusion, so take it with a grain of
salt.
Among the things I noticed:
[snip]
- I have no idea where this factor 25 comes from: "The numbers produced by NICTA
indicate that it costs around 25 times as much to develop a system this way as to develop
one with no verification, testing, or QA.”
I can understand why somebody might draw that conclusion.
The raw numbers for the total effort to develop and verify seL4 that were often quoted
back in 2012 (when the article was written) were around the 25 person-year mark. The TOCS
paper from 2014 should however be used these days as the authoritative figure on that
question: ssrg.nicta.com.au/publications/nictaabstracts/7371.pdf
I remember Tanenbaum writing somewhere ages ago that one can expect about a person-year to
design and write a kernel ala MINIX (although presumably that figure would include some
testing...). Indeed, for rubbish, one might expect to do it in a lot less than 1py. (This
highlights the meaninglessness of comparing effort for verified software to that for
rubbish, of course. Not to mention that seL4 and MINIX are very different.)
That said, the state of the art in systems software verification has moved on a little
since 2009. Our own work at NICTA in the context of file systems is already showing how to
dramatically reduce the work required for proving functional correctness (albeit for
software with less internal coupling than a microkernel) by co-designing the programming
language and verification infrastructure, taking advantage of cool language type systems
coupled with corresponding automated reasoning in the theorem prover. But that's a
story for another day.
Toby
________________________________
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.
2281
days inactive
2282
days old
7 comments
6 participants
participants (6)
-
Gernot Heiser -
Gerwin Klein -
Jeroen "Slim" van Gelderen -
Raymond Jennings -
Toby Murray -
Tom Mitchell