FYI: microkernel.info community site

older
Capability faults on seL4_Send and...

Jakub Jermář

11 Mar 2016 11 Mar '16

6:50 a.m.

Hello, just FYI, I have set up a simple web page[1] to promote the wider microkernel community and its goals. So far, the page comes with a brief description of the microkernel concept and an incomplete list of microkernel projects with links to each project's web. The description is made out of the first two sentences I found in the "What is XYZ" section or elsewhere on the web of the respective project. I also took the freedom to use the respective project's logo (or what I believed was the project's logo) for promoting it. I hope you will find this small web a good idea. It was inspired by a similar (though a little bit more informative) site set up by the unikernel community [2]. The sources of the [1] web are hosted on Github [3], so feel free to submit issues or PR to make the site better. Please send me a PM if there are any issues pertaining your project's cartouche that cannot be dealt with using Github. Thanks, Jakub [1] http://microkernel.info [2] http://unikernel.org/projects/ [3] https://github.com/jermar/microkernel.info

Show replies by date

Gernot Heiser

11 Mar 11 Mar

8:33 a.m.

Interesting statement on the Muen kernel section: "The world’s first Open Source microkernel that has been formally proven to contain no runtime errors at the source code level. “ We proved full functional correctness (which is a superset of absence of runtime errors) for seL4 in 2009. I must be missing something. Gernot

...

On 11 Mar 2016, at 6:50 , Jakub Jermář wrote:

Hello,

just FYI, I have set up a simple web page[1] to promote the wider microkernel community and its goals. So far, the page comes with a brief description of the microkernel concept and an incomplete list of microkernel projects with links to each project's web. The description is made out of the first two sentences I found in the "What is XYZ" section or elsewhere on the web of the respective project. I also took the freedom to use the respective project's logo (or what I believed was the project's logo) for promoting it.

I hope you will find this small web a good idea. It was inspired by a similar (though a little bit more informative) site set up by the unikernel community [2]. The sources of the [1] web are hosted on Github [3], so feel free to submit issues or PR to make the site better.

Please send me a PM if there are any issues pertaining your project's cartouche that cannot be dealt with using Github.

Thanks, Jakub

[1] http://microkernel.info [2] http://unikernel.org/projects/ [3] https://github.com/jermar/microkernel.info

_______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel

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

Wolfgang Keller

9:21 a.m.

...

Interesting statement on the Muen kernel section: "The world’s first Open Source microkernel that has been formally proven to contain no runtime errors at the source code level. “

We proved full functional correctness (which is a superset of absence of runtime errors) for seL4 in 2009. I must be missing something.

I believe how it is meant is the following: "The first kernel to both reach being open source and being proven to contain no runtime errors is Muen." (of course among the kernels that are *now* open source, seL4 is the first one for which the absence of runtime errors was proven) Wolfgang On Thu, Mar 10, 2016 at 10:33 PM, Gernot Heiser wrote:

...

Interesting statement on the Muen kernel section: "The world’s first Open Source microkernel that has been formally proven to contain no runtime errors at the source code level. “

We proved full functional correctness (which is a superset of absence of runtime errors) for seL4 in 2009. I must be missing something.

Gernot

...
On 11 Mar 2016, at 6:50 , Jakub Jermář wrote:

Hello,

just FYI, I have set up a simple web page[1] to promote the wider microkernel community and its goals. So far, the page comes with a brief description of the microkernel concept and an incomplete list of microkernel projects with links to each project's web. The description is made out of the first two sentences I found in the "What is XYZ" section or elsewhere on the web of the respective project. I also took the freedom to use the respective project's logo (or what I believed was the project's logo) for promoting it.

I hope you will find this small web a good idea. It was inspired by a similar (though a little bit more informative) site set up by the unikernel community [2]. The sources of the [1] web are hosted on Github [3], so feel free to submit issues or PR to make the site better.

Please send me a PM if there are any issues pertaining your project's cartouche that cannot be dealt with using Github.

Thanks, Jakub

[1] http://microkernel.info [2] http://unikernel.org/projects/ [3] https://github.com/jermar/microkernel.info

_______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel

________________________________

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 https://sel4.systems/lists/listinfo/devel

Christian Stroetmann

11:33 a.m.

On the 10th of March 2016 at 23:21, Wolfgang Keller wrote

...

...
Interesting statement on the Muen kernel section: "The world’s first Open Source microkernel that has been formally proven to contain no runtime errors at the source code level. “

We proved full functional correctness (which is a superset of absence of runtime errors) for seL4 in 2009. I must be missing something. I believe how it is meant is the following: "The first kernel to both reach being open source and being proven to contain no runtime errors is Muen." (of course among the kernels that are *now* open source, seL4 is the first one for which the absence of runtime errors was proven)

Wolfgang

Indeed, I also found this statement a little confusing at first. But nevertheless, I am still very critical with this claim by NICTA as well, because I am virtually for 100% sure, that on the one hand the NASA verified an RTOS for a spacecraft, the USArmy (DARPA, AFRL, etc.) verified an RTOS for a cruise missile or another critical equipement, and one of the largest aircraft manufacturers (e.g. Boeing, Lockheed Martin, Tupolev, or Mikoyan-Gurevich) verified some kind of a small operating system. On the other hand there were always attempts to do such a work, as it could be seen for example with [1], and it is hardly not convincing that in the following 22 years nobody else tried and eventually achieved it. In the case of the NASA and the USArmy I am still waiting for a disclosure of historical informations, which in the case of the army most potentially is still confidential. What makes a judgement even more difficult or even impossible is the problem to draw the exact limits in relation with what is understood as a microkernel, a general purpose operating system kernel and so on for being able to make such a statement "The first verified ... system" at all. Regards Christian Stroetmann [1] William R. Bevier: "A Verified Operating System Kernel", Technical Report 11, October, 1987

...

On Thu, Mar 10, 2016 at 10:33 PM, Gernot Heiser wrote:

...
Interesting statement on the Muen kernel section: "The world’s first Open Source microkernel that has been formally proven to contain no runtime errors at the source code level. “

We proved full functional correctness (which is a superset of absence of runtime errors) for seL4 in 2009. I must be missing something.

Gernot

...
On 11 Mar 2016, at 6:50 , Jakub Jermář wrote:

Hello,

just FYI, I have set up a simple web page[1] to promote the wider microkernel community and its goals. So far, the page comes with a brief description of the microkernel concept and an incomplete list of microkernel projects with links to each project's web. The description is made out of the first two sentences I found in the "What is XYZ" section or elsewhere on the web of the respective project. I also took the freedom to use the respective project's logo (or what I believed was the project's logo) for promoting it.

I hope you will find this small web a good idea. It was inspired by a similar (though a little bit more informative) site set up by the unikernel community [2]. The sources of the [1] web are hosted on Github [3], so feel free to submit issues or PR to make the site better.

Please send me a PM if there are any issues pertaining your project's cartouche that cannot be dealt with using Github.

Thanks, Jakub

[1] http://microkernel.info [2] http://unikernel.org/projects/ [3] https://github.com/jermar/microkernel.info

_______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel

________________________________

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 https://sel4.systems/lists/listinfo/devel

Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel

Gerwin Klein

12:12 p.m.

Hi Christian, we did of course do a lot of digging in that direction, there is at least a 30-year history of attempted OS verification, and quite a few success stories (PSOS, KSOS, EROS, KIT etc). Specifically, the claim for seL4 is machine-checked code-level verification. As far as we are aware, only [1] has done something comparable before seL4, and it is very much a demo toy system only, orders of magnitude smaller. Everything else we’re aware of is not machine-checked verification (i.e. pen-and-paper) or is model-level verification, where not the code is verified, but a manually constructed model of what the code does. Cheers, Gerwin

...

On 11 Mar 2016, at 11:33, Christian Stroetmann wrote:

On the 10th of March 2016 at 23:21, Wolfgang Keller wrote

...
...
Interesting statement on the Muen kernel section: "The world’s first Open Source microkernel that has been formally proven to contain no runtime errors at the source code level. “

We proved full functional correctness (which is a superset of absence of runtime errors) for seL4 in 2009. I must be missing something. I believe how it is meant is the following: "The first kernel to both reach being open source and being proven to contain no runtime errors is Muen." (of course among the kernels that are *now* open source, seL4 is the first one for which the absence of runtime errors was proven)

Wolfgang

Indeed, I also found this statement a little confusing at first.

But nevertheless, I am still very critical with this claim by NICTA as well, because I am virtually for 100% sure, that on the one hand the NASA verified an RTOS for a spacecraft, the USArmy (DARPA, AFRL, etc.) verified an RTOS for a cruise missile or another critical equipement, and one of the largest aircraft manufacturers (e.g. Boeing, Lockheed Martin, Tupolev, or Mikoyan-Gurevich) verified some kind of a small operating system. On the other hand there were always attempts to do such a work, as it could be seen for example with [1], and it is hardly not convincing that in the following 22 years nobody else tried and eventually achieved it.

In the case of the NASA and the USArmy I am still waiting for a disclosure of historical informations, which in the case of the army most potentially is still confidential.

What makes a judgement even more difficult or even impossible is the problem to draw the exact limits in relation with what is understood as a microkernel, a general purpose operating system kernel and so on for being able to make such a statement "The first verified ... system" at all.

Regards Christian Stroetmann

[1] William R. Bevier: "A Verified Operating System Kernel", Technical Report 11, October, 1987

...
On Thu, Mar 10, 2016 at 10:33 PM, Gernot Heiser wrote:

...
Interesting statement on the Muen kernel section: "The world’s first Open Source microkernel that has been formally proven to contain no runtime errors at the source code level. “

We proved full functional correctness (which is a superset of absence of runtime errors) for seL4 in 2009. I must be missing something.

Gernot

...
On 11 Mar 2016, at 6:50 , Jakub Jermář wrote:

Hello,

just FYI, I have set up a simple web page[1] to promote the wider microkernel community and its goals. So far, the page comes with a brief description of the microkernel concept and an incomplete list of microkernel projects with links to each project's web. The description is made out of the first two sentences I found in the "What is XYZ" section or elsewhere on the web of the respective project. I also took the freedom to use the respective project's logo (or what I believed was the project's logo) for promoting it.

I hope you will find this small web a good idea. It was inspired by a similar (though a little bit more informative) site set up by the unikernel community [2]. The sources of the [1] web are hosted on Github [3], so feel free to submit issues or PR to make the site better.

Please send me a PM if there are any issues pertaining your project's cartouche that cannot be dealt with using Github.

Thanks, Jakub

[1] http://microkernel.info [2] http://unikernel.org/projects/ [3] https://github.com/jermar/microkernel.info

_______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel

________________________________

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 https://sel4.systems/lists/listinfo/devel

Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel

_______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel

Alexander Senier

12 Mar 12 Mar

2:03 a.m.

Hi Gernot, when analyzing the statement carefully, you'll find that it's indeed true. The seL4 source was *open-sourced* in July 2014 whereas the Muen source was released in August 2013. But of cause you're right, we're not talking about the same properties here. Cheers, Alex On 03/10/2016 10:33 PM, Gernot Heiser wrote:

...

Interesting statement on the Muen kernel section: "The world’s first Open Source microkernel that has been formally proven to contain no runtime errors at the source code level. “

We proved full functional correctness (which is a superset of absence of runtime errors) for seL4 in 2009. I must be missing something.

-- Dipl.-Inf. Alexander Senier Scientific Assistant TU Dresden Faculty of Computer Science Institute of System Architecture Chair of Privacy and Data Security 01062 Dresden Tel.: +49 351 463-38719 Fax : +49 351 463-38255

Gernot Heiser

1:05 p.m.

On 12 Mar 2016, at 2:03 , Alexander Senier wrote:

...

when analyzing the statement carefully, you'll find that it's indeed true. The seL4 source was *open-sourced* in July 2014 whereas the Muen source was released in August 2013.

But of cause you're right, we're not talking about the same properties here.

… and even the above is at best of historical relevance. Gernot

Vasily A. Sartakov

14 Mar 14 Mar

7 p.m.

New subject: [HelenOS-devel] FYI: microkernel.info community site

Greetings this is a good initiative, I like it. Also, it seems to me, the content of the site can be enhanced by getting-started matherials of relevant projects, or (I prefer), MOOC project about microkernels with basics, history, architectures and examples based on different projects. Also, the final (graduate) practice of this project could be participation in GSOC or just resolving important issues in bug trackers. In my opinion, such course should be sufficient to turn any systems-friendly developer (student) to microkernel practitioner/developer/enthusiast capable to solve engineering issues of open source projects. Several years ago we recorded some lectures bout the L4Re and Genode (Thanks Bjoerd, Norman, Udo): https://www.youtube.com/channel/UCwBjjt60Mmp9X3N71mba3GQ And of course there are many addition materials in any other projects, so, I do not think that it will be complicated to make joint course. Finaly, about the diffusion of microkernels, I think it is important to see how all (and other) projects can be used to solv actual issues, thus, examples of application could also enchance the content (and impact) of the site.

...

just FYI, I have set up a simple web page[1] to promote the wider microkernel community and its goals. So far, the page comes with a brief description of the microkernel concept and an incomplete list of microkernel projects with links to each project's web. The description is made out of the first two sentences I found in the "What is XYZ" section or elsewhere on the web of the respective project. I also took the freedom to use the respective project's logo (or what I believed was the project's logo) for promoting it.

I hope you will find this small web a good idea. It was inspired by a similar (though a little bit more informative) site set up by the unikernel community [2]. The sources of the [1] web are hosted on Github [3], so feel free to submit issues or PR to make the site better.

Please send me a PM if there are any issues pertaining your project's cartouche that cannot be dealt with using Github.

-- Vasily A. Sartakov sartakov@ksyslabs.org

Jakub Jermář

8:04 p.m.

New subject: [HelenOS-devel] FYI: microkernel.info community site

Hi Vasily, On 03/14/2016 09:00 AM, Vasily A. Sartakov wrote:

...

this is a good initiative, I like it.

Also, it seems to me, the content of the site can be enhanced by getting-started matherials of relevant projects, or (I prefer), MOOC project about microkernels with basics, history, architectures and examples based on different projects. Also, the final (graduate) practice of this project could be participation in GSOC or just resolving important issues in bug trackers. In my opinion, such course should be sufficient to turn any systems-friendly developer (student) to microkernel practitioner/developer/enthusiast capable to solve engineering issues of open source projects.

Several years ago we recorded some lectures bout the L4Re and Genode (Thanks Bjoerd, Norman, Udo):

https://www.youtube.com/channel/UCwBjjt60Mmp9X3N71mba3GQ

And of course there are many addition materials in any other projects, so, I do not think that it will be complicated to make joint course.

Finaly, about the diffusion of microkernels, I think it is important to see how all (and other) projects can be used to solv actual issues, thus, examples of application could also enchance the content (and impact) of the site.

Yes, the site can be definitely enhanced to contain more useful stuff such as tutorials, papers, blog entries and microkernel news. It could also serve as a basis for a prospective microkernel umbrella organization for the various summer of code programs and also the Microkernel devroom at FOSDEM in order to maximize chances of being accepted. Focusing on the web site's content for now, I've already merged PR's of several people and am willing to continue within, including the creation of a menu and subpages for the above content as soon as it appears. Jakub

...

...
just FYI, I have set up a simple web page[1] to promote the wider microkernel community and its goals. So far, the page comes with a brief description of the microkernel concept and an incomplete list of microkernel projects with links to each project's web. The description is made out of the first two sentences I found in the "What is XYZ" section or elsewhere on the web of the respective project. I also took the freedom to use the respective project's logo (or what I believed was the project's logo) for promoting it.

I hope you will find this small web a good idea. It was inspired by a similar (though a little bit more informative) site set up by the unikernel community [2]. The sources of the [1] web are hosted on Github [3], so feel free to submit issues or PR to make the site better.

Please send me a PM if there are any issues pertaining your project's cartouche that cannot be dealt with using Github.

-- Vasily A. Sartakov sartakov@ksyslabs.org

_______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel

3202

Age (days ago)

3206

Last active (days ago)

List overview

Download

8 comments

8 participants

participants (8)

Alexander Senier
Christian Stroetmann
Gernot Heiser
Gernot Heiser
Gerwin Klein
Jakub Jermář
Vasily A. Sartakov
Wolfgang Keller