Zobrazeno 1 - 10
of 35
pro vyhledávání: '"Kevin Elphinstone"'
Publikováno v:
DSN
High availability and integrity are paramount in systems deployed in life-and mission-critical scenarios. Such fault-tolerance can be achieved through redundant co-execution (RCoE) on replicated hardware, now cheaply available with multicore processo
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::cd99c5887452cfe9d37eebdad90a8033
https://doi.org/10.1109/dsn.2019.00031
https://doi.org/10.1109/dsn.2019.00031
Autor:
Gernot Heiser, Kevin Elphinstone
Publikováno v:
ACM Transactions on Computer Systems. 34:1-29
The L4 microkernel has undergone 20 years of use and evolution. It has an active user and developer community, and there are commercial versions that are deployed on a large scale and in safety-critical systems. In this article we examine the lessons
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::7a495a014ec6908f768851019a2bedfc
https://doi.org/10.1145/2893177
https://doi.org/10.1145/2893177
Publikováno v:
APSys
In the paper, we argue that it is worthwhile to revisit building microkernel-based multiserver operating systems, and introduce a multiserver OS architecture. We argue that recent formal verification of microkernels provides a compelling platform for
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::90ddba04164d5561459ead8515da7658
https://doi.org/10.1145/3124680.3124727
https://doi.org/10.1145/3124680.3124727
Autor:
Gernot Heiser, Toby Murray, Rafal Kolanski, Gerwin Klein, Kevin Elphinstone, June Andronick, Thomas Sewell
Publikováno v:
ACM Transactions on Computer Systems. 32:1-70
We present an in-depth coverage of the comprehensive machine-checked formal verification of seL4, a general-purpose operating system microkernel. We discuss the kernel design we used to make its verification tractable. We then describe the functional
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::6988263e7d27a8bf0cfe1da1abd42f3b
https://doi.org/10.1145/2560537
https://doi.org/10.1145/2560537
Autor:
Harvey Tuch, Dhammika Elkaduwe, Simon Winwood, Kai Engelhardt, Thomas Sewell, June Andronick, Philip Derrin, Gernot Heiser, Gerwin Klein, Kevin Elphinstone, David Cock, Rafal Kolanski, Michael Norrish
Publikováno v:
Communications of the ACM. 53:107-115
We report on the formal, machine-checked verification of the seL4 microkernel from an abstract specification down to its C implementation. We assume correctness of compiler, assembly code, hardware, and boot code. seL4 is a third-generation microkern
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::2d1faa2c206cf0c9f122a6d20eb286a5
https://doi.org/10.1145/1743546.1743574
https://doi.org/10.1145/1743546.1743574
Publikováno v:
Scopus-Elsevier
ICFP
ICFP
We report on our experience using Haskell as an executable specification language in the formal verification of the seL4 microkernel. The verification connects an abstract operational specification in the theorem prover Isabelle/HOL to a C implementa
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::2214d9a2cf3e7a8a2e32017cf69d876f
https://doi.org/10.1145/1631687.1596566
https://doi.org/10.1145/1631687.1596566
Publikováno v:
ACM SIGOPS Operating Systems Review. 41:3-11
As computer systems become increasingly mission-critical, used in life-critical situations, and relied upon to protect intellectual property, operating-system reliability is becoming an ever growing concern. In the past, mission- and life-critical em
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::99a9ac9642bfe1a402a81a7300ac614c
https://doi.org/10.1145/1278901.1278904
https://doi.org/10.1145/1278901.1278904
Autor:
Yanyan Shen, Kevin Elphinstone
Publikováno v:
EDCC
Trustworthy isolation is required to consolidate safety and security critical software systems on a single hardware platform. Recent advances in formally verifying correctness and isolation properties of a microkernel should enable mutually distrusti
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::0f0e0d9b1b42a754ddfdd01ba974596f
https://doi.org/10.1109/edcc.2015.16
https://doi.org/10.1109/edcc.2015.16
Publikováno v:
APSys
It is well-established that high-end scalability requires fine-grained locking, and for a system like Linux, a big lock degrades performance even at moderate core counts. Nevertheless, we argue that a big lock may be fine-grained enough for a microke
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::42102584ca247a31e6705b08a0e3852d
https://doi.org/10.1145/2797022.2797042
https://doi.org/10.1145/2797022.2797042
Autor:
Charles A. Gray, Luke Macpherson, Nicholas FitzRoy-Dale, Yueting (Rita) Shen, Daniel Potts, Stefan Götz, Gernot Heiser, Ben Leslie, Kevin Elphinstone, Peter Chubb
Publikováno v:
Journal of Computer Science and Technology. 20:654-664
Running device drivers as unprivileged user-level code, encapsulated into their own process, has often been proposed as a technique for increasing system robustness. However, in the past, systems based on user-level drivers have generally exhibited p
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::76532f0ed567e53d45b85f70a7734b2b
https://doi.org/10.1007/s11390-005-0654-4
https://doi.org/10.1007/s11390-005-0654-4