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 条
  • [21] Coverage metrics for formal verification
    Hana Chockler
    Orna Kupferman
    Moshe Vardi
    International Journal on Software Tools for Technology Transfer, 2006, 8 (4-5) : 373 - 386
  • [22] Formal verification of firewall policies
    Liu, Alex X.
    2008 IEEE INTERNATIONAL CONFERENCE ON COMMUNICATIONS, PROCEEDINGS, VOLS 1-13, 2008, : 1494 - 1498
  • [23] Coverage metrics for formal verification
    Chockler, H
    Kupferman, O
    Vardi, MY
    CORRECT HARDWARE DESIGN AND VERIFICATION METHODS, PROCEEDINGS, 2003, 2860 : 111 - 125
  • [24] Formal verification of reconfigurable systems
    Rahim, Muhammad Abdul Basit Ur
    Raheem, Muhammad Ahsan Ur
    Sohail, Muhammad Khalid
    Farid, Mohammad Atif
    Mufti, Muhammad Rafiq
    SOFT COMPUTING, 2023,
  • [25] Formal verification of an ARM processor
    Patankar, VA
    Jain, A
    Bryant, RE
    TWELFTH INTERNATIONAL CONFERENCE ON VLSI DESIGN, PROCEEDINGS, 1999, : 282 - 287
  • [26] Formal Verification of Bayesian Mechanisms
    Mittelmann, Munyque
    Maubert, Bastien
    Murano, Aniello
    Perrussel, Laurent
    THIRTY-SEVENTH AAAI CONFERENCE ON ARTIFICIAL INTELLIGENCE, VOL 37 NO 10, 2023, : 11621 - 11629
  • [27] Formal verification for C program
    Qian, Junyan
    Xu, Baowen
    INFORMATICA, 2007, 18 (02) : 289 - 304
  • [28] Formal verification of an OS submodule
    Pendharkar, NS
    Gopinath, K
    FOUNDATIONS OF SOFTWARE TECHNOLOGY AND THEORETICAL COMPUTER SCIENCE, 1998, 1530 : 197 - 208
  • [29] Polynomial Formal Verification of Multipliers
    Martin Keim
    Rolf Drechsler
    Bernd Becker
    Michael Martin
    Paul Molitor
    Formal Methods in System Design, 2003, 22 : 39 - 58
  • [30] The MODUS Approach to Formal Verification
    Brewka, Lukasz
    Soler, Jose
    Berger, Michael
    BUSINESS SYSTEMS RESEARCH JOURNAL, 2014, 5 (01): : 21 - 33
12345