Sistemas & Desarrollo

encontrados: 4, tiempo total: 0.043 segundos rss2
14 meneos
67 clics
Liberado GNU Hurd 0.7 y GNU Mach 1.6

Liberado GNU Hurd 0.7 y GNU Mach 1.6

Se ha liberado una nueva versión de Hurd, el proyecto creado en 1990 para ser el núcleo de los sistemas GNU, que en aquel momento ya contaba con compilador, editores, shell…y que sería el encargado de reemplazar los tradicionales kernels tipo Unix, por un sistema de microkernel que ofrece las funcionas más básicas de acceso al hardware y la memoria, mientras delega en una especies de servidores las funciones más avanzadas, proporcionando un sistema más modular que los llamados kernel monolíticos.
9 5 0 K 51
1 comentarios
9 5 0 K 51
5 meneos
73 clics

Microkernels L4: lecciones después de 20 años de investigación y despliegue [ENG]

El microkernel L4 tiene 20 años de uso y evolución. Además, tiene una comunidad de usuarios y desarrolladores muy activa junto con versiones comerciales desplegadas en sistemas a gran escala y críticos. En este artículo se examinarán las lecciones aprendidas después de 20 años de diseño y desarrollo de microkernels L4, desde sus orígenes hasta las últimas implementaciones. [Este artículo es un extracto, pero se puede descargar la publicación completa en PDF: www.nicta.com.au/pub-download/full/8988 615 KB]
5 0 0 K 40
sin comentarios
5 0 0 K 40
9 meneos
115 clics
El microkernel seL4 ha sido verificado formalmente para procesadores RISC-V [ENG]

El microkernel seL4 ha sido verificado formalmente para procesadores RISC-V [ENG]

El kernel de un sistema operativo es el software que funciona a más bajo nivel en un ordenador. Es el código que funciona en modo privilegiado (S-Mode en RISC-V), por lo que es el responsable principal y único de la seguridad del sistema. Que un kernel, en este caso seL4, esté formalmente verificado significa que su implementación en C es funcionalmente correcta, ya que ha sido matemáticamente verificada mediante software probando que está libre de errores.
5 4 0 K 47
5 comentarios
5 4 0 K 47
3 meneos
12 clics

El código binario del microkernel seL4 ha sido verificado formalmente para procesadores RISC-V [ENG]

En junio de 2020 anunciamos que el microkernel seL4 fue el primer kernel de sistema operativo del mundo con prueba de corrección de implementación verificada por máquina, también verificada para la arquitectura RV64, lo que lo convierte en el primer sistema operativo verificado formalmente para RISC-V. Ahora nos complace anunciar que esta verificación se ha extendido al código binario ejecutable, lo que significa que se ha demostrado que el código máquina que se ejecuta en el procesador es correcto. // Relacionada: El microkernel seL4 ha sido verificado formalmente para procesadores RISC-V.
2 1 0 K 39
sin comentarios
2 1 0 K 39

menéame