L4.sec implementation and formal verification
Hello Misters, As you are microkernel experts, I am asking your help. I am attempting to build up a team. I believe it's time for a full-fledge verified OS. If somebody is interested in functional programming and in formal methods to help to implement the L4.sec kernel , he is welcome :) Here is an example of a protocol formalisation : network stack : http://www.cl.cam.ac.uk/~pes20/Netsem/ 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
You may want to have a look at L4.verified. http://ertos.nicta.com.au/research/l4.verified/ Gernot
On Sat, 26 Aug 2006 04:05:11 +0200, William DUCK <guillaume.fortaine@wanadoo.fr> said: WD> Hello Misters, WD> As you are microkernel experts, I am WD> asking your help.
WD> I am attempting to build up a team. WD> I believe it's time for a full-fledge verified OS. WD> If somebody is interested in functional programming and in formal methods to WD> help to implement the L4.sec kernel , he is welcome :) WD> Here is an example of a protocol formalisation : WD> network stack : WD> http://www.cl.cam.ac.uk/~pes20/Netsem/ WD> If you want to contact me, my mail is guillaume_dot_fortaine_at_wanadoo_dot_fr WD> I will set up a mailing-list, a web server, a wiki and an IRC WD> Best Regards, WD> Guillaume FORTAINE
participants (2)
-
Gernot Heiser -
William DUCK