Formal verification of an OS kernel


SeL4: Verificación formal de un kernel del sistema operativo
seL4: Formal verification of an OS kernel [1] (A proof engineer perspective). Alejandro Gomez-Londoño. Affiliation: Proof Engineer at Data61/CSIRO, Australia. Febrero 13 de 2017.
Abstract: The seL4 microkernel is «The world’s first operating-system kernel with an end-to-end proof of implementation correctness and security enforcement» [2]. In this talk, we present a high-level overview of seL4s specification and proofs, along with user cases and future challenges of the seL4 project.

[1] seL4: Formal verification of an OS kernel?. Gerwin Klein et al, ACM Symposium on Operating Systems Principles 2009.

[2] seL4 project website

Autor: envivo

Compartir esta publicación en

Deja un comentario

Este sitio usa Akismet para reducir el spam. Aprende cómo se procesan los datos de tus comentarios.