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
相关论文
共 50 条
  • [31] Formal verification of PLC programs
    Rausch, M
    Krogh, BH
    PROCEEDINGS OF THE 1998 AMERICAN CONTROL CONFERENCE, VOLS 1-6, 1998, : 234 - 238
  • [32] Formal verification of embedded SoC
    Wang, B
    Lin, ZH
    2001 4TH INTERNATIONAL CONFERENCE ON ASIC PROCEEDINGS, 2001, : 769 - 772
  • [33] Formal Verification of a Transistor PCell
    Langner, Kerstin
    Scheible, Juergen
    2017 13TH CONFERENCE ON PH.D. RESEARCH IN MICROELECTRONICS AND ELECTRONICS (PRIME), 2017, : 205 - 208
  • [34] On bridging simulation and formal verification
    Goldberg, Eugene
    VERIFICATION, MODEL CHECKING, AND ABSTRACT INTERPRETATION, 2008, 4905 : 127 - 141
  • [35] Formal verification made easy
    Schlipf, T
    Buechner, T
    Fritz, R
    Helms, M
    Koehl, J
    IBM JOURNAL OF RESEARCH AND DEVELOPMENT, 1997, 41 (4-5) : 567 - 576
  • [36] The evolution of commercial formal verification
    Kurshan, RP
    PROCEEDINGS OF THE INTERNATIONAL CONFERENCE ON PARALLEL AND DISTRIBUTED PROCESSING TECHNIQUES AND APPLICATIONS, VOLS I-V, 2000, : 2975 - 2980
  • [37] The PERF Approach for Formal Verification
    Benaissa, Nazim
    Bonvoisin, David
    Feliachi, Abderrahmane
    Ordioni, Julien
    RELIABILITY, SAFETY, AND SECURITY OF RAILWAY SYSTEMS: MODELLING, ANALYSIS, VERIFICATION, AND CERTIFICATION, RSSRAIL 2016, 2016, 9707 : 203 - 214
  • [38] On formal equivalence verification of hardware
    Khasidashvili, Zurab
    COMPUTER SCIENCE - THEORY AND APPLICATIONS, 2008, 5010 : 11 - 12
  • [39] Formal verification of an optimizing compiler
    Leroy, Xavier
    TERM REWRITING AND APPLICATIONS, PROCEEDINGS, 2007, 4533 : 1 - 1
  • [40] Formal Verification of Optimizing Compilers
    Zhang, Yiji
    Zuck, Lenore D.
    DISTRIBUTED COMPUTING AND INTERNET TECHNOLOGY (ICDCIT 2018), 2018, 10722 : 50 - 65
12345