Full-Fledge Verified OS

[ziteribo]

Hello Misters,

As you are interested in OS design, I am asking your help.

I believe it's time for a full-fledge verified OS.

http://www.ertos.nicta.com.au/publicati ... _KH_05.pdf

I am attempting to build a team.

OS-design :
[*] http://www.ertos.nicta.com.au/publicati ... lie_06.pdf ( for transition )
[*] http://www.marcus-brinkmann.org/hurd-ng.pdf
[*] http://www.eecg.toronto.edu/~tornado/ ( scalability / hot swapping )

kernel :
[*]http://os.inf.tu-dresden.de/L4/L4.Sec/
[*]http://www.doclsf.de/papers/vstte06.pdf

network stack :
[*]http://www.cl.cam.ac.uk/~pes20/Netsem/

programming :
[*] http://fling-l.seas.upenn.edu/~plclub/c ... _Challenge
[*] http://www.informatik.uni-bonn.de/~loeh/GFP.html
[*] http://maude.cs.uiuc.edu/tools/scc/

proving environment :
[*] http://isabelle.in.tum.de/
[*] http://www.cl.cam.ac.uk/Research/HVG/HOL/

compiler :
[*] http://pauillac.inria.fr/~xleroy/compcert-backend/
[*] http://www.score.is.tsukuba.ac.jp/~okuma/vc/

Any suggestions ?

Thank you for your answer,

If you want to contact me, my mail is guillaume_dot_fortaine_at_wanadoo_dot_fr

I will set up a mailing-list, a web server, a wiki and an IRC

Best Regards,

Guillaume FORTAINE

[ineo]

Hello !

Interesting links.
This is hardly an OS design, but I guess these are the main guidelines you plan to follow.

I am interested to see how far you can prove your OS does what it should be doing For example if you use multitasking most of your proof will be very difficult, Cf. Leslie Lamport well known problems.

Good luck !

[ziteribo]

Hello !

Interesting links.
This is hardly an OS design, but I guess these are the main guidelines you plan to follow.

I am interested to see how far you can prove your OS does what it should be doing For example if you use multitasking most of your proof will be very difficult, Cf. Leslie Lamport well known problems.

Good luck !

Hello ineo ,

I believe we could use this paper as a good start point :

http://www.cs.missouri.edu/~harrison/papers/amast06.pdf

The use of a functional language, a good API and a verified kernel will help too .

[*] http://www.ertos.nicta.com.au/research/sel4/api.pml
[*] http://www.doclsf.de/papers/vstte06.pdf

Ohters interesting publications :
Design Principles and Patterns for Computer Systems That Are Simultaneously Secure and Usable

[*] http://www.simson.net/thesis/thesis.pdf
[*] http://kbs.cs.tu-berlin.de/teaching/ws2 ... kernel.pdf

Best Regards,

Will

[Pype.Clicker]

hm .. that's certainly an interesting collection of links, but for those who are not familiar with formal verification of programs, would you mind describing what your "full-fledge verified" OS would have to comply with ?

[ziteribo]

Hello,

I would want to comply with the HurdNG requirements ( the grailos will ensure transition ) . We should include cutting-edge specifications : hot swapping, state of the art device driver framework, and secure based microkernel formally verified. This is my goal. Generic programming should be a great help to ensure this one ...

All these toys OS are useless nowadays ... Linux largely outperforms them ... We always reinvent the wheel ... Some great publications are forgot ... We need to join our forces together, to have the best framework available to think higher ...

Best Regards,

Will

[Kemp]

We should include cutting-edge specifications : hot swapping, state of the art device driver framework, and secure based microkernel formally verified.

We need to join our forces together, to have the best framework available to think higher

Ever considered a job in marketting?

[spider]

Hello,

I would want to comply with the HurdNG requirements ( the grailos will ensure transition ) . We should include cutting-edge specifications : hot swapping, state of the art device driver framework, and secure based microkernel formally verified. This is my goal. Generic programming should be a great help to ensure this one ...

All these toys OS are useless nowadays ... Linux largely outperforms them ... We always reinvent the wheel ... Some great publications are forgot ... We need to join our forces together, to have the best framework available to think higher ...

Best Regards,

Will

Why not just work on linux then?

[Solar]

Because Linux cannot be proven correct formally. Basically, no OS not designed with that proof in mind can be proven retroactively, not without a huge amount of extra work.

But why the HurdNG specs? I know there is a industry standard for proven software, that could open you a couple of doors...

Then again:

We always reinvent the wheel ... Some great publications are forgot ... We need to join our forces together, to have the best framework available to think higher ...

You will make the very same mistakes, and some of the others here might tell you that they have the "best framework", or that you should use OSKit, or Linux, or Singularity... don't expect to rally everyone under your banner. Doesn't work. I know. I have been there.

[ziteribo]

.. don't expect to rally everyone under your banner. Doesn't work. I know. I have been there.

"Nobody should start to undertake a large project. You start with a small _trivial_ project, and you should never expect it to get large. If you do, you'll just overdesign and generally think it is more important than it likely is at that stage. Or worse, you might be scared away by the sheer size of the work you envision. So start small, and think about the details. Don't think about some big picture and fancy design. If it doesn't solve some fairly immediate need, it's almost certainly over-designed. And don't expect people to jump in and help you. That's not how these things work. You need to get something half-way _useful_ first, and then others will say "hey, that _almost_ works for me", and they'll get involved in the project. " (2004)

Linus Torvalds

Best Regards,

Will

[Brendan]

Hi,

"Nobody should start to undertake a large project. You start with a small _trivial_ project, and you should never expect it to get large. If you do, you'll just overdesign and generally think it is more important than it likely is at that stage. Or worse, you might be scared away by the sheer size of the work you envision. So start small, and think about the details. Don't think about some big picture and fancy design. If it doesn't solve some fairly immediate need, it's almost certainly over-designed. And don't expect people to jump in and help you. That's not how these things work. You need to get something half-way _useful_ first, and then others will say "hey, that _almost_ works for me", and they'll get involved in the project. " (2004)

Linus Torvalds

In my experience the above is completly misleading bullshit - designing a simplistic system and then trying to retro-fit less simplistic functionality is at least twice as hard as designing it properly to begin with.

However, I do understand how someone could form this opinion after half implementing someone else's OS design, and then being fortunate enough to have thousands of other programmers volunteer years of thier time to fix the resulting mess...


Cheers,

Brendan

[Kemp]

Total agreement with Brendan there, Linux would be an absolutely terrible system if it didn't have a huge number of people fixing/working around all the problems with it. As for whether it was worth it in the end, that's up to personal opinion, but I haven't heard any reductions in the people moaning about how hard it is to dev on due to poor decisions in the past that can't be revoked because it'd break half the rest of it.

[Habbit]

Total agreement with Brendan there, Linux would be an absolutely terrible system if it didn't have a huge number of people fixing/working around all the problems with it. As for whether it was worth it in the end, that's up to personal opinion, but I haven't heard any reductions in the people moaning about how hard it is to dev on due to poor decisions in the past that can't be revoked because it'd break half the rest of it.

I think you have quite a point there. I strongly advocate microkernel designs because, for example, I am sick of printer drivers crashing my XP box or ANY driver killing my Ubuntu one just because they run as "executive" or "modules" linked into the kernel...
But if you _really_ want to restart the ten-year-old flame war, we can invite Prof. Tanenbaum and Mr. Torvalds to this forum ;D (IIRC, Prof. said he would have failed Torvalds for his kernel design. oh my, that _was_ good ^_^)

[Brendan]

Hi,

Of course I should point out that I mean no disrespect to Linus or his work - he is an extremely accomplished programmer who has succeeded in an area that is considerably difficult, and is responsible for what has become a very professional, stable and powerful OS....

I'm just saying that "OS design" shouldn't be confused with "OS implementation", and also hoping that if I ever become as famous as Linus that no-one finds some of the "less than well-thought-out" things I've said in the past..

There is also some truth in what Linus said, but to me it's more about attracting volunteers than the technical details of the project itself - something that works is more likely to receive attention than something that is much better designed but only partially implemented...


Cheers,

Brendan