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 条
  • [1] Breaking into the KeyStore: A Practical Forgery Attack Against Android KeyStore
    Sabt, Mohamed
    Traore, Jacques
    COMPUTER SECURITY - ESORICS 2016, PT II, 2016, 9879 : 531 - 548
  • [2] Formal Verification
    Meenakshi, B.
    RESONANCE-JOURNAL OF SCIENCE EDUCATION, 2005, 10 (05): : 26 - 38
  • [3] Formal verification
    B Meenakshi
    Resonance, 2005, 10 (5) : 26 - 38
  • [4] VERIFICATION - FORMAL OR OTHERWISE
    NEALE, RG
    ELECTRONIC ENGINEERING, 1994, 66 (811): : 5 - 5
  • [5] Formal Verification of Websites
    Flores, Sonia
    Lucas, Salvador
    Villanueva, Alicia
    ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2008, 200 (03) : 103 - 118
  • [6] Formal verification at Intel
    Harrison, J
    18TH ANNUAL IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE, PROCEEDINGS, 2003, : 45 - 54
  • [7] Formal verification of μ-charts
    Goldson, D
    APSEC 2002: NINTH ASIA PACIFIC SOFTWARE ENGINEERING CONFERENCE, 2002, : 129 - 136
  • [8] Formal verification of synchronizers
    Kapschitz, T
    Ginosar, R
    CORRECT HARDWARE DESIGN AND VERIFICATION METHODS, PROCEEDINGS, 2005, 3725 : 359 - 362
  • [9] Formal Verification of HotStuff
    Jehl, Leander
    FORMAL TECHNIQUES FOR DISTRIBUTED OBJECTS, COMPONENTS, AND SYSTEMS, FORTE 2021, 2021, 12719 : 197 - 204
  • [10] Perspectives on Formal Verification
    Friedman, Harvey M.
    PROCEEDINGS OF THE 5TH ACM SIGPLAN CONFERENCE ON CERTIFIED PROGRAMS AND PROOFS (CPP'16), 2016, : 1 - 1
12345