Experience Report: seL4 Formally Verifying a High-Performance Microkernel

被引：5
|
作者：
Klein, Gerwin
Derrin, Philip
Elphinstone, Kevin
机构：
来源：
ACM SIGPLAN NOTICES | 2009年 / 44卷 / 8-9期
关键词：
Verification; Design; Languages; Haskell; seL4; microkernel; Isabelle/HOL;
D O I：
10.1145/1631687.1596566
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
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 implementation of the microkernel. We describe how this project differs from other efforts, and examine the effect of using Haskell in a large-scale formal verification. The kernel comprises 8,700 lines of C code; the verification more than 150,000 lines of proof script.
引用
收藏
页码：91 / 95
页数：5
相关论文
共 50 条
  • [1] Experience Report: seL4 Formally Verifying a High-Performance Microkernel
    Klein, Gerwin
    Derrin, Philip
    Elphinstone, Kevin
    ICFP'09: PROCEEDINGS OF THE 2009 ACM SIGPLAN INTERNATIONAL CONFERENCE ON FUNCTIONAL PROGRAMMING, 2009, : 91 - 95
  • [2] Model-driven development for the seL4 microkernel using the HAMR framework
    Belt, Jason
    Hatcliff, John
    Shackleton, John
    Carciofini, Jim
    Carpenter, Todd
    Mercer, Eric
    Amundson, Isaac
    Babar, Junaid
    Cofer, Darren
    Hardin, David
    Hoech, Karl
    Slind, Konrad
    Kuz, Ihor
    Mcleod, Kent
    Mcleod, Kent
    JOURNAL OF SYSTEMS ARCHITECTURE, 2023, 134
  • [3] seL4 Microkernel for Virtualization Use-Cases: Potential Directions towards a Standard VMM
    de Matos, Everton
    Ahvenjarvi, Markku
    ELECTRONICS, 2022, 11 (24)
  • [4] A High-Performance Multicore IO Manager Based on libuv (Experience Report)
    Han, Dong
    He, Tao
    PROCEEDINGS OF THE 11TH ACM SIGPLAN INTERNATIONAL SYMPOSIUM ON HASKELL (HASKELL '18), 2018, : 172 - 178
  • [5] A High-Performance Multicore IO Manager Based on libuv (Experience Report)
    Han, Dong
    He, Tao
    ACM SIGPLAN NOTICES, 2018, 53 (07) : 172 - 178
  • [6] CoMoO4 nanorods coated separator for high-performance lithium sulfur batteries
    Huang, Minggang
    Jiang, Xiangli
    Xu, Chun
    Zhao, Shuo
    Zhang, Shan
    Li, Guochun
    MATERIALS CHEMISTRY AND PHYSICS, 2023, 295
  • [7] CaMoO4 Nanoparticle-Doped Graphene Oxide as Electrodes for High-Performance Supercapacitors
    Chen, Gang
    Chen, Guangzhou
    Pan, Li
    Chen, Dongsheng
    NANO, 2022, 17 (03)
  • [8] Co3O4@NiCo2O4 microsphere as electrode materials for high-performance supercapacitors
    Zhu, Yan-Rong
    Peng, Pan-Pan
    Wu, Jin-Zhu
    Yi, Ting-Feng
    Xie, Ying
    Luo, Shaohua
    SOLID STATE IONICS, 2019, 336 : 110 - 119
  • [9] Surfactant-assisted morphology modification of nanostructured MnMoO4 for high-performance asymmetric supercapacitors
    Kumcham, Prasad
    Sreekanth, T. V. M.
    Yoo, Kisoo
    Kim, Jonghoon
    NEW JOURNAL OF CHEMISTRY, 2024, 48 (17) : 7820 - 7835
  • [10] NiMoO4 nanowire arrays and carbon nanotubes film as advanced electrodes for high-performance supercapacitor
    Zhang, Si-Wen
    Yin, Bo-Si
    Liu, Chang
    Wang, Zhen-Bo
    Gu, Da-Ming
    APPLIED SURFACE SCIENCE, 2018, 458 : 478 - 488
12345