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/2666356.2594296, 10.1145/2594291.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 [J].

Kuz, Ihor ;

Liu, Yan ;

Gorton, Ian ;

Heiser, Gernot .

JOURNAL OF SYSTEMS AND SOFTWARE, 2007, 80 (05) :687-699

[7] Formal Verification of a Realistic Compiler [J].

Leroy, Xavier .

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 [J].

Sewell, Thomas ;

Myreen, Magnus ;

Klein, Gerwin .

ACM SIGPLAN NOTICES, 2013, 48 (06) :471-481

← 1 2 →