On 08/31/15 19:30, Tom Mitchell wrote:

On Mon, Aug 31, 2015 at 2:28 AM, Gernot Heiser mailto:gernot@nicta.com.au> wrote:

On 31 Aug 2015, at 18:57 , Raymond Jennings 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.

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... ? 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.

-- T o m M i t c h e l l

On 31 Aug 2015, at 19:33 , Jeroen Slim van Gelderen 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.abstra... - 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.pmlhttps://ssrg.nicta.com.au/publications/nictaabstracts/Elphinstone_Heiser_13.... 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.

On 31/08/2015 9:46 pm, Gernot Heiser wrote: On 31 Aug 2015, at 19:33 , Jeroen Slim van Gelderen <mailto:askslim@gmail.comaskslim@gmail.commailto:askslim@gmail.com> wrote: http://www.informit.com/articles/article.aspx?p=1994798http://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.