Formal Verification of a Keystore

被引：0
作者：
Boender, Jaap [1 ]
Badevic, Goran [1 ]
机构：
[1] Hensoldt Cyber GmbH, Taufkirchen, Germany
来源：
THEORETICAL ASPECTS OF SOFTWARE ENGINEERING, TASE 2022 | 2022年 / 13299卷
关键词：
Formal verification; Software verification; C language; Experience report; Isabelle; Key store;
D O I：
10.1007/978-3-031-10363-6_4
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
This paper is an experience report concerning the verification of a component of our operating system using Isabelle. The component allows for the secure storage of cryptographic key material. We will discuss the method used, describe the connection we created between the component and a standard library, identify lessons learned (both for the verification itself as to the process followed to write and adapt the software to be verified), and discuss possible avenues for further research.
引用
收藏
页码：49 / 64
页数：16
相关论文
共 11 条
  • [1] Cock D, 2008, LECT NOTES COMPUT SC, V5170, P167, DOI 10.1007/978-3-540-71067-7_16
  • [2] Constable S., 2018, ELECT ENG COMPUTER S
  • [3] Greenaway D, 2014, ACM SIGPLAN NOTICES, V49, P429, DOI [10.1145/2594291.2594296, 10.1145/2666356.2594296]
  • [4] Klein G, 2009, SOSP'09: PROCEEDINGS OF THE TWENTY-SECOND ACM SIGOPS SYMPOSIUM ON OPERATING SYSTEMS PRINCIPLES, P207
  • [5] Klein G, 2009, ICFP'09: PROCEEDINGS OF THE 2009 ACM SIGPLAN INTERNATIONAL CONFERENCE ON FUNCTIONAL PROGRAMMING, P91
  • [6] CAmkES: A component model for secure microkernel-based embedded systems
    Kuz, Ihor
    Liu, Yan
    Gorton, Ian
    Heiser, Gernot
    [J]. JOURNAL OF SYSTEMS AND SOFTWARE, 2007, 80 (05) : 687 - 699
  • [7] Formal Verification of a Realistic Compiler
    Leroy, Xavier
    [J]. COMMUNICATIONS OF THE ACM, 2009, 52 (07) : 107 - 115
  • [8] Sahebolamri A., 2018, ELECT ENG COMPUTER S
  • [9] Schirmer N., 2006, DISSERTATION
  • [10] Translation Validation for a Verified OS Kernel
    Sewell, Thomas
    Myreen, Magnus
    Klein, Gerwin
    [J]. ACM SIGPLAN NOTICES, 2013, 48 (06) : 471 - 481
12