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 条

[41] Formal Verification of Operational Transformation
Liu, Yang
Xu, Yi
Zhang, Shao Jie
Sun, Chengzheng
FM 2014: FORMAL METHODS, 2014, 8442 : 432 - 448
[42] Formal Verification of Unsatisfiability Results
Heule, Marijn J. H.
PROCEEDINGS OF THE 2018 18TH CONFERENCE ON FORMAL METHODS IN COMPUTER AIDED DESIGN (FMCAD), 2018, : 2 - 2
[43] Formal verification of digital systems
Swamy, G
TENTH INTERNATIONAL CONFERENCE ON VLSI DESIGN, PROCEEDINGS, 1997, : 213 - 217
[44] Formal Verification of Differential Privacy
Gaboardi, Marco
PLAS'18: PROCEEDINGS OF THE 13TH WORKSHOP ON PROGRAMMING LANGUAGES AND ANALYSIS FOR SECURITY, 2018, : 1 - 1
[45] Industrial experience with formal verification
Payer, Michael
IT - Information Technology, 2001, 43 (01): : 16 - 21
[46] Formal Verification of the xDAuth Protocol
Alam, Quratulain
Tabbasum, Saher
Malik, Saif U. R.
Alam, Masoom
Ali, Tamleek
Akhunzada, Adnan
Khan, Samee U.
Vasilakos, Athanasios V.
Buyya, Rajkumar
IEEE TRANSACTIONS ON INFORMATION FORENSICS AND SECURITY, 2016, 11 (09) : 1956 - 1969
[47] On combining formal and informal verification
Yuan, J
Shen, J
Abraham, J
Aziz, A
COMPUTER AIDED VERIFICATION, 1997, 1254 : 376 - 387
[48] Modeling and formal verification of IMPP
Khan, S
Waheed, A
SERP'03: PROCEEDINGS OF THE INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING RESEARCH AND PRACTICE, VOLS 1 AND 2, 2003, : 522 - 528
[49] Formal verification of pipelined processors
Bryant, RE
TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, 1998, 1384 : 1 - 4
[50] Formal verification of microinstruction sequencing
Ivanov, L
INTERNATIONAL CONFERENCE ON COMPUTING AND INFORMATION TECHNOLOGIES : EXPLORING EMERGING TECHNOLOGIES, 2001, : 165 - 176

← 1 2 3 4 5 →