Historias
Slashboxes
Comentarios
 

seL4 Microkernel verificado formalmente ahora Open Source

editada por neu___ el Martes, 05 Agosto de 2014, 20:13h   Printer-friendly   Email story
desde el dept. super-seguros
Un pobrecito hablador nos cuenta: «En 2009, OKLabs / NICTA anunció el primer microkernel verificado formalmente, seL4 (un miembro de la familia L4). Por desgracia, era software privativo. Hoy en día, ya no es el caso: seL4 ha sido liberado bajo la GPLv2 (sin la cláusula de "o versiones posteriores"). Citando la fuente de OsNews:
OSNews informa que el formalmente verificado microkernel seL4 es ahora de código abierto: "General C4 Systems Dynamics y NICTA se complacen en anunciar la liberación de seL4, el primer kernel del mundo probado mátemáticamente de extremo a extrema tanto en su implementación como en su seguridad. El sistema operativo más altamente asegurado del mundo. El código fuente se encuentran en Github (aunque visto lo anterior no creo que manden muchos bugs). Es compatible con ARM y x86 (incluyendo la famosa placa BEAGLEBONE ARM). Si tienes un x86 con las extensiones VT-x y EPT podrías ejecutar Linux sobre seL4 (tal como hace la página web de seL4). Más información en el FAQ . Y tu ¿has abandonado ya GNU/Hurd por un microkernel más "formal"?»

Mostrar opciones Umbral:
Y recuerda: Los comentarios que siguen pertenecen a las personas que los han enviado. No somos responsables de los mismos.